Elapsed-time-sensitive DEVS for model checking
Hae Young Lee · Winter Simulation Conference · 2013
The necessity of formal verification for discrete event system specification (DEVS) has recently arisen mainly due to the application of DEVS to engineering of embedded systems. This paper presents a sub-class of DEVS, called elapsed-time-sensitive DEVS (ES-DEVS). In order to provide a more convenient and intuitive way to build simulation models for timed systems, conditions on elapsed times are imposed on state transitions caused by input events. While still verifiable, ES-DEVS is more expressive than finite and deterministic DEVS (FD-DEVS) that is another verifiable and deterministic class of DEVS. ES-DEVS models could be exhaustively verified based on reachability analysis techniques.