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:
FACTum
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 (Marmsoler & Blakqori, 2019).
The following MSC shows such a proof for a reliable adder:
APML proof for 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
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 (Marmsoler, 2019).
Proof Hierarchies
FACTum also supports hierarchical specifications (Marmsoler & Gidey, 2019) and reuse of composition proofs through the notion of verified patterns (Marmsoler, 2018).
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.
References
2019
-
APML: An Architecture Proof Modeling Language
Diego Marmsoler, and Genc Blakqori
In Formal Methods – The Next 30 Years, 2019
To address the increasing size and complexity of modern software systems, compositional verification separates the verification of single components from the verification of their composition. In architecture-based verification, the former is done using Model Checking, while the latter is done using interactive theorem proving (ITP). As of today, however, architects are usually not trained in using a full-fledged interactive theorem prover. Thus, to bridge the gap between ITP and the architecture domain, we developed APML: an architecture proof modeling language. APML allows one to sketch proofs about component composition at the level of architecture using notations similar to Message Sequence Charts. With this paper, we introduce APML: We describe the language, show its soundness and completeness for the verification of architecture contracts, and provide an algorithm to map an APML proof to a corresponding proof for the interactive theorem prover Isabelle. Moreover, we describe its implementation in terms of an Eclipse/EMF modeling application, demonstrate it by means of a running example, and evaluate it in terms of a larger case study. Although our results are promising, the case study also reveals some limitations, which lead to new directions for future work.
-
A Calculus for Dynamic Architectures
Diego Marmsoler
Science of Computer Programming, 2019
With the emergence of mobile and adaptive computing, dynamic architectures have become increasingly important. In such architectures, components may appear or disappear, and connections between them may change over time. Dynamic architectures are usually specified in terms of two separate specifications: a specification of component behavior and a specification of component activation and reconfiguration. To verify them, both specifications are first interpreted over a common model for dynamic architectures and verified against a property specified over the same model. Interpreting the specifications over the model, however, introduce repetitive proof steps, which increase the length of proofs, and thus the effort to develop and maintain them. To address this problem, we developed a calculus for dynamic architectures providing rules to reason about component behavior in a dynamic environment. We proved soundness and relative completeness of the rules, implemented them in the interactive theorem prover Isabelle, and mechanized the corresponding soundness proofs. The calculus can be used to support the abstract verification of dynamic architectures in Isabelle. This is demonstrated by means of a running example and evaluated in terms of four case studies. Our results suggest that the calculus has the potential to reduce the length of proofs for the verification of dynamic architectures, thus reducing the effort to develop and maintain verification results.
-
Interactive Verification of Architectural Design Patterns in FACTum
Diego Marmsoler, and Habtom Kahsay Gidey
Formal Aspects Computing, 2019
Architectural design patterns (ADPs) are architectural solutions to common architectural design problems. They are an important concept in software architectures used for the design and analysis of architectures. An ADP usually constrains the design of an architecture and, in turn, guarantees some desired properties for architectures implementing it. Sometimes, however, the constraints imposed by an ADP do not lead to the claimed guarantee. Thus, applying such patterns for the design of architectures might result in architectures which do not fulfill their intended requirements. To address this problem, we propose an approach for the verification of ADPs, based on interactive theorem proving. To this end, we introduce a model for dynamic architectures and a language for the specification of ADPs over this model. Moreover, we propose a framework for the interactive verification of such specifications based on Isabelle/HOL. In addition we describe an algorithm to map a specifi cation to a corresponding Isabelle/HOL theory over our framework. To evaluate the approach, we implement it in Eclipse/EMF and use it for the verification of four ADPs: variants of the Singleton, the Publisher-Subscriber, the Blackboard pattern, and a pattern for Blockchain architectures. With our approach we complement traditional approaches for the verification of architectures, which are usually based on automatic verification techniques such as model checking.
2018
-
Hierarchical Specification and Verification of Architecture Design Patterns
Diego Marmsoler
In Fundamental Approaches to Software Engineering - 21th International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, 2018
