2010 15th IEEE International Conference on Engineering of Complex Computer Systems

Supporting the Design of Safety Critical Systems

Using AADL
T. Correa, L. B. Becker, J.-M. Farines J.-P. Bodeveix, M. Filali F. Vernadat
Federal University of Santa Catarina IRIT-CNRS LAAS-CNRS
Dept of Automation and Control Systems Université de Toulouse Université de Toulouse
Florianopolis, Brazil Toulouse, France Toulouse, France
{tiagotb,lbecker,farines}@das.ufsc.br {bodeveix,filali}@irit.fr [email protected]

Abstract: Designing safety critical systems is a complex II. R ELATED M ETHODOLOGIES AND T OOL S UPPORT
task due to the need of guaranteeing that the resulting Designing new generations of embedded real-time systems
model can cope with all the functional and non-functional is so complex that became mandatory to work with higher
requirements of the system. Obtaining such guarantees is abstractions (namely computational models) previous to imple-
only possible with the use of model verification techniques. mentation. The Model Driven Engineering (MDE) [10] is, for
This paper presents an approach aimed to fulfill the needs instance, an initiative to help developers to manage software
of critical system design. The proposed approach is based development complexity using models at the very beginning,
on the Architecture Analysis and Design Language (AADL), and with different abstraction levels. The key aspect from
which is suitable to describe the system’s architecture. A this technology is the design of models that are decoupled
sequence of model transformations facilitates the verification from their target platform. Among the main benefits of the
of the designed AADL model and so assures its correctness. emerging MDE approach it should be highlighted its enhanced
It must be highlighted that this is not performed in a single possibilities for early model verification.
step, as it is possible to verify AADL models with different In fact, many recent tools have been proposed to support
abstraction levels, which allows successive refinements in a different kinds of verification. With respect to our concerns,
top-down approach. timing verification tools have been an active area of research
over these last years. It is interesting to remark that although
most of these tools are based on existing theoretical models,
I. I NTRODUCTION
e.g., timed automata, Petri nets, the limitations (especially
with respect to combinatorial explosion and scalability) of
The Architecture Analysis & Design Language (AADL) [6]
which are well known, the effort has been undertaken to
is a textual and graphical language used to design and analyze
achieve them. In fact, it is hoped that first, the abstraction
the software and hardware architecture of safety critical real-
and the structure brought by the model driven approach and
time systems. AADL is used to describe the structure of
second, the adoption of a specific execution model will help
systems as an assembly of software components mapped
to struggle against these limitations. Along these lines, we
onto an execution platform. It is used to describe functional
can cite the Cheddar [4] scheduling tool which proposes
interfaces to components (such as data inputs and outputs) and
dedicated analysis for the AADL execution model. Currently,
performance-critical aspects of components (such as timing).
it considers mainly analytical models. Future versions should
In order to support model analysis, AADL relies on a precise
take into account more detailed behavior descriptions [7]. The
execution model. AADL is by now a standard [9]; The version
tools Uppaal Port [8] and Pola[2] are based on the traditional
2 has been recently voted.
model checking approach. Uppaal Port is based on timed
The goal of this paper is to present an approach that supports automata and supports component based development. In order
model checking over AADL models. This is possible by means to reduce the combinatorial explosion Uppaal Port adopts a
of a sequence of model transformations, which finishes when synchronous like execution model which restricts interleaving
the model is suitable for verification, as further discussed along of the asynchronous approach. Moreover, it proposes partial
the paper. Using the proposed approach we expect to enhance order techniques for reducing space explorations. The tool Pola
considerably the reliability of AADL models designed for is based on timed Petri nets, and it proposes specific support
safety-critical applications. for the AADL execution model.
The remainder parts of the paper are structured as follows:
Section II discusses some related methodologies and tool III. T HE P ROPOSED A PPROACH
support. Sections III and IV detail the proposed verification Our proposed design-process for critical embedded systems
approach and its application in a case study. Section V presents supports the safe design of the system’s architecture using
our conclusions and directs our future work. MDE’s principles. By safe design we mean that the resulting

978-0-7695-4015-3/10 $26.00 © 2010 IEEE 331

