Nondeterministic and elapsed-time-sensitive DEVS
Ji-Hyeon Yoon, Hae‐Young Lee · 2014
Discrete Event System Specification (DEVS) has been applied to the development of embedded systems, so that the necessity of formal verification for DEVS has arisen. This paper presents a verifiable subclass of DEVS, called nondeterministic and elapsed-time-sensitive DEVS (NES-DEVS). By mapping a state into an interval, NES-DEVS allows non-determinism at the time advance function. It also provides a more intuitive way to describe systems whose transitions are affected by elapsed times, by imposing time constraints on external state transitions. While still verifiable, it is more expressive than finite and real-time DEVS that is another verifiable subclass of nondeterministic DEVS.