ELAPSED-TIME-SENSITIVE DEVS FOR MODEL CHECKING

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.