FACTum is a framework to support the verification of component-based systems combining model checking and interactive theorem proving. 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.
Keywords for this software
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)