A Formal Modeling Framework for Time-Aware Cyber–Physical Systems of Systems

Cyber–Physical Systems of Systems (CPSoS) integrate autonomous constituent systems to accomplish complex missions. Nonetheless, decentralized coordination and continuous evolution create intricate dependencies that make behavior difficult to analyze. Current semi-formal modeling approaches, despite being easy to understand and widely accessible, lack semantic precision and are not computationally checkable to guarantee time-critical properties. Furthermore, current formal methods are often fragmented: they analyze behavior either at the individual CPS level or the collective CPSoS level, failing to provide a multi-level specification. To address these limitations, we propose an integrated framework combining SysML and Maude rewriting logic. SysML provides structural and behavioral specification capabilities, while Maude enables rigorous semantics, executable models, and formal verification. First, our approach proposes MM-CPSoS, a meta-model that unifies CPS and CPSoS entities with explicit temporal constraints. Dynamic behavior is captured through evolution patterns governing mission progression across both levels. Then, we encode SysML models into Maude as object-oriented configurations and conditional rewrite rules, enabling linear temporal logic (LTL) model checking of temporal properties. Finally, we demonstrate our approach through a Time-Aware Road Crisis Management System (TaRCiMaS2).