Formal behavior specification for AADL

Author

Li, Changde ; Zhou, Xingshe ; Dong, Yunwei

Author_Institution

Sch. of Comput. Sci. & Eng., Northwestern Polytech. Univ., Xi´´an, China

Volume

2

fYear

2010

fDate

10-11 July 2010

Firstpage

110

Lastpage

113

Abstract

AADL is an Architecture Description Language based on the MetaH language which describes an embedded system, as a collection of interacting components. This paper discusses the use of CSP for the specification of architectural models expressed in the modeling language AADL. This allows simulation of systems specified in AADL and application to these systems of formal verification techniques developed for CSP, e.g. deadlock detection. A prototype of behavior specification is proposed through the transformation semantics of flow and port connection. And finally, a case study is given to validate the feasibility.

Keywords

embedded systems; formal specification; formal verification; hardware description languages; simulation languages; AADL; MetaH language; architecture description language; behavior transformation semantic; component based software; deadlock detection; embedded system; formal behavior specification; formal verification technique; modeling language; port connection; Reliability engineering; AADL; Architecture; CSP; Component; behavior;

fLanguage

English

Publisher

ieee

Conference_Titel

Industrial and Information Systems (IIS), 2010 2nd International Conference on

Conference_Location

Dalian

Print_ISBN

978-1-4244-7860-6

Type

conf

DOI

10.1109/INDUSIS.2010.5565667

Filename

5565667