With the emergence of ambient and adaptive computing, dynamic architectures have become increasingly important. Dynamic architectures describe an evolving state space of systems over time. In such architectures, components can appear or disappear, and connections between them can change over time. Due to the evolving state space of such architectures, verification is challenging. To address this problem, we developed FACTum Studio, a tool that combines model checking and interactive theorem proving to support the verification of dynamic architectures. To this end, a dynamic architecture is first specified in terms of component types and architecture configurations. Next, each component type is verified against asserted contracts using nuXmv. Then, the composition of the contracts is verified using Isabelle/HOL. In this paper, we discuss the tool’s extended features with an example of an encrypted messaging system. It is developed with Eclipse and active on Github.    «

With the emergence of ambient and adaptive computing, dynamic architectures have become increasingly important. Dynamic architectures describe an evolving state space of systems over time. In such architectures, components can appear or disappear, and connections between them can change over time. Due to the evolving state space of such architectures, verification is challenging. To address this problem, we developed FACTum Studio, a tool that combines model checking and interactive theorem pr...    »