A Symbolic Rewriting Semantics of the COMPASS Modeling Language

Modern information systems are built through the integration of different, autonomous components that may themselves be complex systems. This Systems-of-Systems (SoS) architecture is foreseen to underlie future information systems primarily because it promotes modularity, facilitating reuse and maintenance. Nevertheless, engineering verifiably dependable SoS is particularly difficult due to their complexity. In this paper, we present a semantics-based approach for the formal modeling and analysis of SoS using the COMPASS Modeling Language or CML (compass-research.eu). We present an executable rewriting specification of CML in rewriting logic that captures its operational semantics. The semantics is based on a variant of CML’s structural operational semantics and, therefore, its correctness is straightforward. We then generalize the semantics into a symbolic rewriting semantics with which open systems can be symbolically executed and analyzed through the integration of rewriting with solving satisfiability problems modulo arithmetic theories. We illustrate the approach through an example using a version of the Maude tool that integrates with the CVC3 solver.