Verification of COMDES-II Systems Using UPPAAL with Model Transformation

COMDES-II is a component-based software framework intended for Model Integrated Computing (MIC) of embedded control systems with hard real-time constraints. We present a transformational approach to formally verifying both timing and functional behavior of COMDES-II systems using UPPAAL. The proposed approach adopts timed automata in UPPAAL as the semantic units to which the behavioral semantics of COMDES-II are anchored, such that a COMDES-II system can be equivalently transformed into the timed automata models in UPPAAL, and verified with precise preservation of system operational semantics. In the paper a concrete discussion of semantic transformation from COMDES-II to UPPAAL is given, and a turntable case study is developed to show how to apply the presented approach in practice. 

• Type: Conference
• Year: 2008
• Where: RTCSA
• Authors: Xu Ke, Paul Pettersson, Krzysztof Sierszecki, Christo Angelov
• Keywords: Adopts Timed Automata, Component-based Software Framework, Hard Real-time Constraints, Real-Time Computing, RTCSA 2008