FACTum

FACTum is a framework to support the verification of component-based systems 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.

APML

To support the interactive verification of contract composition, FACTum comes with APML: An Architecture Proof Modeling Language.

The following MSC shows such a proof for a reliable adder:

An APML proof is sketched in a notation similar to message sequence charts and describes why an overall contract follows from the combination of component contracts.

Dynamic Architectures

FACTum also supports the notion of dynamic architectures: architectures in which components can appear and disappear over time and connections between them may change dynamically.

Reasoning about the composition of contracts for dynamic architectures is supported by a corresponding calculus for dynamic architectures.

Proof Hierarchies

FACTum also supports hierarchical specifications and reuse of composition proofs through the notion of verified patterns.

FACTum Studio

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.
• Specification of architecture proofs using APML and generation of corresponding proofs for Isabelle.