FACTum is a framework for the axiomatic specification of dynamically adapting architectures. A FACTum specification consists of:
- Algebraic specifications for the data types exchanged by components.
- Specification of component types by means of architecture diagrams and behavior trace assertions.
- A specification of architectural aspects, such as component activation and reconfiguration using architecture trace assertions.
FACTum is implemented in FACTum Studio, an Eclipse/EMF application with the following main features:
- Speciﬁcation of an architecture according to FACTum.
- Generation of specifications for the NuSMV model checker.
- Generation of theories for the interactive theorem prover Isabelle.
- Generation of monitors for runtime verification of dynamic architectures.