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:

  • Specification 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.