DOI 10.1109/ICECCS.2010.52
system architecture goes through several verification steps 4A). The target hardware architecture definition (level-4B),
in order to assure its correctness. To reach this goal it is although very important in the context of the proposed process,
performed a sequence of model transformations, which starts should be subject of additional investigation and therefore
with an AADL model and finishes with an automaton model is left out of this work. Given that the verification chain is
that can be verified. This section skips the details of the detailed in the next section, the reminder parts of the current
verification chain (which is covered in the next section) and section details every level depicted in Figure 1. We use an
concentrates in the high-level steps of the proposed process, Autonomous Parking (AP) System case study to elucidate the
which are shown in Figure 1. work performed in each level.
A. Requirements Definition
1. Requirements Definition
The initial step in any development methodology is to
2. Functional Modeling + Simulation define the requirements of the system to be developed. This
Proposed
includes both functional requirements (FR) and non-functional
3. Environment Description
AADL process requirements (NFR). While the former depicts the main func-
4A. Sw Architecture Modeling 4B. Hw Architecture Modeling
tionalities to be performed by the system, the latter imposes
restrictions to those functionalities.
5. Sw/Hw Mapping Table III-A presents the list of requirements from the AP
5B. Architecture Simulation system, which has three main functionalities: (FR1) start/stop
the system using a GUI; (FR2) search for a parking slot; and
6. Refine Real‐Time Properties
(FR3) parking the car. NFRs are like properties that must be
7. Timing Verification satisfied by the related FR. For example, NFR2.2 states that
if the speed is too high (over 20km/h), than it is not possible
to search for a parking slot.
Fig. 1. Proposed Design Flow
FR1 - Start/stop the system using a GUI
The process starts in level-1 with the definition of the Description: The system must be explicitly activated
functional and non-functional requirements of the system, by the driver to start operation
resulting in a textual set of requirements. It is followed by NFR1.1 - To start the system the speed must
Maximum speed be kept at ≤ 20Km/h
the design of a functional model for the system (e.g. Lustre or NFR1.2 - The system must inform the user
Simulink model). In level-3 it begins the design of the AADL On operation while it is working
model, providing the specification of the external devices NFR1.3 - The system must inform the user
Finished as it is turned off
(environment) that interact with the system. Level-4 is split
FR2 - Search for a parking slot (real-time operation)
in two parts: (4A) software architecture modeling/verification
Description: When activated, the system must start
and (4B) hardware architecture modeling. The overall result searching a new park slot as the vehicle moves forward
here should be an AADL model with basic properties already NFR2.1 - The system must inform the user
verified and a hardware architecture potentially capable to Driver alert when a new parking slot is found
NFR2.2 - If the speed is too high (over 20km/h)
run the designed software model. In level-5 a mapping from Safety than it is not possible to search a parking slot
the modeled software components to the hardware model is FR3 - Parking (real-time operation)
performed. The result is a complete AADL model. In level-6 it Description: The driver must trigger the beginning
is suggested that the real-time properties of the AADL model of the parking after a parking slot is found.
The system controls the speed and direction of the vehicle.
should be updated with the precise timing information coming
NFR3.1 - The system is allowed to start parking
from the simulation of the software in the target platform, Safety only if the current speed is zero
which is conducted in level-5B. The proposed development NFR3.2 - The system must be halted immediately
process is concluded in level-7 with the final model verifica- Emergency Stop if the driver moves the wheel
NFR3.3 - The system must alert the driver when
tion, which uses as input the AADL model updated with the Finish allert the parking maneuver is finished
precise timing information.
TABLE I
It is important to highlight that the design flow among the R EQUIREMENTS SET OF THE AUTONOMOUS PARKING (AP) S YSTEM
levels is not unidirectional. Every time that a verification step
fails the designer should either backtrack to higher abstraction
levels of the AADL model and its properties or change
assumptions made in earlier levels. For example, if there is B. Functional Modeling and Simulation
an error in the timing verification (level-7), then the designer In many applications, especially those related with control
should be able to judge if the problem is due to the result of systems, it is required to first design a functional model of
level-4A (proposed software architecture) or to the result of the system and to simulate it before any design decision on
level-4B (target hardware architecture). the system architecture is carried on. This is used either to
In this paper we concentrate the discussions on the software provide a deeper understanding of the system functionalities
architecture modeling and in the verification chain (level- or to test/simulate control solutions in early development stage.

332
Tools like Scade/Lustre and Matlab/Simulink are often used times due to the lack of information in the model), a new
for this propose. refinement in each component should take action, starting new
iterations.
C. Environment Description
Following this approach, each component of the AADL
The third level of the proposed process consists of using model can derive into several subcomponents. By definition,
AADL to describe the environment that interacts with the the successive refinements will only finish as the model
system under development. In other words, it is necessary to contains enough details to be proof correct or incorrect by the
define the set of interactions of the system with the external model verification. Each detailed model (i.e. iteration) should,
devices, such as sensors, actuators, user interface, etc. however, cope with the abstract behavior defined for the
For this reason it is suggested here the use of a high- higher level component. Follows a more detailed discussion
level AADL diagram. Figure 2 presents the diagram designed about the main steps of this phase, namely Architecture
for the AP system, where it is possible to observe the main Refinement and Model Verification.
system in the center (named ParkingCtrl) surrounded by 1) Architecture Refinement: The architecture refinement
the devices. An advantage of using AADL is that it allows process consists of successive model refinements and verifi-
detailing each message exchanged between the system and the cation, as suggested in the design flow from Figure 3. It starts
devices, including information like data type, arrival pattern, with identifying the operation modes (1) and threads (2) of
and time constraints. the system, being followed by the mapping of functions to
threads (3). Afterwards the designer can make the connections
among the threads (4) and associate an execution mode to each
thread (5). The reminder of this section details these steps and
presents its application on the AP system.

