Formal behavior specification for AADL

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.