Joint Use of SysML and Reo to Specify and Verify the Compatibility of CPS Components

Modeling and verifying the behavior of Cyber-Physical Systems (CPS) with complex interactions is challenging. Traditional languages such as SysML diagrams are not enough to capture CPS coordination. In this paper, we propose a novel approach called SysReo, which extends SysML diagrams (RD, BDD, IBD, SD) with the Reo coordination language. Our main objective is to enhance the interoperability of CPS by providing a more precise representation of system behavior and interaction protocols. To achieve this goal, we extend the SysML sequence diagram (SD) with Reo to create the SysReo SD. Through this integration, we bridge the gap between traditional modeling languages and the coordination demands of CPS. We develop an algorithm to generate Constraint Automata (CA) from SysReo SD, which ensures that CPS components can seamlessly work together. These automata are used in a verification tool that checks formulas expressed in Linear Temporal Logic (LTL). By leveraging LTL and Constraint Automata, we enhance the precision and rigor of CPS verification processes, while guaranteeing that CPS components can seamlessly work together. Furthermore, we apply our approach to a medical CPS case study, illustrating its effectiveness in identifying design flaws early and ensuring system behavior aligns with desired properties.