Verification of real-time DEVS models

Discrete Event System Specification (DEVS) has been widely used to describe hierarchical models of discrete systems. DEVS has also been used successfully to model with Real-Time constraints. In this paper, we introduce a methodology to verify Real-Time DEVS models, and describe the methodology by using a case study of a DEVS model of an elevator system. Our methodology applies recent advances in theoretical model checking to DEVS models. The methodology also handles the cases where theoretical approach is not feasible to cross the gap between abstract Timed Automata models and the complexity of the DEVS Real-time implementation by empirical software engineering methods. The case study is a system composed of an elevator along an elevator controller, and we show how the methodology can be applied to a real case like this one in order to improve the quality of such real-time applications. Keywords: DEVS, Formal methods verification, Real-Time software, Timed automata. I.