Embedded control systems design based on RT-DEVS and temporal analysis using UPPAAL

Abstract—This work is concerned with modelling, analysis and implementation of embedded control systems using RT-DEVS, i.e. a specialization of classic DEVS (Discrete Event System Speci-fication) 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 proposed in the literature for RT-DEVS model analysis and design. In this work, temporal analysis exploits an efficient translation in UPPAAL timed automata. The paper shows an embedded control system model and its 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 discusses the implementation status and, finally, indicates research directions which deserve further work. Index Terms—DEVS, real-time constraints, embedded control systems, model continuity, temporal analysis, timed automata, model checking, Java. I