RWTH Aachen University
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.