Modeling and checking for Cyber–Physical System based on hybrid interface automata

Cyber–Physical Systems (CPS) are hybrid, safety-critical systems. For finding safety or security hazard in the design phase, modeling for CPS and checking their properties become very important. We focus on the compatibility, i.e., two systems can work together, and behavioral nonexistent consistency, i.e., forbidden behaviors do not occur in a system. Hybrid interface automata (HIA), which extend from interface automata and is not input-enabled, are introduced to model CPS. The compatibility of HIA is checked under an optimistic approach, which means if there is an environment in which two HIA cannot reach an illegal location, namely, at the location one cannot accept the input send by the other, they are compatible. Based on a scenario that specifies forbidden behaviors, behavioral nonexistent consistency is boundedly checked by transforming it to an unconstrained dynamic programming, and solving the programming by a genetic algorithm. The method can directly apply to nonlinear hybrid model. It relaxes a restriction on the form of the system dynamic in traditional algorithms. An experiment and simulation validate our algorithms.