A2.2. Architecture Refinement

1. Identify modes

yes
2. Identify threads
new
refinement?

3. Map functions to threads

A1. Select System or Thread

4. Add connections

Fig. 2. AP System Environment Description.

5. Assign modes to threads

In this phase it is assumed that two different kind of external

devices can exist: reused devices and new devices. While
devices like sensors and actuators are normally reused from Fig. 3. Refined steps from Architecture Refinement
previous applications, devices like User Interfaces (UI) are
normally designed on demand for each application. We suggest organizing the functionalities of the system
New devices can be subject of formal verification prior to using different operation modes. This can be seen as a kind
its use in the model. Therefore it is necessary to specify the of temporal decomposition of the set of available functions.
device’s behavior. In the scope of this work it is suggested to Therefore it is necessary to identify how many different modes
describe behavior using finite automatons. the system should have. These modes can be used to guide the
modeling of the distinct AADL processes that will be used to
D. Software Architecture Modeling decompose the system in sub-parts. In our case study, the sub-
The software architecture modeling (level-4A) is probably functions of the first decomposition are more or less analogous
the most important phase of the proposed design process. This to the operation modes.
phase may have several steps of iterations, given the fact that After the identifications of the system (sub)functions it is
the designer may create several AADL models, from more possible to decompose the AADL model into different threads.
abstract to more detailed ones. Moreover, each step should This can be either the first level of decomposition of the
have its properties verified before the designer proceeds with AADL-system or a refinement of an existing thread. Defin-
detailing the AADL model. ing connections means to establish the information exchange
In the first iteration the designer must detail the AADL among the system subparts (threads). This also requires the
system process (e.g. ParkingCtrl at Figure 2) into a set of definition of the data types associates with each port that
subcomponents (that can be either processes or threads). As transfer data.
this detailing is completed, model verification is performed, For the AP system case study, the first level of decomposi-
as explained in the next section. If the verification fails (many tion consists basically in three threads, as shown in Figure 4.

333
SystemManagement is used to start or halt the AP system be obtained using, for example, model simulation on top
by means of the graphical interface (FR1), SlotSelection of the target architecture. Thereby it is possible to obtain
is responsible to search for a parking slot (FR2), and finally the worst case execution time (WCET) for each function of
ParkingManeuver is responsible to perform the parking the system prior to its implementation. The last step of the
(FR3). proposed process is in charge of making the verification of the
timing properties. Schedulability and response-time analysis
are exemples of possible properties to be verified.
IV. V ERIFICATION P ROCESS
It is possible to argue that our proposed verification process
supports the safe design of the system’s architecture using
MDE’s principles. By safe design we mean that the resulting
system architecture goes through several verification steps
in order to assure its correctness. To reach this goal it is
performed a sequence of model transformations, which starts
with an AADL-like model and finishes with an equivalent
automaton model that is suitable for verification.
The verification process we have been working on uses
AADL models as input and performs the model checking of
LTL properties. Moreover, schedulability and buffer overflow
can also be analyzed, as well as user defined properties. This
process is split in the following phases (Figure 5):
Fig. 4. AADL model of parking control system (in the first decomposition)

Once we have both functions and threads defined it is AADL LTL

model property
necessary to relate them, i.e. define which functions belong to
each thread. Here, information like periodicity and deadlines
of threads and functions can be defined. The result of this AADL2FIACRE selt diagnostic
mapping in the AP system is shown in Figure 4. As it can be
observed, in this level every thread is responsible for one FR frac tina Automaton
Fiacre TTS
of the system. model model model
Finally it is required to define in which operation modes
each thread will be active. This represents a common modeling
procedure to make the timing decomposition of the system Fig. 5. The verification process.
functionalities. In AADL this is performed directly in the code,
i.e. there is no graphical representation for this association. It • Use of the OSATE-TOPCASED [11], [12] environment
must be highlighted, however, that it is possible to associate for AADL model edition and XMI generation. We con-
a thread with several operation modes. sider AADL together with its behavioral annex.
2) Model Verification: It is a modeler decision whether • Translation of AADL XMI models to Fiacre [1].
he wants to perform further refinements (as discussed in the • Translation of Fiacre to the timed transition system (TTS)
previous subsection) or to verify the behavior of the current input format of Tina toolbox.
model. In order to make the model verification it is necessary • Translation to an untimed automaton via an LTL-
to provide the abstract behavior of each thread that belongs to preserving time abstraction.
the AADL model. Afterwards designer should define the set of • Verification of LTL properties using the Selt tool from
properties of interest to be verified and perform the verification the Tina toolbox.
process. Such process is detailed in the next section and, for
A. Verification Tools
the remainder of this section, we conclude the presentation of
the proposed methodology. TINA is a software environment to edit and analyze Petri
nets, Time Petri nets, Time Transition Systems, and also
E. Time-Related Levels extension of these nets handling data, priorities and temporal
To verify the real-time properties of the model it is necessary preemption. Beside the usual editing and analysis facilities of
to make the Software/Hardware Mapping (level-5). After this similar environments, the essential components of the toolbox
step, every thread must be associated with a specific processor. are a state space abstraction tool (also called Tina) and a model
The hardware architecture must have at least one processor. checking tool (selt). Detailed information about the toolbox
Thereby, in the Real-Time Properties Refinement (level-6), capabilities can be found in [3].
the designer can add additional timing information in the TINA offers various abstract state space constructions that
AADL model to be further verified. Such information must preserve specific classes of properties of the state spaces of

