Verification of COMDES-II Systems Using UPPAAL with Model Transformation

Ke Xu, Paul Pettersson, Krzysztof Sierszecki, Christo K. Angelov

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

444 Downloads (Pure)

Abstract

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.
OriginalsprogEngelsk
TitelProceedings of the 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications RTCSA'2008
Antal sider8
ForlagIEEE Computer Society Press
Publikationsdato2008
ISBN (Trykt)9780769533490
StatusUdgivet - 2008
BegivenhedThe 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2008) - Kaohsiung, Taiwan
Varighed: 25. aug. 200827. aug. 2008
Konferencens nummer: 14

Konference

KonferenceThe 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2008)
Nummer14
Land/OmrådeTaiwan
ByKaohsiung
Periode25/08/200827/08/2008

Fingeraftryk

Dyk ned i forskningsemnerne om 'Verification of COMDES-II Systems Using UPPAAL with Model Transformation'. Sammen danner de et unikt fingeraftryk.

Citationsformater