Application of real-time DEVS to analysis of safety-critical embedded control systems: Railroad crossing control example

This article presents an application of the Discrete Event System Specification (DEVS) framework to the design and safety analysis of a real-time embedded control system, a railroad crossing control system. The authors employ an extension of the DEVS formalism, real-time DEVS (RT-DEVS), which has a sound semantics for the specification of real-time systems in a hierarchical modular fashion. The notion of a clock matrix for communicating RT-DEVS models is proposed, which represents a global time between the models. Based on the composition rules and the clock matrix, an algorithm for the generation of a timed reachability tree is developed that can be used for safety analysis at two phases: an untimed and timed analysis phase. A railroad crossing control example demonstrates that the proposed analysis for RT-DEVS models would be effective to verify the safety property of real-time control systems.