334
 nets, like absence of deadlocks, linear time temporal prop- handled by the translator to generate a specific deadlock
erties, or bisimilarity. For untimed systems, abstract state if the capacity of the input buffer is exceeded.
spaces help to prevent combinatorial explosion. For timed 2) Real-time observers: Some properties such as bounded
systems, TINA provides various abstractions based on state response time can be expressed using AADL threads acting as
classes, preserving reachability properties, linear properties or real-time observers. The component to be checked is linked
branching properties. to an observer which plays the role of its environment and
State space abstractions are provided in various formats checks its responses.
suitable for existing model checkers. The TINA toolbox also For example, properties of the maneuver component of the
provides a native model checker, selt. Selt allows one to check parking can be verified by specifying an environment as the
more specific properties than the general ones (boundedness, following. It checks that the highSpeed signal is emitted one
deadlocks, liveness) already checked by the state space genera- period (fixed here at 10ms) after the speed becomes non zero.
tion tool. Selt implements an extension of linear time temporal Otherwise, the err state would be reached. It also checks
logic known as State/Event LTL [5], a logic supporting both that the abort signal is sent if the wheels are moved. The
state and transition properties. The modeling framework con- selt model checker is used to show that the err state is
sists of Kripke transition systems (labeled Kripke structures, unreachable.
the state class graph in our case), which are directed graphs
in which states are labeled with atomic propositions and t h r e a d i m p l e m e n t a t i o n E n v i r o n m e n t T h r e a d . imp
annex b e h a v i o r s p e c i f i c a t i o n {∗∗
transitions are labeled with actions. states
State/Event-LTL formulas are interpreted over the compu- s0 : i n i t i a l complete s t a t e ;
tation paths of the model. They may express a wide range of s1 , s2 , e r r : c o m p l e t e s t a t e ;
state and/or transition properties. Some typical formulas are transitions
the following (a formula evaluates to true if it does so on all s 0 −]→[ s0 { speed ! ( 0 ) ; r a n g l e ! ( 0 ) ; } ;
s 0 −[f i n i s h e d ?]→ s 0 ;
computation paths, X, F, G and U are LTL modalities, p, q s 0 −]→[ s1 { speed ! ( 1 0 ) ; } ;
are formulas): s 0 −]→[ s 2 { wheelMoved ! ; } ;
p p holds at the start s 1 −[h i g h S p e e d ?]→ s 0 ;
X p p holds at the next step (next) −− d e t e c t e d i n l e s s t h a n t h e p e r i o d
s 1 −[on h i g h S p e e d ’ c o u n t = 0]→ e r r ;
G p p holds all along the path (globally) s 2 −[a b o r t ?]→ s 0 ;
F p p holds in a future step (eventually) s 2 −[on a b o r t ’ c o u n t =0]→ e r r ;
p U q p holds until q holds (until) and q holds eventually. ∗∗};
end E n v i r o n m e n t T h r e a d . imp ;
We also use the weak until operator W. p W q holds until q
holds. It is not mandatory that q eventually happens. Remark Response time information could be added to the
Real-time properties, like those expressed in so called AADL model as properties of flow specifications and thus
“timed temporal logics”, are checked using the standard tech- be implicitly checked. However, this is not easy if response
nique of observers, encoding such properties into reachability time is greater than the minimum period of the input signal.
properties. The technique is applicable to a large class of Here, our observer supposes that speed does not change while
real-time properties and can be used to analyze most of the waiting for the highSpeed signal.
“timeliness” requirements found in practice. 3) Linear time Temporal Logic: Temporal properties can be
checked on the closed system. They can be expressed in linear
B. Properties Verification
temporal logic (LTL) and passed to the selt tool. Atomic
Currently, we support the verification of three kinds of properties are either event properties or state properties. For
properties: (i) implicit properties taken into account by the example:
translator and leading to deadlock when not satisfied; (ii) user • If the speed is too high, the interface cannot get the
properties specified through AADL real-time observers; and found message while the search has not been restarted.
(iii) properties specified directly in linear temporal logic.
1) Implicit properties: For the moment, two implicit prop-  (highSpeed ⇒ (¬found W startSearch))
erties are taken into account by the translator:
• Schedulability: threads are scheduled using a fixed prior- This property is in fact not satisfied because taking into
ity protocol with user-specified preemption points. Dead- account the speed information and aborting the process
line events are generated by the translator. If a deadline needs one cycle. We use the hyperperiod event H to
occurs while a thread is still active, a specific deadlock reformulate the property as follows: if the speed is too
is generated. high, starting from the next hyperperiod signal, we cannot
• Buffer overflows: AADL defines the property Over- get the found message unless startSearch has been
flow Handling Protocol which specifies what to do in pushed.
case of overflow. Either the oldest or the newest data is
lost, or the component is erroneous. The latest case is highSpeed ⇒ (¬H U H∧(¬found W startSearch))

