Embedded Control Systems Design based on RT-DEVS and temporal analysis using UPPAAL
|Title||Embedded Control Systems Design based on RT-DEVS and temporal analysis using UPPAAL|
|Publication Type||Conference Paper|
|Year of Publication||2008|
|Authors||Furfaro, A, Nigro, L|
|Conference Name||Computer Science and Information Technology, 2008. IMCSIT 2008. International Multiconference on|
|Keywords||Analytical models, Automata, automata theory, Automatic control, control system CAD, Control system synthesis, Control systems, DEVS, discrete event system specification, discrete event systems, embedded control systems, embedded control systems design, embedded systems, Java, model checking, model continuity, Real time systems, real-time constraints, RT-DEVS, Safety, System analysis and design, temporal analysis, timed automata, UPPAAL timed automata|
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 specification) 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.