Temporal Verification of RT-DEVS Models with Implementation Aspects

Finite and Deterministic DEVS (FD-DEVS) is a useful formalism for modelling and analysis of embedded control systems. The formalism differs from classical DEVS in that it admits both state and event sets to be finite. All of this favours verification by permitting the generation of a finite time reachability graph. In the work described in this paper, FD-DEVS concepts are exploited in the context of the RT-DEVS language. Key points of RT-DEVS are the adoption of a weak-synchronous communication model and the use of time pairs in phases for representing the time advance function. RT-DEVS models are preliminarily transformed into Uppaal timed automata for property analysis through model checking. Although verification normally rests on the assumption of maximal parallelism (i.e., each component runs on its associated processor) the proposed transformation process is able to take into account also a limited number of computing resources and a specific scheduling algorithm. The paper details the developed approach and demonstrates its application through the modelling and verification of a real-time system with timing constraints, supposed to be executed on a single processor under non-preemptive (NP) earliest deadline first (EDF) scheduling.