FACTum is a framework to support the verification of architecture specifications combining model checking and interactive theorem proving.
The approach can be sketched as follows:
In FACTum, the verification of overall system properties is split into two steps: First, suitable contracts are specified for the components (represented by gray boxes) and verified against their implementation. Since single components are usually of limited complexity, this step can be fully automated using model checking techniques. In a second step the contracts are combined to verify overall system properties. This step is usually more complex and usually requires manual interaction. Thus, in FACTum, we use interactive theorem proving to reason about the combination of contracts.
FACTum is implemented in FACTum Studio, an Eclipse/EMF application with the following main features:
- Algebraic specifications for the data types exchanged by components.
- Specification of component behavior by means of statemachines and corresponding contracts by means of behavior trace assertions.
- Specification of architectural aspects using architecture diagrams and architecture trace assertions.
- Generation of corresponding specifications for the NuSMV model checker.
- Generation of theories for the interactive theorem prover Isabelle.