Model Checking Coordination of CPS Using Timed Automata

The growing complexity of Cyber-Physical Systems (CPS) increasingly challenges the existing methods and techniques. The correctness of coordination between heterogeneous components of CPS is still a challenging problem. The coordination of CPS could be implemented with co-simulation technology, which uses Functional Mock-up Interface (FMI) techniques to generate simulations of heterogeneous components in CPS. However, the master algorithm for co-simulation may cause livelock or deadlock. Moreover, the architecture modeling of CPS may also introduce an algebraic loop which is a feedback loop resulting in cyclic dependencies. To solve these problems, we propose a novel approach for model checking several properties of coordination such as deadlock, liveness and reachability. We model the architecture of CPS with SysML Block Definition Diagrams (BDDs) and Internal Block Diagrams (IBDs), which capture the dependence of Functional Mock-up Units (FMUs) and the orchestration of the master algorithm. According to BDD models, the coordination between components is implemented with the master algorithm. We model three various master algorithms with Timed Automata (TA). Besides, we encode FMU components with TA to bridge the semantics gap between FMU and TA. With the help of the model checker UPPAAL, we can analyse the correctness of the master algorithms and detect whether there is an algebraic loop in the architecture. In this way, the coordination of CPS is verified with model checking.