Title :
A Study of the AADL Mode Change Protocol
Author :
Bertrand, Dominique ; Deplanche, A.-M. ; Faucou, Sébastien ; Roux, Olivier H.
Author_Institution :
Univ. de Nantes, Nantes
fDate :
March 31 2008-April 3 2008
Abstract :
This paper describes a contribution to the verification of AADL models. It focuses on the part of the language dealing with operating modes. An analysis of the AADL mode change protocol is provided. Then, a translation process is exposed, that takes as an input an AADL model and produces as an output a time Petri net. Lastly, it is explained how the resulting time Petri net model can be used to (formally) verify some real-time properties of the AADL model.
Keywords :
Petri nets; formal verification; protocols; software architecture; Architecture Analysis and Design Language mode change protocol; formal verification; time Petri net model; translation process; Communication switching; Computer architecture; Control systems; Delay; Protocols; Real time systems; Resource management; Safety; Switches; System recovery; AADL; multi-modal systems; time Petri nets;
Conference_Titel :
Engineering of Complex Computer Systems, 2008. ICECCS 2008. 13th IEEE International Conference on
Conference_Location :
Belfast
Print_ISBN :
0-7695-3139-3
DOI :
10.1109/ICECCS.2008.29
