A development methodology for embedded systems based on RT-DEVS

This work is concerned with modelling, analysis and implementation of embedded control systems using RT-DEVS, i.e. a specialization of classic discrete event system specification (DEVS) for real-time. RT-DEVS favours model continuity, i.e. the possibility of using the same model for property analysis (by simulation or model checking) and for real time execution. Special case tools are reported in the literature for RT-DEVS model analysis and design. In this work, temporal analysis of a model exploits a translation in Uppaal timed automata for exhaustive verification. For large models a simulator was realized in Java which directly stems from RT-DEVS operational semantics. The same concerns are at the basis of a real-time executive. The paper describes the proposed RT-DEVS development methodology and clarifies its implementation status. The approach is demonstrated by applying it to an embedded system example which is analyzed through model checking and implemented in Java. Finally, research directions which deserve further work are indicated.