This paper studies 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. We present a concise description of AADL and BIP followed by the presentation of the translation methodology illustrated by a Flight Computer example.
AADL [
An AADL specification describes the software, hardware, and system part of an embedded real-time system. Basically, an AADL specification is composed of components such as data, subprogram, threads, processes (the software side of a specification), processors, memory, devices and buses (the hardware side of a specification) and system (the system side of a specification).
The AADL specification language is designed to be used with analysis tools that support automatic generation of the source code needed to integrate the system components and build a system executable.
BIP [
In order to demonstrate the feasibility of the BIP language and its runtime
for the construction of real-time systems, several case studies were carried out
such as an MPEG4 encoder [
AmSud project TAPIOCA
This paper provides a general methodology for translating AADL models
into BIP models [
We use existing case studies [
The SAE Architecture Analysis & Design Language (AADL) [
A system modelled in AADL consists of application software mapped to an execution platform. Data, subprograms, threads, and processes collectively represent application software. They are called software components. Processor, memory, bus, and device collectively represent the execution platform. They are called execution platform components. Execution platform components support the execution of threads, the storage of data and code, and the communication between threads. Systems are called compositional components. They permit software and execution platform components to be organized into hierarchical structures with well-defined interfaces. Operating systems may be represented either as properties of the execution platform or can be modelled as software components.
Components may be hierarchical, i.e. they my contain other components. In fact, an AADL description is almost always hierarchical, with the topmost component being an AADL system that contains, for example, processes and processors, where the processes contain threads and data, and so on.
Compared to other modeling languages, AADL defines low-level abstractions including hardware descriptions. These abstractions are more likely to help design a detailed model close to the final product. 2.2
In this section, we describe the fragment of AADL components, connections and annex behavior taken into account by our translation.
Software Components AADL has the following categories of software components: subprogram, data, thread and process. Subprogram : A subprogram component represents an execution entry-point in the source text. Subprograms can be called from threads and from other subprograms. These calls are handled sequentially by the threads. A subprogram call sequence is declared in other subprograms or thread implementations.
A subprogram type declaration contains parameters (in and out), out event ports, and out event data ports. A subprogram implementation contains connections subclause, a subprogram calls subclause, annex behavior subclause, and subprogram property associations. Figure 1 gives an example of a subprogram, that takes as input two integers A, B, and produces the result as output. Data : The data component type represents a data type in the source text that defines a representation and interpretation for instances of data. A data implementation can contain data subcomponents, and data property associations. An example of data is given in Figure 1. subprogram operation features
A: in parameter integer; B: in parameter integer; result: out parameter integer; end operation; data Person end Person; data implementation Person.impl subcomponents
Name : data string; Adress: data string;
Age : data integer; end Person.impl; Thread : A thread represents a sequential flow of control that executes instructions within a binary image produced from source text. A thread always executes within a process. A scheduler manages the execution of a thread.
A thread type declaration contains ports such as data port, event port, and event data port, subprogram declarations, and property associations. A thread component implementation contains data declarations, a calls subclause, annex behavior, and thread property associations.
Threads can have properties. A property has a name, a type and a value. Properties are used to represent attributes and other characteristics, such as the period, dispatch protocol, and deadline of the threads, etc. Dispatch protocol is a property which defines the dispatch behavior for a thread. Four dispatch protocols are supported in AADL: periodic, aperiodic, sporadic, and background.
Figure 2 presents a thread component called sensor, that is a periodic thread with inter-arrival time of 20ms. This thread receives an integer data through port inp and sends an event through port outp.
Process : A process represents a virtual address space. Process components are an abstraction of software responsible for executing threads. Processes must contain at least one explicitly declared thread or thread group, and can contain a connections subclause, and a properties subclause. Figure 2 presents an example of process called Partition, that contains thread subcomponents and two types of connections (data port and event port) between threads. thread sensor features inp : in data port integer; outp : out event port; properties
Dispatch protocol=>Periodic;
Period => 20ms; end sensor; process Partition end Partition; process implementation Partition.Impl subcomponents
Sensor A : thread Sensor Thread.A; Data Fusion: thread Fusion Thread.Impl;
Alrm 1 : thread Alrm Thread.Impl; connections data port
Sensor A.outp->Data Fusion.inpA; event port
Sensor A.launch alrm->Alrm.launch A; end Partition.Impl; Hardware Components Execution platform components represent hardware and software that is capable of scheduling threads, interfacing with an external environment, and performing communication for application system connections. We consider two types of hardware components: processors and devices. Processor : AADL processor components are an abstraction of hardware and software that is responsible for scheduling and executing threads. In other words, a processor may include functionality provided by operating systems. Device : A device component represents an execution platform component that interfaces with the external environment. A device can interact with application software components through their ports.
Systems A system is the toplevel component of the AADL hierarchy of components. A system component represents a composite component as an assembly of software and execution platform components. All subcomponents of a system are considered to be contained in that system. We present an example of system: system Platform end Platform; system implementation Platform.Impl subcomponents
Part : process Partition.Impl;
p : processor myProcessor ;
...
end Platform.Impl;
Annex Behavior Specification Behavior specifications [
<state variables>? <initialization>? <states>? <transitions>? **}; – State variables section declares typed identifiers. They must be initialized in the initialization section. – States section declares automaton states. – Transitions section defines transitions from a source state to a destination state. The transition can be guarded with events or boolean conditions. An action part can be attached to a transition.
Connections A connection is a linkage that represents communication of data and control between components. This can be the transmission of control and data between ports of different threads or between threads and processor or device components. There are two types of connections: port connections, and parameter connections.
Port connection: Port connections represent transfer of data and control between two concurrently executing components. There are three types of port connections: event, data and event data.
Parameter connection: represent flow of data between the parameters of a sequence of subprogram calls in a thread. 3
BIP (Behavior Interaction Priority) is a framework for modeling heterogeneous
real-time components [
The BIP framework consists of a language and a toolset including a
frontend for editing and parsing BIP programs and a dedicated platform for model
validation. The platform consists of an Engine and software infrastructure for
executing models. It allows state space exploration and provides access to
modelchecking tools of the IF toolset [
An atomic component consists of a set of ports used for the synchronization with other components, a set of transitions and a set of local variables. Transitions describe the behavior of the component. They are represented as a labeled relation between control states. A transition is labeled with a port p, a guard g and a function f written in C. The guard g is a boolean expression on local variables and the function f is a block of C code. Fig. 3. BIP Atomic Component When g is true, an interaction involving p may occur, in which case f is executed. The interactions between components are specified by connectors.
Figure 3 shows an atomic component with two control states Si and Sj, ports in and out,and corresponding transitions guarded by guard gi and gj .
Interactions between components are specified by connectors. A connector is a list of ports of atomic components which may interact. To determine the interactions of a connector, its ports have the synchronization attributes trigger or synchron, represented graphically by a triangle and a bullet, respectively. A connector defines a set of interactions defined by the following rules: - If all the ports of a connector are synchrons then synchronization is by rendezvous. That is, only one interaction is possible, the interaction including all the ports of the connector. - If a connector has one trigger port then synchronization is by broadcast. That is, the trigger port may synchronize with the other ports of the connector. The possible interactions are the non empty sublists containing this trigger port.
In BIP, it is possible to associate with an interaction an activation condition (guard) and a data transfer function both written in C. The interaction is possible if components are ready to communicate through its ports and its activation condition is true. Its execution starts with the computation of data transfer function followed by notification of its completion to the interacting components. 4
In this section, we present the translation from AADL [
We define the translation of the different AADL software components into BIP. Subprogram Depending on its structure, we translate the AADL subprograms into atomic or compound BIP components:
As compound component : When the AADL subprogram contains subprogram calls and connections, it is modelled as a compound BIP component. The subprogram calls are executed sequentially. This execution is modelled by an atomic component with states wait call1...wait calln and wait return1...wait returnn, transitions labeled by the ports call1...calln and return1...returnn (where n is the number of the subprograms called sub1...subn). To enforce the right sequence of execution and the transfer of parameters, two ports call and return are used to express calls to the compound subprogram by other subprograms or threads, and the port data to sends event or data to the threads, as shown in Figure 5. Data The data component type represents a data type in the source text that defines a representation and interpretation for instances of data in the source text. In BIP it is transformed into a C data structure. Thread : An AADL thread is modelled in BIP by an atomic component as shown in Figure 6. The initial state of the thread is halted. On an interaction through port load the thread is initialized. Once initialization is completed the thread enters the ready state, if the thread is ready for an interaction through the port req exec. Otherwise, it enters the suspended state. When the thread is in the suspended state it cannot be dispatched for execution.
When in the suspended state, the thread is waiting for an event and/or period to be activated depending on the thread dispatch protocol (periodic, aperiodic, sporadic). In the ready state, a thread is waiting to be dispatched through an interaction in the port get exec. When dispatched, it enters the state compute to make a computation. Upon successful completion of the computation, the thread goes to the outputs state. If there are some out ports to dispatch the thread returns to the outputs state. otherwise, it enters the finish state.
The thread may be requested to enter its halted state through a port stop after completing the execution of a dispatch. A thread may also enter the thread halted state immediately through an abort port.
Process : Processes must contain at least one explicitly declared thread or thread group. The process behavior is illustrated in Figure 7. Once processors of an execution platform are started, the process enters to the state loading through port load and it is ready to be loaded.
A process is considered as stopped when all threads of the process are halted. When a process is stopped, each of its threads is given a chance to finalize its execution.
A process can be aborted by using abort port. In this case, all contained Fig. 7. BIP model for process behavior threads terminate their execution immediately and release all resources.
The Load deadline property specifies the maximum amount of elapsed time allowed between the time the process begins and completes loading. 4.2
This section defines the translation into BIP of processors and devices. Processors AADL processor components are an abstraction of hardware and software that is responsible for scheduling and executing threads. Schedulers are modelled as atomic BIP components as shown in Figure 8. The initial state of a scheduler is idle. When a thread become ready, the scheduler enters the choice state through an interaction on port ready. In this state, the thread ID is stored into the scheduler memory. When a thread is dispatched, the scheduler selects a thread identifier (into SelectedID variable) and enters the wait end state through an interaction on port dispatch. If there are several threads to be dispatched the scheduler re-enters to the state choice, otherwise, it enters the state idle. Devices A device component represents an execution platform component that interfaces with the external environment. A device can interact with application software components through their ports. It is modelled as an atomic component in BIP. 4.3
A system component represents an assembly of software and execution platform components. All subcomponents of a system are considered to be contained in that system. A system is modelled as a compound component in BIP. Figure 9 shows a BIP component representing a system and connexion between threads, process, and scheduler. 4.4
Some annex behavior elements can be directly translated to BIP whereas for others we need new BIP facilities. Actual behaviors are supposed to be described using the implementation language. The proposed behavioral annex allows the expression of data dependent behaviors so that more precise behavioral analysis remains possible.
– The state variables section declares typed identifiers. In BIP, they correspond to data variables. They must be initialized in the initialization section, which is directly included in the BIP initialization part. – The states section declares automaton states as: The initial state is directly included in BIP. The return state indicates the return to the caller. This case is represented in BIP as a transition from return state to idle state. – The transitions section defines transitions from a source state to a destination state. Transitions can be guarded with events or boolean conditions, and can contain an action. Each transition is translated as one or a sequence of BIP transitions. Port connection : is translated in BIP depending on the categories : – an event connection is translated into strong synchronization between the corresponding event ports. – a data connection is translated into connection with transfer of data. – an event data connection is translated into a strong synchronization between the corresponding ports with transfer of data.
Parameter connection : is translated in BIP by transfer of data between the parameters of a sequence of subprogram calls in a thread, as shown in section 4.1. 5
From the high-integrity systems point-of-view, the use of automatic code generation in the development process is profitable. As the generated code is a combination of a relatively small set of extensively tested design patterns, the analysis and review of this code is easier than for hand-written code.
The tool chain is described in Figure 10, 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 (Figure 10) 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.
Fig. 10. AADL to BIP Tool Architecture 6
We used some examples of AADL [
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 interarrival time of 10ms. The graphical representation of Flight Computer system model is given in Figure 11. The AADL model of the Flight Computer is transformed into BIP automatically by using our AADL to BIP translation tool. Figure 12 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 that are shown in the Figure 9.
The component Dummy In Out models the communication between the Dummy Out and Dummy In events ports. In the AADL model (Figure 11), 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. 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 model checking techniques for
verification have been applied:
Model checking by Aldebaran: The first technique of verification is deadlock
detection by using the tool Aldebaran [
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. We apply this technique to verify two properties: • Verification of thread deadlines by using an observer component keeping track of the execution time of threads. If the execution time of a thread exceeds its deadline the observer moves to an error state. • Verification of synchronization between components: Landing Gear is sporadically activated bye HCI trough the Req port. When it is activated, it send back an acknowledgement through the ACK port, and possibly reactivates itself through the Dummy In Out component. This property can be verified by an observer which monitors the interactions between HCI, landing Gear and Dummy In Out components (Figure 11).
The Architecture Analysis and Design Language (AADL) suffers from the
absence of concrete operational semantics. In this paper, we address this problem by
providing a translation from AADL to BIP, which has an operational semantics
formally defined in terms of labelled transition systems. This translation allows
simulation of AADL models, as well as application verification techniques, such
as state exploration (using IF toolset [