Translating AADL into BIP - Application to the Verification of Real-time Systems
In this paper, the authors study a general methodology and an associated tool for translating AADL (Architecture Analysis and Design Language) and annex behavior specification into the BIP (Behavior Interaction Priority) language. This allows simulation of systems specified in AADL and application to these systems of formal verification techniques developed for BIP, e.g. deadlock detection. They present a concise description of AADL and BIP followed by the presentation of the translation methodology illustrated by a flight computer example.