Composition and Refinement of Timing Behavior in Safety-Critical Cyber Physical Systems

Cyber physical systems (CPS) are usually used in safety critical scenarios, which require real-time monitoring, compute the feedback data, and realize automatic control and management of the external environment. Model driven development method is the main way to develop real-time and heterogeneous CPS, and the composability of the model is the key point. In this paper, the timing behavior specification model of the system is established by the clock constraint specification language (CCSL), and on this basis, the timing behavior semantics of CCSL is described by the transition systems, and its composition operation method and the formal definition of composability is given. Further, the timing behavior is refined, and the transformation method from the timing behavior model of specification to the task execution model is given, The timing constraint behavior at the specification level is transformed into the timing constraint behavior at the task level. At the same time, the model behavior is learned based on the L* method to realize compositional verification to alleviate the state explosion problem, and the composability of the refined model is verified. Finally, the refinement and verification methods are evaluated by simulation experiments and the master-slave intelligent vehicle example. The relevant data shows that, the refined method and compositional verification methods have some performance advantages in processing time and memory consumption.