DocumentCode
3292158
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
fYear
2008
fDate
March 31 2008-April 3 2008
Firstpage
288
Lastpage
293
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Engineering of Complex Computer Systems, 2008. ICECCS 2008. 13th IEEE International Conference on
Conference_Location
Belfast
Print_ISBN
0-7695-3139-3
Type
conf
DOI
10.1109/ICECCS.2008.29
Filename
4492905
Link To Document