Table of Contents

• 1- What is AADL ?
• 2- TOOL : AADL to BIP
• 3- Installation
• 4- Case studies
  • 4.1- Simple Example
  • 4.2- Missile Guidance Example
  • 4.3- Flight Computer example
• 5- Deterministic Data Flow Communication
• 5- Verification
• 6- Publications

Architecture Analysis & Design Language (AADL) is a textual and graphical language used to design and analyze the software and hardware architecture of performance-critical real-time systems. The Society of Automotive Engineers standardized it in 2004.
AADL is used to describe the structure of component-based systems as an assembly of software components mapped onto an execution platform. AADL is used to describe functional interfaces and performance-critical aspects of components. It is used to describe how components interact, and to describe the dynamic behavior.

More information can be found on the AADL web site: www.aadl.info.

The tool chain is described in Figure below, and it has the following features:

AADL to BIP Transformation:

Using model transformations, allows to perform analysis on the models before code generation. The tool generating BIP from AADL has been implemented in Java, as a set of plugins for the open source Eclipse platform. It takes an input an AADL model (.aaxl) conforming to the AADL metamodel and generates a BIP model conforming to the BIP metamodel. Models generated may be timed or untimed. Timed models can be transformed into untimed models in which time progress is represented by a tick port that exists in all timed components and a connector connecting all tick ports.

Code Generation:

Takes as input a BIP model and generate the C/C++ code to be executed by the Engine.

Exploration Engine:

The engine has a state space exploration mode, which under some restrictions on the data used, generates state graphs that can be analyzed by using finite state model-checking tools.

Simulation:

Monitors the state of atomic components and finds all the enabled interactions by evaluating the guards on the connectors. Then, between the enabled interactions, priority rules are used to eliminate the ones with low priority.

Verification:

Automatic verification is very useful for early error detection.

In order to install the AADL2BIP plugin you will need Eclipse and the OSATE AADL environment. Below the steps needed to install these components are given in detail.
AADL2BIP Installalation

We used some examples of AADL with/without annex behavior specification. In this section, we present some examples of AADL translated to BIP :

Using data port

--> AADL model:
we will take the AADL model given in the following figure:


The two thread instances TH1 and TH2 are both periodic with periods of 50ms each. At each dispatch TH1 executes before TH2 and deposits an integer value into its output port port1 which is read by TH2 through the input port foo. TH2 multiplies the value by 2 and sends the result back to TH1 through port bar which is read by TH1 on the next dispatch through its input port port2. The system model is given in foobar.aadl. Download it, instantiate the given system and generate the BIP code. Once the code is generated you can executed.

--> BIP model:
Figure below shows the obtained BIP model:


AADL data connection is translated into BIP connector with transfer of data between the corresponding data ports.

AADL model :

Missile Guidance Example has a thread called Controller that periodically sends float data throught port Controlleinput, and receive float data throught port Outputfeedback. The contoller has also a subprogram called Sunseekerconroller that contains a C code (SunSeekerConroller.c) to make some computation. It also has a thread called Plant that periodically sends float data throught port Outputfeedback, and receive float data throught port Controlleinput. This thread has also a subprogram called Sunseekerplant that contains a C code (SunSeekerPlant.c) to make some computation. The outgoing rate specifies the maximum produced missrate, the incoming rate specifies the maximum expected rate that the controller can handle. This AADL model is inspired from the original SunSeeker model published by SEI for the SAE AADL standard.
The graphical representation of missile guidance (SunSeeker.aadl) system model is given below :

BIP model :

The AADL model of the Missile Guidance is transformed into BIP automatically by using our AADL to BIP translation tool. Figure below shows the obtained BIP model.


This Figure represents the BIP atomic components (AADL Threads with subprograms) and connectors between them. The connectors between threads, process and scheduler are represented in this Figure:

AADL model :

The Flight Computer has a thread called Sensor_Sim that periodically sends integers data for the current AoA(angle-of-attack) and Climb Rate, and an event in case of Engine Failure. It also has a thread called Stall Monitor that is periodic and monitors the condition of the AoA and Climb Rate sensors and raise a stall warning if certain conditions are met. The thread Operator simulates the pilot. It is a periodic thread that sends a command (Gear_Cmd) at every dispatch to raise or lower the landing gear of the aircraft. The thread Landing Gear simulates the landing gear subsystem. It receives a command to start a landing gear operation, and is a sporadic thread with a minimum inter-arrival time of 3 seconds. The thread HCI is a human computer interface. It receives a Stall Warning as an event data of type Integer; Engine Failure as an event; a landing gear command from the pilot. It may send a landing gear operation request (Gear_Req) to the landing gear subsystem, and receives a landing gear operation acknowledgement (Gear_Ack) from the landing gear subsystem. It is a sporadic thread with a minimum inter-arrival time of 10ms. The graphical representation of Flight Computer (flt_mgmt.aadl) system model is given below :

