FORS: Separating Configuration From Formal Specification

FORS is a domain specific language (DSL) language for formal specification of product lines. It is specifically designed to allow domain experts to specify the behavior of a (new) product in an unambiguous manner. FORS uses a library design. The allowed generic behavior of the product line is formally specified in libraries. Building a specification then consists of combining and configuring generic behavior from these libraries. This separation of configuration and specification allows for division of labor. Domain engineers can create the libraries by domain modeling and domain experts can configure/create products without any intimate knowledge of formal specification. The language uses Alloy, a lightweight model checker, to test the specifications. FORS requires as input a formal specification which describes the product, the pre- and postconditions of each event (operation) on the product and its invariants. The output consists of an Alloy model. In Alloy all combinations of possible events in a bounded scope are executed in order to test the product's invariants. A benefit of FORS over Alloy directly is that it is also able to construct test cases (traces of operations) from the specification which can be used to test the implementation. FORS was tested in a real world scenario, in the domain of savings accounts. In collaboration with ING the accounts were modeled and formally specified in FORS. FORS was able to find a scenario in which the positive balance invariant was violated. It showed how a series of events allowed by the specification led to a negative balance. The language however does not scale very well due to a lack of primitives within Alloy, more specifically in SAT. Satisfiable Modulo Theories (SMT), an extension to SAT, does include a larger set of primitives and could be used in further research to verify formal specifications.