关键词: Event-B, 实时系统建模, 时间触发系统, 分布式多时钟

Abstract: Modeling and verifying timing properties are essential for the safety-critical Cyber-Physical Systems (CPS). The model verification based on Event-B avoids the state space explosion problem of the model checking method based on state traversal, and the time consuming is less. Therefore, it is suitable for high-concurrency systems modeling. However, there is no time semantics in the common Event-B method, especially for time-triggered property that can greatly improve the predictability of systems. Firstly, based on Event-B, an abstract modeling framework for time-triggered systems (TTEB) is proposed, which models and refines timing properties for the behavior layer and the implementation layer. Secondly, the time-triggered properties of the behavior layer is modeled by a time- triggered transition composed of an ordered chain of events. The transition from the behavior model to the implementation model is realized by the refinement and decomposition of the global clock to the local clock. The periodic synchronization of distributed clocks in the implementation layer is modeled by the time-triggered transition. Finally, the modeling and verification of the master-slave car following system proves the usability and effectiveness of the method.

Key words: Event-B, real-time system modeling, time-triggered system, distributed multi-clock