BIP model :

The AADL model of the Flight Computer is transformed into BIP automatically by using our AADL to BIP translation tool. Figure below shows the obtained BIP model.


This Figure represents the BIP atomic components (AADL Threads) and connectors between them. Notice that we omit here the connectors between threads, process and scheduler.
The component Dummy_In_Out models the communication between the Dummy_Out and Dummy_In events ports. In the AADL model, these two events are used to control thread reactivation: execution of the Landing_Gear thread is activated by the Dummy_In event; it emits a Dummy_Out event upon completion. Thus, synchronizing these two events ensures periodic activation of this thread.

AADL provides the structure of component-based systems as an assembly of software components mapped onto an execution platform. AADL is used to describe functional interfaces and performance-critical aspects of components. It is used to describe how components interact, and to describe the dynamic behavior of the runtime architecture. The language is designed to be extensible to accommodate analysis of runtime architectures.

One of the properties that critical systems must usually exhibit is determinism, i.e.: two runs of the system with the same inputs should produce the same outputs, every time. In fact, deterministic execution is one of the pre-requisites for creating high-integrity applications such as control or embedded systems. The main reason is that, the validation is usually performed by testing the implementation of the system, and testing non-deterministic implementation is difficult: non-determinism can make the tests non-reproducible, and the test coverage is hard to define and to measure.

Unfortunately, data flow communication between AADL components is not deterministic, thus leading to non-deterministic execution in general and preventing the use of AADL for most critical systems.

Modelization of deterministic data flow communication:

We model deterministic data flow communication, in two atomic BIP components (get_data and set_data):



The modelization which we proposed is applicable for both data port connections:

Immediate data connection:

We call a Deterministic BIP Communications for Immediate connection by DBCI, the pair of atomic components (get_data & set_data) that implement a data flow between two threads. The communication between two threads and DBCI is shown below:

Delayed data connection:

We call a Deterministic BIP Communications for Delayed connection by DBCD, the atomic component (set_data) that implement a data flow between two threads. The communication between two threads and DBCD is shown below:


The type of BIP connectors between threads and DBCI/DBCD is a strong synchronization with transfer of data from in ports to out ports.

Case study :

Consider a simple application, consisting of three threads sensors with period=20ms, one thread Data_Fusion with period=30ms, and one Actuator that works at 20ms also. All the threads are periodic (Dispatch\_Protocol => Periodic). The application architecture of control System(control.aadl) is shown below:


Sensor_A, Sensor_B and Sensor_C increments an integer variable and sends it periodically to Data_Fusion over its data port. Those threads contains a C code respectively (sensorA.c, sensorB.c, sensorC.c).

Data_Fusion reads the values of its data ports, adds them, and periodically sends the sum to the Actuator thread. The thread Data_Fusion control its inputs. When the variable received from Sensor_A, Sensor_B and Sensor_C are not equals, then the thread prints an error statement, otherwise it does nothing.These thread contain a C code dataFusion.c

Actuator reads and print the value of its data port at every dispatch. These thread contain a C code actuator.c

Simulation :

To try the example, you will need to download control.aadl, Create an AADL project and copy the control.aadl inside aadl folder. Instantiate the system and generate code from it.
The AADL model of control system is transformed into BIP automatically by using our AADL to BIP translation tool. We execute a BIP model. The thread Data_Fusion prints out an error message each time it encounters an unexpected value. In the current case the outputs are of the form:
``DataFusion : ERROR does not have the same inputs''

These errors are due to the non-deterministic nature of the data-flow among the various threads. In order to fix this problem, in AADL, We generate a BIP model using a DBCI component. This time, there will be no errors in the execution.

The model construction methodology applied to this example, opens the way for enhanced analysis and early error detection by using verifications techniques. Once the model has been generated, two mo del checking techniques for verification have been applied:

Model checking by Aldebaran:

The first technique of verification is deadlock detection by using the tool Aldebaran. Exhaustive exploration by the BIP exploration engine, generates a Labeled Transition System (LTS) which can be analyzed by model checking. e.g, Aldebaran takes as input the LTS generated from BIP and checks for deadlock-freedom.

Model checking with observers:

The second technique of verification is by using BIP observers to express and check requirements. Observers allow us to express in a much simple manner most safety requirements.

Mohamed Yassin Chkouri, Anne Robert, Marius Bozga, and Joseph Sifakis. Translating AADL into BIP - Application to the Verification of Real-time Systems. In Proceeding of Model Based Architecting and Construction of Embedded Systems, 2008.[pdf]

*This work is partially supported by the ITEA/Spices project as well as by OpenEMBeDD.