335
 • It is possible to park the car, i.e. there exists an execution we have suggested the use of mu-calculus. We intend to study
path leading to a state where the car is parked. It is in future work suitable patterns to enhance the use of such
expressed as a negated property: it is not true that in a logic. Another further direction of this research would be
any execution, finished is never sent. providing a risk analysis to assist the design.

Parking 6|= ¬finished ACKNOWLEGEMENTS

This work was developed with the grant CAPES STIC-
• The car can be parked infinitely often. It is also expressed AmSud 003/07 TAPIOCA : Timing Analysis and Program
as a negated property: Implementation On Complex Architectures and supported by
Parking 6|= ♦¬finished the French AESE project Topcased.
R EFERENCES
4) Modal mu-calculus: There exists some useful properties
that cannot be expressed neither in LTL, nor in CTL. For [1] B. Berthomieu, J.-P. Bodeveix, P. Farail, M. Filali, H. Garavel, P. Gaufil-
let, F. Lang, and F. Vernadat. Fiacre: an intermediate language for model
example, the fact that the user interface can be reinitializable verification in the TOPCASED environment. Proceedings of the 4th Eu-
by the user whatever the system does. To solve this problem, ropean Congress on Embedded Real-Time Software ERTS’08(Toulouse,
it can be expressed in modal mu-calculus using the macro France), January 2008.
[2] B. Berthomieu, F. Peres, and F. Vernadat. Model checking bounded
bellow, where U is the set of user events and ϕ the property prioritized time petri nets. In K. S. Namjoshi, T. Yoneda, T. Higashino,
to be reachable, i.e. the initial state. It defines the set of states and Y. Okamura, editors, ATVA, volume 4762 of Lecture Notes in
from where ϕ is reachable by user events even if non user Computer Science, pages 523–532. Springer, 2007.
[3] B. Berthomieu, P. Ribet, and F. Vernadat. The tool TINA – construction
events are fired as a smallest fixed point (the min operator). of abstract state spaces for petri nets and time petri nets. International
_ Journal of Production Research, 42(14), 2004.
reachable(U, ϕ) = min X | ϕ ∨ ([−U]X ∧ ([e]X ∧ heiX) [4] P. Dissaux and F. Singhoff. Stood and cheddar: Aadl as a pivot language
e∈U for analysing performances of real time architectures. In 4th European
Congress ERTS EMBEDDED REAL TIME SOFTWARE, Jan. 2008.
Such a property can be verified on atemporal models by the [5] S. C. Edmund, E. M. Clarke, N. Sharygina, and N. Sinha. State/event-
muse tool of the Tina toolbox. It must be associated with a based software model checking. In In Integrated Formal Methods, pages
128–147. Springer-Verlag, 2004.
stability property expressing that non-user events do not leave [6] P. Feiler, D. Gluch, and J. Hudak. The architecture analysis &
the initial state. design language (AADL): An introduction. Technical report, Software
Engineering Institute, Carnegie Mellon University, 2006.
It would also be possible to encode a possibly real-time [7] R. B. Franca, J.-P. Bodeveix, M. Filali, J.-F. Rolland, D. Chemouil, and
winning strategy using the AADL behavior annex and check D. Thomas. The AADL behaviour annex – experiments and roadmap. In
that the initial state is reachable using an LTL property over ICECCS ’07: Proceedings of the 12th IEEE International Conference on
Engineering Complex Computer Systems, pages 377–382, Washington,
the generated abstract automaton. In our example, this is very DC, USA, 2007. IEEE Computer Society.
simple because a user command can always be used. [8] J. Håkansson, J. Carlson, A. Monot, P. Pettersson, and D. Slutej.
Component-based design and analysis of embedded systems with uppaal
V. C ONCLUSIONS port. In ATVA ’08: Proceedings of the 6th International Symposium on
Automated Technology for Verification and Analysis, pages 252–257,
In this paper we presented a verification approach and Berlin, Heidelberg, 2008. Springer-Verlag.
the related toolset to design safety critical systems using [9] SAE. Architecture Analysis & Design Language (AADL), AS-5506. SAE
International, 2004.
the AADL language. This work is part of a more general [10] D. Schmidt. Model-driven engineering. IEEE Computer, 39(2), 2006.
project, which also covers the hardware architecture definition [11] S. A. Team. OSATE: An extensible source aadl tool environment. Tech-
in more details, going towards producing safe models for nical report, Software Engineering Institute, Carnegie Mellon University,
2004.
critical applications. It must be highlighted that in the end of [12] Topcased. (toolkit in open-source for critical apllications and systems
the process it is possible to make automatic code generation development). http://www.topcased.org.
from the AADL model for a given platform.
It should be noticed, however, that given the complexity
of the situation, the guarantee of the existence of a correct
solution cannot be asserted. This also applies to the imple-
mentation derived from the generated model. To overcome
this problem, designer feedbacks are necessary and, more
generally, it should be wise to superpose to the software
engineering process risk management.
Currently there is no automated process to transforms the
requirements identified at a high level of abstraction and the
final concrete properties to verify on the final formal model.
This is currently under investigation in our group.
Finally, this study has made us aware of the fact that
linear temporal logic although simple is not rich enough for
expressing some required intuitive properties. In this paper,

336