Verification of COMDES-II Systems Using UPPAAL with Model Transformation

Ke Xu (Foredragsholder)

Aktivitet: Foredrag og mundtlige bidragForedrag og præsentationer i privat eller offentlig virksomhed


COMDES-II is a component-based software framework
intended for model-integrated development of embedded control systems with hard real-time constraints. It provides various kinds of component models to address critical domain-specific issues, such as real-time concurrency and communication in a timed multitasking environment, modal continuous operation combining reactive control behavior with continuous data processing, etc., by following the principle of separation-of-concerns. In the paper we present a transformational approach to the formal verification of both timing and reactive behaviors of COMDES-II systems using UPPAAL, based on a semantic anchoring methodology. The proposed approach adopts UPPAAL timed automata as the
semantic units, to which different behavioral concerns of COMDES-II are anchored, such that a COMDES-II system can be precisely specified in UPPAAL, and verified against a set of desired requirements with the preservation of system original operation semantics.
Periode26. aug. 2008
BegivenhedstitelThe 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2008)
PlaceringKaohsiung, Taiwan