=Paper=
{{Paper
|id=Vol-1233/paperAll
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1233/proceedings.pdf
|volume=Vol-1233
}}
==None==
https://ceur-ws.org/Vol-1233/proceedings.pdf
ACM/IEEE 17th International Conference on
Model Driven Engineering Languages and Systems
September 28 – October 3, 2014 Valencia (Spain)
ACVI 2014 – Architecture Centric Virtual
Integration Workshop Proceedings
Julien Delange and Peter Feiler
Published on Sept 2014 v1.0
© 2014 for the individual papers by the papers’ authors. Copying permitted for private and academic
purposes. Re-publication of material from this volume requires permission by the copyright owners.
Organizers
Julien Delange (co-chair) Carnegie Mellon Software Engineering Institute
Peter Feiler (co-chair) Carnegie Mellon Software Engineering Institute
Program Committee
Canals Agusti C-S
Etienne Borde TELECOM ParisTech
Matteo Bordin Adacore
Jörgen Hansson University of Skövde, Sweden
Jerome Hugues ISAE
Emilio Insfran Universitat Politcnica de Valncia
Akihito Iwai DENSO Corporation
Alexey Khoroshilov ISPRAS
Bruce Lewis US ARMY
Oleg Sokolsky University of Pennsylvania
Jean-Pierre Talpin INRIA
Steve Vestal Adventium Labs
Bechir Zalila National School of Engineers of Sfax
Table of Contents
Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
Opening Keynote: The Story of AADL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
Peter Feiler
Contract-based specification and analysis of AADL models . . . . . . . . . . . . . . . . . . . . . 4
Ernesto Posse, Juergen Dingel
An Extension for AADL to Model Mixed-criticality Avionic Systems Deployed 14
on IMA architectures with TTEthernet . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Robati Tiyam, Amine El Kouhen, Abdelouahed Gherbi, Sardaouna Hamadou,
John Mullins
A Discrete-event Simulator for Early Validation of Avionics Systems . . . . . . . . . . . 28
Denis Buzdalov, Alexey Khoroshilov
Multi-core Code Generation from Polychronous Programs with Time-Predictable 39
Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali
Modeling Shared-Memory Multiprocessor Systems with AADL . . . . . . . . . . . . . . . . . 49
Stphane Rubini, Pierre Dissaux, Frank Singhoff
Executable AADL: Real-Time Simulation of AADL Models . . . . . . . . . . . . . . . . . . . . 59
Pierre Dissaux, Olivier Marc
Automatic Derivation of AADL Product Architectures in Software Product Line 69
Development . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Javier Gonzalez-Huerta, Silvia Abrahao, Emilio Insfran
Towards an Architecture-Centric Approach dedicated to Model-Based Virtual 79
Integration for Embedded Software Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Huafeng Yu, Jean-Pierre Talpin, Sandeep Shukla, Prachi Joshi, Shin’Ichi Shi-
raishi
Preface
New real-time systems have increasingly complex architectures because of the intricacy of
the multiple interdependent features they have to manage. They must meet new require-
ments of reusability, interoperability, flexibility and portability. These new dimensions
favor the use of an architecture description language that offers a global vision of the sys-
tem, and which is particularly suitable for handling real-time characteristics. Due to the
even more increased complexity of distributed, real-time and embedded systems (DRE),
the need for a model-driven approach is more obvious in this domain than in monolithic RT
systems. The purpose of this workshop is to provide an opportunity to gather researchers
and industrial practitioners to survey existing efforts related to behavior modelling and
model-based analysis of DRE systems.
Cyber-Physical systems (CPS) combine many challenges to meet requirements for
reusability, interoperability, flexibility or dependability. The use of architecture description
language helps to integrate components before implementing the system. Such integra-
tion approach eases system design analysis and implementation, detects design errors and
potential defects before development efforts, avoiding re-engineering costs and making the
system more robust and safe. This first edition of this workshop seeks contributions from
researchers and practitioners interested in architecture-centric methods and their use to
design and analyze systems. The conference topics of interest are:
– Modeling Notations: new languages, inter-operability between languages
– Architecture Centric Analysis Tools
– Virtual Integration Process and Tools
– Definition of extensions for the design of specific systems (e.g. avionics) or support
of a particular analysis (e.g. safety)
– Automatic Code Generation from Models
– Model Transformation
– Model Analysis Methods
– Support of Certification (e.g. DO178C) using Models
– Industrial experiences of use of Model-Based technologies
The Architecture-Centric Virtual Integration Workshop is colocated with the ACM/IEEE
17th International Conference on Model Driven Engineering Languages and Systems.
September 2014 Julien Delange and Peter Feiler
1
Keynote
The Story of AADL
Peter Feiler
Carnegie Mellon Software Engineering Institute
5 years ago the SAE AS-2C subcommittee started to work on the Archi-
tecture Analysis & Design Language (AADL) standard. AADL was targeted to
address issues in mission and safety critical software-reliant systems, aka. Cyber-
physical systems. AADL addresses the increasing challenges of such systems -
the exponential increase in verification related software rework cost. Industry
studies show that 70% of defects are introduced in requirements and architec-
ture design, while 80% are discovered post-unit test. After a short history and
summary of the challenges, the presentation highlights the expressive, analyt-
ical, and auto-generation capabilities of the AADL core language as well as
several of its standardized extensions to address multiple quality dimensions
and do so incrementally at different levels of fidelity. The presentation then
illustrates these capabilities on several realistic industrial examples. The presen-
tation concludes by outlining a four part improvement strategy: architecture-led
requirement specification to improve the quality of requirements, architecture
refinement and incremental virtual system integration to discover issues early,
compositional verification through static analysis to address scalability, and in-
cremental verification and testing throughout the life cycle as assurance evidence.
Peter Feiler is a 29 year veteran and Principal Researcher of the Architecture Prac-
tice (AP) initiative at the Software Engineering Institute (SEI). His current research
interest is in improving the quality of safety-critical software-reliant systems through
architecture-centric virtual system integration and incremental life cycle assurance to
reduce rework and qualification costs. Peter Feiler has been the technical lead and main
author of the SAE Architecture Analysis & Design Language (AADL) standard. He has
a Ph.D. in Computer Science from Carnegie Mellon.
DM-0001610
3
Contract-based specification and analysis of
AADL models?
Ernesto Posse Juergen Dingel
{eposse,dingel}@cs.queensu.ca
School of Computing – Queen’s University
Kingston, Ontario, Canada
Abstract. We describe an approach to the specification, analysis and
verification of AADL models using assume/guarantee behavioural con-
tracts specified with the Property Specification Language (PSL). This
approach aids the development process by 1) supporting the reuse and
replacement of components based on their contracts rather than only
their interface or their implementation and thus reducing the need for
re-engineering; 2) providing early discovery of behavioural inconsistencies
that may pose problems with integration; and 3) allowing an incremen-
tal and flexible application of specification and verification instead of
requiring an all-or-nothing approach. It also helps improving the prod-
uct itself by detecting safety and liveness problems via model-checking.
We also briefly discuss a prototype plug-in for OSATE supporting an
annex language which we call AGCL.
1 Introduction
The development of distributed, real-time embedded systems (DRE) presents
multiple challenges born out of their inherent complexity. In order to address
the complexity of these systems and their design, component-based and model-
driven approaches are often used. Such approaches often rely on modelling and
architecture description languages such as the Architecture Analysis and Design
Language, AADL [6], which provides the means to describe systems in terms of
interacting components and their composition.
Complex patterns of interaction between components pose a challenge to de-
velopers, making it difficult to understand how a system behaves and whether it
satisfies its requirements and behaves correctly, e.g., satisfying safety and live-
ness constraints. In order to provide some relief to the developer, automatic
formal verification techniques such as model-checking can help to analyze a sys-
tem’s behaviour. Nevertheless, formal verification often faces the so-called state-
explosion problem, whereby adding a component multiplies the number of states
in a system, resulting in an exponential growth in the state-space which provides
a challenge to verification techniques and tools.
?
This work was financed in part by Edgewater Computer Systems Inc., Ontario Cen-
tres of Excellence and Connect Canada.
4
An approach to deal with the state-explosion problem is the use of composi-
tional analysis which leverage the structure of the system. In these techniques,
the analysis of a composite system is reduced to the analysis of its parts. A
main advantage of such techniques is that if a single component changes, there
is no need to reanalyze the whole system, only the portion directly affected. This
provides the basis for incremental analysis, which aids development by focusing
verification only on the components on which the developer is working.
A well-known compositional approach is based on assume/guarantee con-
tracts where each component is annotated with a contract consisting of an as-
sumption specifying how the component expects its environment to behave, and
a guarantee specifying the behaviour guaranteed by the component if the as-
sumptions hold. Contract-based specification facilitates integration not only by
making expectations and assurances explicit, but also by ensuring preservation of
correctness when a component with a given contract is replaced by another com-
ponent whose contract conforms to or refines the first. Contract-based analysis
uses the contracts to automatically establish whether a composition of compo-
nents satisfy the contract of the composite component to which they belong.
Most approaches to assume/guarantee analysis (e.g., [3]) limit the scope of
assumptions to component inputs and guarantees to component outputs. Fur-
thermore, in many approaches the form of a contract is of the form “assuming
these inputs, we guarantee these outputs”. These are two big limitations. As-
sumptions and guarantees are supposed to capture behaviour, not just individual
inputs and outputs. Furthermore, both assumptions and guarantees should de-
scribe “conversations” between a component and its environment, with assertions
about information flowing both ways. For example, a component may assume
that whenever it sends a particular output to its environment, the environment
will send back some particular message as input to the component.
In this paper we address these shortcomings by we proposing an AADL an-
nex sub-language for annotating components with assume/guarantee contracts
and a prototype verifier that performs compositional analysis. In this sublan-
guage we use the Property Specification Language, PSL, an IEEE Standard [4]
which allows the specification of behaviour combining the expressive power of
ω-regular expressions and linear temporal logic (LTL), and in which both as-
sumptions and guarantees can refer to inputs and outputs.
Another shortcoming of many formal approaches to analysis is that they usu-
ally require an all-or-nothing commitment on the part of the developer, for ex-
ample requiring a full, formal account of all components’ behaviours. We address
this by supporting the notion of viewpoints. A viewpoint represents a particular
set of requirements distributed across components. The designer may annotate
any given component with several contracts. All contracts sharing the same
name across different components form a viewpoint. For example, the designer
can define some safety viewpoints separately from some liveness viewpoints. This
allows the developer to add contracts and viewpoints as the design progresses.
This notion of viewpoint is simpler than that found in [2] where the developer
is required to explicitly use more complex operators to combine contracts.
5
2 AGCL: a sublanguage for assume/guarantee contracts
Consider the model shown in Figure 1 depicting a system consisting of a client
and a server which itself consists of a front-end or mediator, and a back-end. In
this common pattern, the client may issue requests via a channel req and expects
an answer on channel ans. The front-end of the server receives these requests,
may perform some preprocessing, and delegates the requests to the back-end
server via the internal_req channel. When the back-end server responds on
the internal_ans channel, the front-end may do some post-processing, and
deliver the final answer to the client.
(a) composite (b) server
Fig. 1. A simple client-server architecture with a mediator process.
To annotate components with contracts we need to declare viewpoints, which
is done at the package-level annex library as shown below (using the viewpoint key-
word). The enforce keyword is used to inform the tool which viewpoints should
be analyzed.1
1 package client_server_mediator
2 public
3 annex AGCL {**
4 viewpoint normal_operation;
5 viewpoint alternative_operation;
6 enforce normal_operation;
7 **};
8 -- etc.
9 end client_server_mediator;
1
To keep the presentation of our example simple we show only the annex for each
classifier. We also ommit the specification of the top-level process, the client and
focus on the server only, and we ommit the thread type declarations with ports
which are visible in Figure 1.
6
2.1 Contracts for atomic components (threads)
Figure 2 shows the backend server. Its annex has a behaviour clause describing
the behaviour of the actual implementation, and a contract clause defining
a contract for this component within the normal_operation viewpoint. The
behaviour states that whenever the server receives a request (an in event on the
req port with some signal s1), then it will produce an output on the ans port
in the next state or cycle. The contract in this case has no assumptions and
therefore it is simply true. The guarantee is that whenever the backend receives
a request, it will eventually produce an answer. In this case, it should be fairly
trivial that the beahviour satisfies the contract.
1 thread implementation BackendServer.impl1
2 annex AGCL {**
3 behaviour always (in req:s1 -> next out ans:s2);
4 contract normal_operation
5 assumption TRUE;
6 guarantee always (in req:s1 -> eventually out ans:s2);
7 end normal_operation;
8 **};
9 end BackendServer.impl1;
Fig. 2. Backend server.
Note that the guarantee can talk about both inputs and outputs. The same
is true for assumptions. A guarantee represents an obligation on the component,
whereas an assumption represents an obligation on its environment. Hence, when
a guarantee states an atomic proposition labeled in, it is stating the component’s
obligation to accept or receive an input. When a in atomic proposition appears
in an assumption, the input direction is stated from the point of view of the
component but it actually represents an output obligation from the component’s
environment to the component. Similarly, an out in a guarantee is an obligation
for the component to produce output, whereas an out in an assumption, while
stated from the point of view of the component, actually represents an obligation
on the environment to accept or receive input coming from the component.
Figure 3 shows the frontend. Its behaviour clause specifies that whenever an
external request arrives (from the client), eventually it will reach a state where
it will send a request to the backend (through the internal_req port) and
from that point onwards, whenever it receives an answer from the backend, it
will eventually forward the answer to the client on the external_ans port. The
contract clause specifies as assumption that whenever it sends a request to the
backend server, it will get an answer from it eventually. The guarantee states
that whenever it receives an external request from the client, it will eventually
send an internal request to the backend, and whenever it gets a response from
the backend it will eventually send an answer back to the client. In this case it
7
is less trivial that the behaviour satisfies the contract, but this follows from the
formal semantics of PSL.
In general, for threads, a behaviour B satisfies a contract C = (A, G) with
assumption A and guarantee G, if the formula B ∧ A ⇒ G is valid. Intuitively,
the behaviour and the assumptions must be enough to imply the guarantee. A
(linear) temporal logic formula (including PSL) is valid if it holds in all possi-
ble paths for every possible model. In our case, the premise of this implication
captures the model: the guarantee will be required to be true only on those
models with behaviour B, if the assumption A is true as well. The validity of
PSL formulas can be established with a model-checker (see Section 4).
1 thread implementation Frontend.impl1
2 annex AGCL {**
3 behaviour always (in external_req:s1
4 -> eventually (out internal_req:s1
5 & always (in internal_ans:s2
6 -> eventually out external_ans:s2)));
7 contract normal_operation
8 assumption always (out internal_req:s1
9 -> eventually in internal_ans:s2);
10 guarantee always (in external_req:s1
11 -> eventually out internal_req:s1)
12 & always (in internal_ans:s2
13 -> eventually out external_ans:s2);
14 end normal_operation;
15 **};
16 end Frontend.impl1;
Fig. 3. Server frontend (mediator).
An AGCL annex can contain multiple contracts, which can be verified inde-
pendently. This allows the developer to add contracts as the design progresses,
and define contracts which focus only on particular aspects of interest.
2.2 Contracts for composite components (thread groups)
Figure 4 shows the server combining frontend and backend. In this case, the
thread group does not have a behaviour specification, but only a contract. It’s
contract doesn’t make any assumptions, but it states the guarantee that when-
ever an external request comes from the client, eventually it will answer it.
The problem in this case is the following: if we already know that the subcom-
ponents satisfy their respective contracts, how do we establish if the composition
(the Server.impl1) satisfies its contract? This can be established as follows: let
C1 = (A1 , G1 ) and C2 = (A2 , G2 ) be contracts for the two subcomponents K1
and K2 of a composite component K with contract C = (A, G). Assuming that
K1 satisfies C1 , and K2 satisfies C2 , then K satisfies C if the following two
PSL formulas are valid:
8
def
1. G0 ⇒ G where G0 = G1 ∧ G2 , and
def
2. A ⇒ A0 where A0 = (G2 ⇒ A1 ) ∧ (G1 ⇒ A2 )
Intuitively the first one states that the guarantees of the subcomponents together
must imply the guarantee of the composite. The second one states that the
assumption of the composite must be enough to ensure that 1) the guarantee
of the second must imply the assumption of the first, and 2) the guarantee of
the first component implies the assumption of the second. This is because the
subcomponents may be connected and information may flow both ways between
them, and they are part of each other’s environments: the behaviour of K1 ’s
environment is given by K2 ’s guarantees G2 together with K’s environment given
by A. Hence, A and G2 must imply A1 . Similarly for K2 . To be precise, there
is a little processing that needs to be done on the formulas Gi and Ai , namely
we need to replace port references ocurring in atomic propositions by connector
references so that they refer to the same entity, and we need to flip the direction
(in/out) of those atomic propositions in assumptions for the same reason. For
composite components with n subcomponents, the formulas are generalized to
def def
G0 = G1 ∧ G2 ∧ · · · ∧ Gn and A0 = ∧ni=1 ((∧j6=i Gj ) ⇒ Ai ) respectively. In other
words, the guarantees of all subcomponents must imply the guarantee of the
composition, and the assumption of each subcomponent must be implied by the
guarantees of all other subcomponents. This later requirement can be relaxed
in that it is only needed that the assumption of each subcomponent must be
implied by the guarantees of only those subcomponents connected to it.
In our example, K1 and K2 are Backend.impl1 and Frontend.impl1, and
K is Server.impl1. As before, we establish the validity of the formulas above
with a model-checker (see Section 4), and in this case they happen to be true.
1 thread group implementation Server.impl1
2 subcomponents
3 backend : thread BackendServer.impl1;
4 frontend : thread Frontend.impl1;
5 connections
6 client_req : port req -> frontend.external_req;
7 client_ans : port frontend.external_ans -> ans;
8 server_req : port frontend.internal_req -> backend.req;
9 server_ans : port backend.ans -> frontend.internal_ans;
10 annex AGCL {**
11 contract normal_operation
12 assumption TRUE;
13 guarantee always (in external_req:s1
14 -> eventually out external_ans:s2);
15 end normal_operation;
16 **};
17 end Server.impl1;
Fig. 4. The server.
9
Incremental analysis is supported in the following way: if one component
changes its behaviour, for example the frontend, we only need to check whether
this behaviour satisfies its contract(s). If the result of this analysis is positive,
then there is no need to check other components, or the validity of the composite
formulas, as the contract has not changed and therefore the validity of formulas
1 and 2 is preserved. If the result of this analysis fails, then the developer needs
to either modify the behaviour or the contract for the component in question. If
the contract for a component changes then one must re-analyze that component
(recursively if it is a composite component) and then re-evaluate the implications
G0 ⇒ G and A ⇒ A0 as above, but there is no need to re-analyze components
which have not changed or whose contract has not changed, as they would not
change the validity of these formulas.
2.3 Conformance
Contracts can annotate not only implementations but also types. This opens a
set of closely related problems that need be addressed. The first one is this: if
we have a component implementation K of type T and K has a contract CK =
(AK , GK ) and T is annotated with contract CT = (AT , GT ), how do we know
that CK conforms to CT ? This can be answered by checking two implications:
GK ⇒ GT and AT ⇒ AK . Note that the implication is covariant on guarantees
and contravariant on assumptions. For guarantees, this is because the guarantee
of the type must be a guarantee of any of its implementations: the set of possible
observable behaviours described in GK must be a subset if the set of behaviours
defined by GT , otherwise there would be at least one behaviour guaranteed
by the implementation which does not conform to what the type prescribes. For
assumptions the direction is contravariant because the set of behaviours specified
by AT must be a subset of the set of behaviours specified by AK . If this wasn’t
required, there would be at least one environment behaviour acceptable by AT
but not by AK which would entail that component K would not be able to be
placed in some composite components expecting type T .
The other related problems occur when an implementation extends another
implementation or a type extends a type and both have contracts in the same
viewpoint. These cases can be handled as the above: if K 0 (or T 0 ) has contract
C 0 = (A0 , G0 ) and it extends K (resp. T ) with contract C = (A, G), then con-
formance can be established by checking the validity of G0 ⇒ G and A ⇒ A0 .
3 Relation between PSL sequences and AADL behaviours
A key issue in the use of a specification language or temporal logic such as PSL to
describe behaviours and contracts of AADL models is the correspondance be-
tween the semantics of PSL expressions and the behaviour of the AADL model
which they intend to describe. However, there is a fundamental obstacle: the core
AADL standard doesn’t define a unique way of specifying behaviour. It is up to
annexes or external languages to provide the implementation of a component and
10
therefore it is not possible to define a general correspondance, but only consider
specific types of implementation. One such possibility is to use the behaviour
annex where the implementation is defined as a kind of (hierarchical) state ma-
chine. In this paper we do not assume any particular formalism, annex or type of
implementation. Nevertheless, if behaviour is specified with the behaviour annex
or a similar state-based formalism, we can infer the PSL behaviour specifica-
tion from such state machine using standard transformations (e.g., automata to
regular expression, [7]) and then apply the analysis algorithms as described. Al-
ternatively, we could use the behaviour clause itself to infer an automaton that
implements it, using well-known algorithms that can transform such expressions
and formulas into automata (e.g., [7,8]).
Another way of relating the PSL specifications with the behaviour of AADL
components is to establish a correspondance with the thread semantics defined
by the AADL standard ([6] Subsection 5.4).
A PSL expression is evaluated with respect to a path or sequence of states
labelled with the atomic propositions which are true in such state. Given a
sequence, a PSL expression may hold strongly, hold, be pending or fail. The
expression holds strongly when it contains no bad states, all future obligations
have been met, and the expression holds on all extensions to the sequence. The
expression holds (but does not hold strongly) when it contains no bad states, all
future obligations have been met, and the expression may or may not hold on
any given extension of the path. The expression is pending when it contains no
bad states, but future obligations have not been met, and the expression may
or may not hold on any given extension of the path. Finally, the expression fails
when there is some bad state in the path, future obligations may or may not
have been met and the expression will not hold on any extension of the path.
Additionally, a PSL expression is evaluated with respect to a clock context,
a boolean expression that determines in which cycles the expression is to be
evaluated. The PSL standard does not specify any particular time granularity
or what counts as a cycle or clock tick. It is up to verification tools to decide.
The default context is true so that the expression is evaluated at every cycle.
There are several alternative ways to establish a correspondance between
these paths and cycles and the states of an AADL thread. One possibility, is
to consider a cycle every time the thread is dispatched. This is the natural
choice when the thread is periodic. For aperiodic threads it is also possible to
consider a cycle when the thread is dispatched, but in this case the dispatch
occurs only when an event arrives at a port. For sporadic, timed or hybrid
threads, the cycle would occur either by an event or by the specified period. If
one adopts such convention, then the designer must be aware that the meaning
of the PSL expressions depend on the type of thread. For example, the formula
a ∧ X b asserting that a holds in the current cycle and b holds in the next cycle
means, for a periodic thread, that a holds at the current time t according to the
clock, and b holds at time t+p where p is the thread’s period. On the other hand,
for an aperiodic thread the formula would mean that when an event arrives to
one of the thread’s ports, a holds, and b will hold the next time an event arrives.
11
If we are using the behaviour annex to specify implementations, the choice of
associating cycles with dispatches may lead to the traditional interpretation of
temporal operators with respect to automata, where “next” does really mean the
next state. Since the behaviour annex allows for hierarchical state machines, by
“state” we would mean a state in the flattened state machine, with a particular
assignment of variables to values.
Another possibility is to treat all kinds of threads in the same way, as peri-
odic threads, i.e., assuming that there is an underlying periodic clock, even for
aperiodic threads. In this case, there must be a way for the verification tool to
obtain the current state of a thread at any time t of this underlying clock.
Since there are several possibilities, none of which seems to be a priori any
more fundamental than the others, it is up to the developer to decide which
interpretation of PSL expressions is more suitable.
4 An AGCL analysis tool
We have implemented a prototype of the AGCL annex and the analyses out-
lined in the previous sections as a plugin for OSATE. The tool allows the user to
apply the analyses outlined in this paper, providing results sorted by either view-
point or by component. When the result of a particular analysis fails, a counter-
example is generated by the model checker. Our plug-in uses the NuSMV model-
checker to check the validity of the formulas in question, but the underlying
architecture can easily be extended to support other model-checkers.
A model-checker receives as input a model and a specification (temporal logic
formula) and decides whether the model satisfies the formula or not. A model-
checker can be used to check validity by checking the formula against a universal
model for the formula, this is, a model that contains all possible states and tran-
sitions about which the formula could talk. For example, if a formula contains
three atomic propositions, the universal model has three boolean variables and
therefore eight states, all of which are initial, and all possible transitions be-
tween them. Such universal model contains every possible model of the formula
embedded in it, and therefore every possible path. A linear temporal formula is
valid if it holds in every path of every model, hence, it is valid if it holds in every
path of the universal model. On the other hand, if there is at least one path in
the universal model for which the formula doesn’t hold, then there exists at least
one model for which the formula doesn’t hold and therefore the formula is not
valid.
In terms of complexity, dealing with universal models might appear un-
tractable, but the size of such models depends only on the size of the formulas
(the number of atomic propositions) and not on the size of the state space of the
components themselves. This observation combined with the fact that contracts
don’t need to describe all aspects of behaviour, and can be specified in separate
viewpoints and analyzed independently makes the technique feasable.
12
5 Final remarks
We have sketeched an approach to specify and verify assume/guarantee con-
tracts for AADL components and briefly discussed the kinds of analyses that
can be performed and discussed our prototype implementing these. Given the
space limitations we are unable to provide here the actual algorithms and their
proof of correctness, but these are available in detail as a technical report [5].
The theory behind this work is based on [1] which developed a generic theory of
contract-based reasoning applicable to a wide range of specification formalisms.
In our technical report we extended and specialized that theory to PSL, show-
ing in particular that when using PSL we can compose contracts, the basis
for the compositional analysis. Our approach differs from other compositional
techniques such as [3] in that we do not restrict assumptions to inputs and guar-
antees to outputs. Furthermore, with viewpoints, we make it possible to divide
requirements into sets of smaller contracts, providing the developer with flexi-
bility as well as making automatic verification more feasible. While this work
is preliminary and we have yet to test the plugin on large-scale models, we be-
lieve our early results show promise, and contract-based analysis can provide a
fundamental support to the development process of DRE systems.
References
1. S. S. Bauer, A. David, R. Hennicker, K. G. Larsen, A. Legay, U. Nyman, and
A. Wasowski. Moving from specifications to contracts in component-based design.
In Juan de Lara and Andrea Zisman, editors, Fundamental Approaches to Software
Engineering - 15th International Conference, FASE 2012, Held as Part of the Euro-
pean Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn,
Estonia, March 24 - April 1, 2012. Proceedings, volume 7212 of Lecture Notes in
Computer Science, pages 43–58. Springer, 2012.
2. A. Benveniste, B. Caillaud, A. Ferrari, L. Mangeruca, R. Passerone, and C. Sofronis.
Multiple viewpoint contract-based specification and design. In Frank S. de Boer,
Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, FMCO,
volume 5382 of LNCS, pages 200–225. Springer, 2007.
3. D. D. Cofer, A. Gacek, S. P. Miller, M. W. Whalen, B. LaValley, and L. Sha.
Compositional verification of architectural models. In Alwyn Goodloe and Suzette
Person, editors, NASA Formal Methods, volume 7226 of Lecture Notes in Computer
Science, pages 126–140. Springer, 2012.
4. IEEE Computer Society. IEEE Standard for Property Specification Language
(PSL). IEEE Standard 1850TM -2010, June 2012.
5. E. Posse. Contract-based compositional analysis for reactive sys-
tems in RTEdgeTM , an AADL-based language. Tech. Rep. 2013-
607, School of Computing – Queen’s University, August 2013.
http://research.cs.queensu.ca/TechReports/Reports/2013-607.pdf.
6. SAE International. Architecture Analysis & Design Language (AADL). SAE Stan-
dard AS5506b, 10 September 2012.
7. M. Sipser. Introduction to the Theory of Computation. PWS Publishing, 1997.
8. P. Wolper. The Tableau Method for Temporal Logic: An Overview. Logique et
Analyse, 28(110–111):119–136, June–September 1985.
13
An Extension for AADL to Model
Mixed-criticality Avionic Systems Deployed on
IMA architectures with TTEthernet
Tiyam Robati1 , Amine El Kouhen1 , Abdelouahed Gherbi1 , Sardaouna
Hamadou2 , and John Mullins2
1
Dept. of Software and IT Engineering, École de Technologie Suprieure, Canada
{tiyam.robati.1@ens.etsmtl.ca, amine.elkouhen@etsmtl.ca,
abdelouahed.gherbi@etsmtl.ca}
2
Dept. of Computer and Software Eng, Ecole Polytechnique de Montreal, Canada
{firstname.lastname@polymtl.ca}
Abstract. Integrated modular avionics architectures combined with the
emerging SAE TTEthernet standard provides a strong infrastructure for
the deployment of mixed-critical avionic applications having stringent
safety, reliability and performance requirements. The integration of such
systems is a very complex and challenging engineering task. Therefore, a
model-based approach, which endows system engineers with a method-
ology and the supporting tools to cope with this complexity, is of a
paramount importance. In this research paper, we present an extension
for the standard architecture and analysis modeling language AADL to
enable modeling integrated multi-critical avionic applications deployed
on TTEthernet-based IMA architectures. In particular, we present a
metamodel which extends the core AADL metamodel with concepts and
constraints relevant for this domain, we define the concrete textual syn-
tax for this extension and we outline the implementation of this extension
using the Open Source AADL Tool Environment (OSATE). Finally, we
illustrate our AADL extension using a case study based on the Flight
Management System.
Keywords: AADL, Time-Triggered Ethernet, AFDX, IMA
1 Introduction
On-board avionic systems are safety-critical systems which should meet strict
safety, reliability and performance requirements. These systems have tradition-
ally been engineered using what is called a federated architectures approach,
where each function is designed and deployed to use its exclusive resources. This
approach is however costly in terms of equipments and wiring. The Integrated
Modular Avionics (IMA) architecture is an alternative approach, which is based
a consolidation of resources [22]. This is achieved through resources sharing
between functionalities. With IMA different avionic functions having different
criticality levels (e.g. control functions and comfort functions) share the same
14
hardware resources leading to mixed-criticality systems. Moreover, IMA archi-
tectures are distributed using a communication infrastructure, which should also
be able to meet the same level of safety and performance requirements.
Ethernet is a widely used standard network (IEEE 802.3) which is not only
used as infrastructure for classic office systems but is increasingly supporting
industrial and embedded systems due to the high bandwidths it provides. How-
ever, Ethernet does not meet strict time and safety critical applications. Several
extensions to enhance the predictability of Ethernet have been developed. One
of these extensions is the Avionic Full Duplex AFDX standard ARINC 664 [11].
AFDX is a deterministic real-time extension of Ethernet based on an static
bandwidth scheduling and control using the concept of virtual links. The SAE
standard TTEthernet [3] is the most recent Ethernet extension based on the
time-triggered communication paradigm [14] [19] to achieve bounded latency
and low jitter. A TTEthernet network implements a global time using clock
synchronisation and offers fault isolation mechanisms to manage channel and
nodes failures. TTEthernet integrates three data flow: Time-Triggered (TT) data
flow which is the higher priority traffic; Rate Constrained (RC) traffic, which is
equivalent to AFDX traffic, and Best Effort (BE) traffic. This makes TTEth-
ernet suitable for mixed-criticality applications such as avionic and automotive
applications where highly critical control functions such as a flight management
system cohabit with less critical functions such as an entertainment system.
The focus of this research work is on avionic applications deployed on IMA
architectures interconnected using TTEthernet. The advantages of this infras-
tructure are numerous. First, the IMA modules enable the resource sharing.
Second, the combination of IMA and TTEthernet enables the error isolation
provided not only at the level of the modules through the partitioning but also
the level of the network using different data traffics and the concept of virtual
links. Third, TTEthernet enable the safe integration of data traffics with dif-
ferent performance and reliability requirements. However, these systems are on
the other hand complex and the integration of diverse applications with mixed-
criticality levels having strict real-time requirements is very challenging. In order
to control the complexity of such systems, a model-based approach, which pro-
vides the systems engineers with a methodology and the supporting tools to
accomplish correctly and efficiently this integration, is required. A key element
of such approach is a modeling language which allows the engineers to express
the system at a convenient level of abstraction and to interface with sophisti-
cated formal analysis techniques to verify safety and performance properties of
the system.
AADL is a well-established standard modeling language in the domain of real-
time critical systems. AADL has been extended to support the modeling of IMA
with an Annex ARINC 653 [2]. However, there is no support for AADL to model
the networking of IMA modules through the recent technology TTEthernet.
We present in this paper an extension for AADL to support the modeling of
IMA architectures interconnected using TTEthernet. In particular, we present
a metamodel for the domain of IMA and TTEhernet. We provide a concrete
15
textual syntax based on this metamodel, which enables the system engineers to
describe a full IMA-based avionic systems interconnected with TTEthernet. We
have implemented this extension in the framework of the Open Source AADL
Tools (OSATE2)[5] . We illustrate the expressiveness of this extension through
it application to model a subsystem of the the Flight Management System [18].
This paper is organized as follows: In Section 2, we introduce the concepts
of IMA and the main features of the TTEthernet standard. We describe in
Section 3 the main components of the proposed extension metamodel and discuss
the rational behind its design. We outline the implementation of the proposed
extension in the framework of OSATE in Section 4. We show the application of
the proposed extension with an illustrative example in Section 5. In Section 6,
we succinctly review the most close related research works to ours. We conclude
the paper and outline our ongoing and future research work in Section 7.
2 Background
In order to make this paper as self-contained as possible, we briefly introduce in
this section the main concept of IMA and TTEthernet.
2.1 Integrated Modular Avionic Architecture (IMA)
The main idea underlying the concept of IMA architecture [22] is the sharing of
resources between some functions while ensuring their isolation to prevent any
interference between them. Resource sharing reduces the cost of large volume of
wiring and equipment while the non interference guarantee is required for safety
reasons. The IMA architecture is a modular real-time architecture for avion-
ics systems defined in the standard ARINC653 [12]. Each functionality of the
system is implemented by one or a set of functions distributed across different
modules. A module represents a computing resource hosting many functions.
Functions deployed on the same module may have different criticality levels. For
safety reasons, the functions must be strictly isolated using partitions. The par-
titioning of these functions is two dimensional: spatial partitioning and temporal
partitioning. The spatial partitioning is implemented by assigning statically all
the resources for the partition being executed in a module and no other partition
can have the access to the same resources at the same time. The temporal par-
titioning is rather implemented by allocating a periodic time window dedicated
for the execution of each partition.
2.2 Time-Triggered Ethernet (TTEthernet)
The new SAE Time-Triggered Ethernet standard (TTEthernet) [3] specifies
time-triggered services extending the Ethernet IEEE standard 802.3. TTEther-
net is based on the Time-triggered communication paradigm [13] and therefore
establishes a system-wide time base implemented through a synchronisation of
the clocks of the end systems and switches. This results in bounded latency and
16
low jitter. TTEthernet integrates both time-triggered and event-triggered com-
munication on the same physical network. TTEthernet limits latency and jitter
for time-triggered (TT) traffic, limits latency for rate constrained (RC) traffic,
while simultaneously supporting the best-effort (BE) traffic service of IEEE 802.3
Ethernet. This allows application of Ethernet as a unified networking infrastruc-
ture. It supports therefore the deployment of mixed-criticality applications at
the network level.
3 Metamodel Extending AADL capability to model
TTEthernet
In this section, we present the metamodel for our extention to AADL in order
to support the modeling of TTEthernet, which will henceforth be called the
AADL-TTEthernet metamodel. This meta-model captures the main concepts
and characteristics of the TTEthernet standard. The AADL-TTEthernet meta-
model will enable building a set of tools to perform the design and analysis of
distributed IMA architectures using TTEthernet as communication infrastruc-
ture. We have designed the AADL-TTEthernet metamodel using the Eclipse
Modeling Framework (EMF), which is also used to specify the AADL Core
metamodel. This allows for a seamless integration of the AADL-TTEthernet in
OSATE2 environment [5] in terms of dependencies and embedded Java API.
On the other hand, using the same mechanism (i.e. Ecore) to specify the two
metamodels eases the expression of the domain concepts dependencies and sim-
plifies the navigation between them. This mechanisim also has been used in
other works [17] aim at implementing new annex and extension to AADL. Our
Aadl2 AADLcMeta-Modelc(EMF)
AnnexSubClause NamedElement AnnexSubClausec
javacclass
AadlTTE
TTEthernetAnnex TTEthernetNamedElement TTEthernetAnnex
javacclass
AADL-TTEthernetcMeta-Modelc(EMF)
extends
produces
Fig. 1. AADL-TTEthernet meta-model dependencies
AADL-TTEthernet metamodel describes the structural aspect of a distributed
IMA systems interconnected using TTEthernet and makes explicit all concepts
17
specified by this standard. The EMF framework generates automatically the
Java implementation classes corresponding to the metamodel objects as it is
shown in Figure 1. In order to extend AADL with our metamodel it is required
to attach a TTEthernet model to an AADL component and to link the objects
of our TTEthernet extension with AADL core objects. This is achieved by the
implementation of the OSATE2 extension mechanism, which requires to link the
TTEthernetAnnex concept in our metamodel to the AnnexSubclause concept of
the AADL core as it is shown in Figure 1. This figure shows also how we use
the EMF/Ecore inheritance mechanism to express the dependencies between the
two metamodels. Consequently, a TTEthernetAnnex extends an AnnexSubclause
and an TTEthernetNamedElement extends a NamedElement. In the metamodel,
the TTEthernetAnnex concept, which links as shown in Figure 2 the metamodel
to the AADL core metamodel, represents the overall model of a TTEhernet-
networked IMA system which will undergoes different analysis to verify safety
and performance properties. The global information about the network elements
and the underlying implementation is described in the TTEthernetAnnex con-
cept. The TTEthernetAnnex is composed of the following (Figure 2):
TTEthernetAnnex AnnexSubClause
RfromDaadl2)
0..* connections scheduler 1 processingResources 0..* 0..* channels 1..* domains 0..* virtualLinks
Connection Scheduler ProcessingResource 1 source Channel SynchronizationDomain VirtualLink
RfromDaadl2)
1 destination
NamedElement
TTEthernetNamedElement
RfromDaadl2)
Fig. 2. AADL-TTEthernet meta-model overview
1. The Synchronization domains concept of TTEthernet standard. TTEthernet
supports system-of-system communication by introducing Synchronization
domains and Synchronization priorities as shown in Figure 3. Synchroniza-
tion domains specify independent subsystems with respect to their synchro-
nization. All the resources configured to belong to the same synchronization
domain should synchronize with each other and components belonging to
different synchronization domains in one TTEthernet network do not syn-
chronize their local clocks.
2. The Scheduler is the entity in TTEthernet that is capable of producing
a schedule, which should be compliant with the scheduling constraints of
TTEthernet. These constraints are depicted in figure 3. The scheduler of
TTEthernet request specific constraint which are presented mathematically
18
in [21]. These constraints are mentioned in figure 3 as constraints type which
is related to constraint class.
3. The Processing Resources represent active hardware components in a net-
work. They can be Computing Resources such as Modules (i.e. end systems)
or Networking Resources such as switches as shown in Figure 4. All pro-
cessing resources have features which can be parameters, access to physical
buses, or ports (i.e, interfaces for frames inputs and outputs). A processing
resource can be a synchronization master and can then transmits its local
time to synchronize the whole network as shown in Figure 3. Several process-
ing resources can be aggregated into logical groups called clusters as shown
in Figure 4. A Cluster is associated with one synchronization domain. Each
single cluster can establish and maintain synchronization by itself.
SynchronizationPriority
level<:>
schedules
ConstraintType 1..g
BoundedSwitchMemory
EndToEndTransmission
ApplicationLevel 0..g constraints
DomainSpecific
PathDependent
SimultaneousRelay
Constraint
ContentionFree
ProtocolControlFlow Type<:>
NetworkingResource ComputingResource ProtocolType
protocolX:XProtocolType TTP
AFDX
Switch Module Partition
partitions
0..*
Fig. 4. Processing resources
by the minimum frame interval, called bandwidth allocation gap, and the
maximum frame length.
The Schedulable Resources represents all the elements which are managed using
the network scheduler. These resources can be the partitions hosted by module,
the data transferred through the network (i.e, Frames), the networks commu-
nication channels or the virtual links as shown in Figure 5. A Frame is unit
Schedule SchedulableResource
schedulableResources
0..*
Channel VirtualLink Frame Partition
virtualLink 0..* frames
0..1 frames 0..*
Fig. 5. Schedulable resources
of transmission, a data packet of fixed or variable length, encoded for digital
transmission over a communication link as depicted in Figure 6. Considering its
order of priority, a frame could be Protocol Control Frame (PCF), TT frame,
Rc frame or BE frame.
4 Implementation of the TTEthernet Extension for
AADL
4.1 Textual Syntax for the TTEthernet Extention for AADL
The definition of a textual syntax is provided by a grammar (i.e, a set of rules
which define the composition of a language). In order to translate the textual
syntax to its corresponding model, a lexer, a parser as well as a component for
the semantical analysis (type checking, resolving of references, etc.) are required.
20
Frame <>
PCFFType
lengthw:wInteger
periodw:wInteger ColdStart
multicastw:wBoolean ColdStartAcknowledge
Integration
BestEffortFrame RateConstrainedFrame TimeTriggeredFrame ProtocolControlFrame
transmissionRatew:wInteger offsetw:wInteger typew:wPCFType
Fig. 6. Frame kinds
The backward transformation, from model to text, is provided by an emitter. All
the components can be generated using the grammar ⇐⇒ meta-model mapping
definition [10]. Figure 7 demonstrates the selected framework to define textual
syntax of our extension. It employs the data provided by the mapping definition
used to generate the parser, emitter and an editor for the corresponding language
to the metamodel. This editor can then use the generated parser and emitter
to modify the text and the model. Therefore it is responsible for keeping the
text and the model in sync, e.g., by calling the parser upon any changes on
the text. Based on this mapping definition, several features of the editor can
be generated, such as syntax highlighing, autocompletion or error reporting. To
MappingDDefinition
references references
reads
Legend Grammar TextualDSyntaxDFramework Metamodel
generates
artifact
activeDcomp. GeneratedDTextualDSyntaxDTools
instanceDof
instanceDof
creates/
r/wDaccess
updates
dependency
reads LexerDDDDDDDDDParserDDDDDDAnalyzer
instanceDof
communication
reads reads
TextDArtifact manipulates Editor manipulates
Model
parses
emits Emitter
Fig. 7. General structure of a textual syntax framework
build the textual editor tool for our AADL-TTEthernet extension, we used the
xText framework [8]. It implements the textual syntax according to an extended
BNF. Figure 8 shows an excerpt of this xText grammar. In this xText framework,
the AADL-TTEthernet metamodel concept is mapped to a Java implementation,
where the TTEthernet objects names are used as class names. All attributes are
implemented as private fields and public get- and set- methods. The composition
relationships are realized in the same way as attributes and contribute to the
constructor of the class. All classes support the Visitor pattern [9] to traverse
the abstract syntax along the composition relationships [15].
21
The analyzer module scans the Abstract Syntax Tree (AST) and checks the
semantics of the AADL-TTEthernet model. First, it proceeds to a resolution
phase (e.g, naming resolver), which links TTEthernet objects to their corre-
sponding AADL objects. In order to achieve this phase, we use the visitors (e.g,
java classes) provided by OSATE2 to retrieve AADL objects. For the sake of
the implementation of our AADL-TTEthernet extension, we have developed the
visitors required to navigate through the AADL-TTEthernet AST. This phase
adds information to the AST and makes its use easier.
1 grammar o r g . o s a t e . t t e t h e r n e t . x t e x t . A a d l t t e
2
3 import ” h t t p : / / ca . e s t m t l . a a d l 2 / a a d l t t e / 1 . 0 ”
4 import ” h t t p : / / a a d l . i n f o /AADL/ 2 . 0 ” as a a d l 2
5 import ” h t t p : / /www. e c l i p s e . o r g / emf /2002/ Ecore ” as e c o r e
6
7 P a r t i t i o n returns P a r t i t i o n :
8 ’ P a r t i t i o n ’ name = ID
9 ’ f r a m e s ’ ’ : ’ f r a m e s += Frame∗
10 ’ end ’ ID ’ ; ’ ;
11 Frame :
12 RateConstrainedFrame | TimeTriggeredFrame | B e s t E f f o r t F r a m e
| ProtocolControlFrame
13 ;
14 S y n c h r o n i z a t i o n P r i o r i t y returns S y n c h r o n i z a t i o n P r i o r i t y :
15 ’ S y n c h r o n i z a t i o n P r i o r i t y ’ name = ID
16 ’ level ’ level = Integer ’ ; ’
17 ’ end ’ ID ’ ; ’ ;
Fig. 8. xText grammar overview for AADL-TTEthernet
4.2 Integration of the AADL-TTEthernet Compiler to OSATE2
Sublanguages are included into AADL specifications as annex subclauses. The
latter may be inserted into AADL component types and AADL component im-
plementations of an AADL model. OSATE2 currently provides four extension
points that can be used to integrate a sublanguage into the tool environment.
These extension points are designed to support parsing, unparsing, name reso-
lution / semantic checking, and instantiation of annex models. From the AADL-
TTEthernet EMF meta-model in the EMF framework, we generate the AADL-
TTEthernet builder factory to build and manipulate TTEthernet objects used in
the compiler. The compiler plug-in contains two modules: a parser/lexer and an
analyzer. The integration of the AADL-TTEthernet plug-in is a two-steps pro-
cess. First, we link the AADL-TTEthernet plug-in to the OSATE2 annex plug-in
22
using the Eclipse extension points mechanism. The annex plug-in defines exten-
sion points which allow to plug-ins be connected together as depicted in Figure
9. Second, we have to register our parser in the OSATE2 annex registry. As the
AADL-TTEthernet metamodel becomes a part of the AADL description and
the AADL-TTEthernet textual syntax tool is connected to OSATE2 registry,
the AADL-TTEthernet plug-in is directly integrated and driven by OSATE2.
Legend
AADL-TTEthernet2Metamodel
plug-in
active2comp.
extends
Unparser222222Parser222222Analyzer
compliant
extension
AADL-TTEthernet
Unparser222222Parser222222Analyzer
AADL22Metamodel
OSATE2
Fig. 9. AADL-TTEthernet plug-in integrated to OSATE2
5 An Example: A Model of a Subsystem of the Flight
Management System
In this section, we illustrate the modeling of a distributed IMA system based on
TTEthernet as a communication network using our extension for AADL. In or-
der to do so, we use as a subsystem of the Flight Management System presented
in [18]. This subsystem controls the display of static navigation information in
the cockpit screens. The structure of the considered FMS subsystem in terms of
modules and the partitions they host is shown in Figure 10. In the original ver-
sion of the system considered in [18], the system is interconnected using AFDX.
In our context, the modules are instead interconnected using TTEthernet. The
AFDX data traffic in the original system corresponds to the RC traffic in the
TTEthernet context. Table 1 shows a subset of the virtual links used in the FMS
subsystem with their corresponding characteristics including the Bandwidth Al-
location Gap (BAG), the sender modules of the VLs and the corresponding
receiver modules. This subsystem can be modeled using our TTEthernet ex-
tension for AADL as follows. The extension is a sub-language for AADL, which
can be included in system implementation of the AADL model of this system.
The concrete textual syntax of AADL-TTEthernet extension provides several
new reserved words, which correspond to the main concepts of the metamodel
described previously, such as module, switch, partition, connection, virtual link,
23
Fig. 10. A Subsystem of the Flight Management System
Virtual Link Source Destination BAG Direction
V L1 KU1 F M1 , F M2 32 {S1 , S2 } , {S1 , S3 }
V L2 KU2 F M1 , F M2 32 {S1 , S2 } , {S1 , S3 }
V L3 F M1 M F D1 8 {S2 , S1 }
Table 1. Virtual Links details
Time-triggered frame, Rate Constraint frame and Best Effort frame. An excerpt
of the model of the FMS subsystem using our AADL-TTEthernet is shown in
Figure 11. The full specification of the model can be downloaded at [20].
6 Related Work
AADL presents two extension mechanisms, namely the property sets and the
sublangues (i.e. annex). Several AADL extensions based on these mechanisms
are now standardized as official annexes. These include the Data modeling annex,
ARINC653 annex, the AADL Behavor Annex [2] , and Error Model Annex [1].
In addition, some research work have focused on extending the language using
these extension mechanisms or investigating alternative ways. The most close
research works to ours are reported in [7] and [17] . J. Delange et al. [7] present
an approach based on AADL, which covers the the modeling, verification and
implementation of ARINC653 systems. The authors describe in the work the
modeling guidelines elaborated in the ARINC653 annex of the AADL standard.
This approach is supported by a tool chain composed of Ocarina AADL toolsuite,
AADL/ARINC653 runtime POK and Cheddar scheduling tool. G Lasnier et al.
[17] present an implementation of the AADL behavior annex as an extension
plug-in to the OSATE 2. We have implemented our AADL TTEthernet extension
using similar techniques. M. lafaye et al. [16] define a modeling approach based
24
Fig. 11. Flight Management Subsystem Model using AADL TTEthernet Extension
on AADL and SystemC, which aims at the design and dynamic simulation of a
IMA-based avionics platform. This is component-based approach, which can be
used to dimension the architecture taking into consideration the application to be
deployed while achieving early platform validation. De Niz and Fieler discuss in
[6] how to extend the AADL language to include new features for the separation
of concerns (i.e. Aspects). Based on this research work, it seems that the AADL
extension mechanisms do not support the separation of concerns and new aspect-
like constructs and mechanisms are then investigated. G. Brau et al. present in [4]
a model of a subsystem of Flight Management System using AADL and show how
to establish important parameters in the AADL model including the virtual links
characteristics for instance. To the best of our knowledge, there is no published
research work, which addresses the modeling of the TTEthernet standard as
networking infrastructure for IMA architecture, which is the contribution of this
work.
7 Conclusions and Future Work
The IMA architecture combined with the new SAE standard TTEthernet as
communication infrastructure provide a strong platform for the deployment of
distributed avionic applications. The integration of mixed-criticality applications
on such platforms is a complex and challenging engineering activity. A model-
25
based approach based on the SAE standard architecture language AADL pro-
vides the system engineers with the tools to cope with this complexity. Modeling
TTEthernet infrastructure using AADL is the research gap that we are target-
ing in this work. We have presented in this paper our contribution to address
this issue, which consists in an extension for the standard architecture and anal-
ysis modeling language AADL to enable modeling integrated mixed-criticality
avionic applications deployed on TTEthernet-based IMA architectures. In our
ongoing research work, we aim at formalizing this extension in the form of a new
annex through the SAE standardization process. Moreover, we aim at defining
a formal semantics for our extension to allow transforming the AADL models
built using our extension to models that are suitable for analysis techniques that
can be used to verify relevant safety and performance properties.
References
1. SAE Aerospace. SAE Architecture Analysis and Design Language (AADL) Annex
Volume 1: Annex A: Graphical AADL Notation, Annex C: AADL Meta-Model and
Interchange Formats, Annex D: Language Compliance and Application Program
Interface Annex E: Error Model Annex,AS5506/1, 2011.
2. SAE Aerospace. SAE Architecture Analysis and Design Language (AADL) Annex
Volume 2: Annex B: Data Modeling Annex Annex D: Behavior Model Annex Annex
F: ARINC653 Annex, AS5506/2, 2011.
3. SAE Aerospace. Time-Triggered Ethernet, sae as6802 edition, 2011.
4. Guillaume Brau, Jérôme Hugues, and Nicolas Navet. Refinement of aadl models
using early-stage analysis methods: An avionics example. Technical Report TR-
LASSY-13-06, Laboratory for Advanced Software Systems, 2013.
5. CMU/SEI. Open source aadl tool environment (osatev2). http://www.aadl.info,
2014.
6. Dionisio De Niz and Peter H Feiler. Aspects in the industry standard aadl. In
Proceedings of the 10th international workshop on Aspect-oriented modeling, pages
15–20. ACM, 2007.
7. Julien Delange, Laurent Pautet, Alain Plantec, Mickaël Kerboeuf, Frank Singhoff,
and Fabrice Kordon. Validate, simulate, and implement arinc653 systems using
the aadl. In ACM SIGAda International Conference on Ada, pages 31–44. ACM,
2009.
8. S. Efftinge. Xtext reference documentation.
http://www.eclipse.org/gmt/oaw/doc/4.1/r80xtextReference.pdf, 2006.
9. Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Pat-
terns: Elements of Reusable Object-oriented Software. Addison-Wesley Longman
Publishing Co., Inc., Boston, MA, USA, 1995.
10. Thomas Goldschmidt, Steffen Becker, and Axel Uhl. Classification of concrete
textual syntax mapping approaches. In Ina Schieferdecker and Alan Hartman,
editors, Model Driven Architecture - Foundations and Applications, volume 5095
of Lecture Notes in Computer Science, pages 169–184. Springer Berlin Heidelberg.
11. Aeronautical Radio Incorporated. ARINC Report 664P7-1 Aircraft Data Network,
Part 7, Avionics Full-Duplex Switched Ethernet Network. AEEC, Maryland, USA,
2009.
12. Aeronautical Radio Incorporated. ARINC Report 653P0 Avionics Application Soft-
ware Standard Interface, Part 0, Overview of ARINC 653, 2013.
26
13. G. Kopetz, Hermann; Bauer. The time-triggered architecture. volume vol.91, no.1,
pp.112,126. Proceedings of the IEEE, 2003.
14. Hermann Kopetz and Günther Bauer. The time-triggered architecture. Proceedings
of the IEEE, 91(1):112–126, 2003.
15. Holger Krahn, Bernhard Rumpe, and Steven Vlkel. Integrated definition of ab-
stract and concrete syntax for textual languages. In Gregor Engels, Bill Opdyke,
DouglasC. Schmidt, and Frank Weil, editors, Model Driven Engineering Languages
and Systems, volume 4735 of Lecture Notes in Computer Science, pages 286–300.
Springer Berlin Heidelberg.
16. Michaël Lafaye, David Faura, Marc Gatti, and Laurent Pautet. A new modeling
approach for ima platform early validation. In Proceedings of the 7th International
Workshop on Model-Based Methodologies for Pervasive and Embedded Software,
pages 17–20. ACM, 2010.
17. Gilles Lasnier, Laurent Pautet, Jérôme Hugues, and Lutz Wrage. An implemen-
tation of the behavior annex in the aadl-toolset osate2. In IEEE ICECCS, pages
332–337. IEEE Computer Society, 2011.
18. M.Lauer. Une méthode globale pour la vérification d’exigences temps réel-
application á l’avionique modular intgrée, 2012. Thse de Doctorat, Institut Na-
tional Polytechnique de Toulouse.
19. Roman Obermaisser. Event-triggered and time-triggered control paradigms, vol-
ume 22. Springer, 2004.
20. Tiyam Robati, Amine El Kouhen, and Abdelouahed Gherbi. Flight
management subsystem model using aadl ttethernet extension.
http://profs.etsmtl.ca/agherbi/ima.aadl, 2014.
21. W. Steiner. An evaluation of smt-based schedule synthesis for time-triggered
multi-hop networks. volume vol., no., pp.375,384. Real-Time Systems Symposium
(RTSS), IEEE 31st, 2010.
22. Christopher B Watkins and Randy Walter. Transitioning from federated avionics
architectures to integrated modular avionics. In Digital Avionics Systems Confer-
ence, 2007. DASC’07. IEEE/AIAA 26th, pages 2–A. IEEE, 2007.
27
A discrete-event simulator for early validation of
avionics systems
Denis Buzdalov and Alexey Khoroshilov
{buzdalov,khoroshilov}@ispras.ru
Institute for System Programming of the Russian Academy of Sciences
Moscow, Russia
Abstract. The paper discusses problems arising in development of avion-
ics systems and considers how discrete-event simulation on the base of
architecture models at the early stages of avionics design can help to mit-
igate some of them. A tool for simulation of AADL architecture models
augmented by behavioural specifications is presented and its main design
decisions are discussed.
Keywords: AADL, discrete-event simulation, early validation
1 Introduction
Nowadays avionics is responsible for control of almost all aspects of aircraft
operation. As a result it became a complex system with thousands of sensors
and actuators, and hundreds of software components spread across dozens of
processor modules. Design and development of such system is a big challenge.
And one of the biggest concerns is bugs introduced at the early stages of system
design that are usually very expensive to fix in terms of both time and money
as long as they often impact a number of components.
Let us demonstrate it on a simple example. A typical prerequisite to guar-
antee safety of flight is a real-time reaction on hazardous conditions. That leads
to a number of safety-critical requirements to avionics subsystems that look like
a limitation on time between a moment when a particular sensor reads actual
data and a moment when software processes that data and takes appropriate
actions, e.g. delivers a control command to an actuator or informs a pilot. If
inability to satisfy such requirement is found during integration tests only, it
may have catastrophic consequences for the project. For example, if an unex-
pected latency appears on an overloaded bus, it may require to redesign data
flows between components and to reschedule software partitions that leads to
redo significant part of safety analysis and other verification activities, i.e. to
significant delays and cost increase for the project.
Model-driven system engineering is considered to be the most promising ap-
proach that can help to address this concern. The main idea behind it is to
represent requirements and architecture decisions in form of models, i.e. in more
or less machine-readable form, and then to apply automated verification tech-
niques or even to automatically derive some parts of implementation from these
28
models. The benefits are manifold. First of all, automated analysis and verifica-
tion help to identify as much problems as early as possible. But even if changes
in system design are introduced, models allow to automate impact analysis and
to reduce effort required for repeated verification.
The cornerstone element that enables analysis of various system character-
istics is an architecture model of the system under development. One of mod-
elling languages designed for this purpose is Architecture Analysis and Design
Language (AADL) [11]. The core of AADL allows to describe an architecture of
software-hardware systems. It supports constructions for step-by-step modelling,
refinement and integration. Besides the core language, AADL has different exten-
sions, e.g. for constraints definition, fault handling and behavioural modelling.
AADL has pretty well-defined semantics that allows different tools to be applied
to the same AADL models without significant effort. There are several open
source frameworks supporting creation and analysis of AADL models including
OSATE [1] and MASIW [7,4].
One way to classify the variety of methods of models analysis is to divide
them to analytical and sampling.
Analytical methods allow to get guaranteed estimations of target character-
istics, e.g. the worst-case latency. But the cost of the guarantee is excessively
pessimistic estimations. Another drawback of analytical methods is that each of
them applicable for a particular tasks only. That means that you usually have
to develop a new method to estimate new characteristics or to get estimation in
a little bit different conditions.
Sampling methods do not provide a guarantee in getting of worst-case esti-
mations. But their benefit is that they can provide realistic estimations and can
be much more easily adopted to new conditions and to new target characteristics.
To apply sampling methods to analysis of architecture models a simulation
of the models is required. One of particular kind of simulation — discrete-event
simulation — is considered in this work. This kind of simulation is naturally
suited to the software-hardware systems modelling. In this approach functioning
of the modelled system is represented as a sequence of discrete events. Each
discrete event is an atomic action of one component’s internal state change and
interaction with the outer world and other components. All actions of a single
discrete event are performed in a single moment of the simulation time.
In the paper we consider possible approaches to model behavioural charac-
teristics of architecture models and discuss design decisions of our AADL sim-
ulation engine. Finally we discuss related works and overview possible direction
of further improvements.
2 Modelling
In this section we are considering aspects of modelling which are relevant to the
discrete-event simulation.
29
2.1 How Behaviour is Modelled
Approaches of the discrete-event simulation can differ in the ways of how be-
haviour of model components is modelled.
Depending on the type of the supported behaviour representation, different
simulation and analysis tools can reach different quality of analysis and can run
into different problems during it.
The AADL core does not contain any constructions to model behaviour of
components but the language is easily extendable. That is why let us consider
some ways of how behaviour can be modelled and some properties of these
variants.
Behaviour model can, for example, be represented as a randomized events
flow with given probability characteristics and description of how the component
reacts to external events.
There is also a class of behaviour representations which can be called imper-
ative. For example, behaviour can be represented as either a finite state machine
(FSM), extensions of FSM which work with extended memory state and time, or
some other transition systems. Transition systems can be combined with random-
ized events flows, particularly as FSMs with the probabilistic non-determinism
resolution.
Also the behaviour can be modelled as a program model, when model is a
code in some programming language.
AADL has a standardized extension called Behavior Model annex [10]. This
annex allows to model behaviour of components as an extended timed FSM
interacting with its environment.
Finite state machines (in particular, extended and timed) and specialized
transition systems are usually naturally suitable for describing of a behaviour
of small components. Also, some of such models are studied well and can be
analyzed in some other way except the execution. Such analyses can be used
during the whole system analysis. But still, these models are not well-suited to
modelling of complicated behaviours (in particular, requiring a lot of internal
states and events).
By contrast, program models can be pretty conveniently used for modelling
of very complicated behaviour but they usually can be used only for execution.
From the simulation point of view program models have an additional advan-
tage: any simpler model (e.g. FSM and other transition systems) can be trans-
lated automatically to a program model. It means that if a simulation system
supports program models, simpler model types can be supported automatically.
Randomized events flow which is a really useful representation sometimes,
usually also can be translated to a program model automatically.
2.2 Levels of Abstraction
In this section we consider a model creation process in time. Models get their
details during a long-term process but analysis of the models have to be per-
formed from the very early stages. That is why simulation have to work with
different levels of abstraction.
30
There are two dimensions of abstraction levels of system models to be con-
sidered.
Structural Abstraction The first one is a structural abstraction. Structurally
abstract models contain components, internal structure of which is still going to
be refined in future. For example, such models may define interconnection inter-
faces approximately or consider some complex subcomponents as black boxes.
For example, it may be known that some not fully specified device D is
connected with a processor block P using some data transmission subsystem T
(probably, involving some buses and devices) but it is not decided yet how this
subsystem should be implemented. This means neither the connection interface
of the device D nor the structure of the subsystem T are known.
Behavioural Abstraction Another dimension is a behavioural abstraction that
depends on how accurately behavioural characteristics are modelled.
The behavioural characteristics include the following aspects that can be
described with different accuracy:
– dependencies between input and output;
– influence of a component on the other ones;
– data which components are working with;
– time intervals between events.
A complexity of a behavioural model accurate by both structural and be-
havioural dimensions is more or less the same as a complexity of a behavioural
model abstract by the both dimensions.
If structurally abstract model is built behaviourally accurate, behavioural
models of each component can be very complex both by internal state and by
interaction with its environment.
2.3 Analysis
Support of analysis of models represented in different abstraction levels is essen-
tial for early model verification and validation. In particular, it is really impor-
tant to analyze structurally abstract and behaviourally accurate models as long
as it allows to check single structure refinements and to expose incorrect ones.
To achieve this goal, the way of how behaviour is modelled have to be conve-
nient for describing complex behaviours. It requires a convenient representation
of an internal state and operations with it. This means a simulation system have
to support program models.
But still, simple behaviours in structurally accurate models have to be de-
fined in a convenient way, e.g. using formalisms based on transition systems. So
combination of program models with other representations should be supported
as well.
Another important aspect of usability of a simulation system is familiarity
of a formalism (or at least its paradigm) to the users.
31
Considering the requirements discussed above the best candidate for the
main formalism is an imperative high-level programming language which has
rich libraries of collections, basic algorithms, etc.
3 AADL Simulator in MASIW
MASIW is an AADL-based framework for development and analysis of avion-
ics and other safety critical systems. It contains various tools for development
(text and graphical editors, model importers and generators) and analysis (static
structure constrains analyzer, static AFDX latency analyzer, AFDX network
simulator).
An AADL-model behaviour simulation tool is a welcome addition to such
integrated toolset that enables early verification activities based on dynamic
analysis.
In this section we consider the most interesting aspects of implementation of
such simulation tool.
3.1 Program Models
As we discussed above, support for program behaviour models is an important
feature for a simulator to be used for early validation. But there are several
problems that should be resolved.
What Program to Consider a Behaviour Model The first problem is how
to organize a program model. On the one hand, it seems to be useful to allow all
convenient constructs of programming languages and libraries to be available in
the program model. On the other hand, arbitrary program code cannot represent
a behaviour model of a component because it have to be compatible with model
interface of the component.
Representing behaviour of a component in a system, program models have
to be able to model interaction with other components. In the context of event-
driven simulation, models also have to be able to explicitly work with simulation
time and discrete events.
Specific actions (like sending messages to other components) can be per-
formed using special simulation library which is used by a program model. Time
management can also be organized by such library. For example, there can be
library calls modelling long-term computation or a launch of a long-lasting pro-
cess.
There are other possible approaches to organize interface with simulation
engine. For example, we can interpret the standard output of general executable
code as outgoing commands of a component for model-specific activities like
sending messages to other components and working with the simulation time.
Similarly, standard input of a program can be considered as models-specific
component input like incoming events and data. This approach is used in some
systems in different areas (one of the widely used examples is FUSE [2]) but it
32
seems that this approach does not really fit for describing behaviour models of
components in AADL-models.
As long as we are not limited by any legacy behavioural models we decided
to use the following program models representation. We decided not to limit user
in the internal state representation. Consequently, there is no limits for the code
that works with it.
A simulation library was implemented to manage everything related to discrete-
event nature of the simulation. It is intended to be explicitly used in the program
model code. The library has a plenty of different calls for time management and
for interaction with other components of a system model.
This model representation allows to express everything needed with maxi-
mum freedom in behaviour definition.
Interaction with the Simulation Library The question of how an interface
of the simulation library should be organized is not trivial as well.
Two fundamentally different approaches were considered.
The first one expects a program model of any component to have a single
entry point that handles all simulation events so that only the program model
and not the simulation library determines when external events and data can be
managed. Simulation library just provides an interface for getting information
of new events. This approach can be called synchronous.
The synchronous approach has an advantage that simulation of a model can
be organized in a very optimal way. If two parts of a model do not interact for
some time, they can be simulated independently. Each independent part can
have its own current simulation time.
But the synchronous approach has also a disadvantage: it is not possible
in the general case to model a situation when some component launches long-
lasting process which is provided by another component, and waits for a result
of this process. Necessity of this is known from the practice.
Another approach of interaction with a simulation library can be called asyn-
chronous. In this case a behaviour program model has several entry points which
are in fact callbacks. These callbacks are called at some moment of simulation
time when some specific sort of event arises, e.g. incoming events and data,
different requests of other components and system events like simulation start.
Some of callbacks can return a value. In particular, such callbacks can model
a response of a component to some other component’s request and the mentioned
above launching of long-lasting process that returns a value.
But still, asynchronous approach has its own shortcomings. First of all, sim-
ulation of different parts of a model cannot be performed independently. The
reason of this is the following. Consider a component A having had performed
some state changes at the simulation time t2 > t1 and a component B running
at the simulation time t1 . Consider now that B has requested some information
related to the internal state of A. If simulation engine lets the component A be
simulated independently with B (i.e. including the time t2 ), then the component
B would be unable to get what it needs.
33
One of possible solutions of the problem is to prohibit any component A to
perform any actions at time t > t1 till other components which may request
something from A have finished their execution at t1 . But this approach limits
abilities to parallelize simulation activities.
We can try to solve the problem by storing states of faster running compo-
nents (like A in the example above) at the moments earlier than the current one
(for t < t2 ) accessible by other components (like the state of A at t1 accessible
by B). But this approach still has problems. Consider we are running the com-
ponent A at the t2 storing all states of A at moments of time between t1 and t2 .
But consider that B at the moment t1 can request a change of the state of A
instead of just reading it. It means that we need to discard all stored states at
the moments of time t > t1 and to rerun simulation for A starting at the time
t1 . So, this solution requires a lot of space to store all needed states and a lot of
overhead for these copies management.
As a result, simulation of asynchronous models can be less effective comparing
to synchronous ones regardless how the asynchronous simulation is organized.
Nevertheless, every synchronous behaviour can be represented as an asyn-
chronous one. This means asynchronous simulation libraries are more universal
than synchronous ones. Considering limited abilities of synchronous approach,
asynchronous one is more preferred.
Table 1. Comparison of simulation library approaches
synchronous asynchronous
code representa- linear (like a single function) a set of callbacks
tion
effectiveness easy to parallelize whole model have to be sim-
ulated at a single moment of
simulation time
abilities issues to model long-term pro- no limits
cesses with a returned value
A comparison of synchronous and asynchronous approaches is presented in
the table 1.
Execution Architecture It is important to consider that code execution of a
program model that uses a simulation library have to be suspended at the end
of discrete events to make other components to able to execute their own events
at the same moment of the model time.
One of the simplest ways of organization of such alternating execution is the
usage of a multiple threads. One thread is created for each component and they
are suspended by a simulation system when a function of the end of discrete event
is called. Thread is suspended until new event is raised for the corresponding
component.
34
This approach is practical and pretty easy to implement. But it has some
remarkable drawbacks.
One of them is that a behaviour model writer can easily create a deadlock.
This situation can be preserved by using of some conventions for the behaviour
model code but these conventions cannot be checked automatically by a simu-
lation system.
But the main drawback, as it is seen from practice, is a high load to the
threading subsystem of an operating system which is used to run simulation.
Models can have tens of thousands of active components that requires the same
number of threads. It worked well for Linux-based operating systems, but some
other operating systems cannot manage such load. So, straightforward multi-
thread approach leads to the portability issues.
However, there is another approach to organize program models execution
that does not have drawbacks mentioned above. This approach is called contin-
uations or coroutines in computer science [8,9].
The continuations approach allows to execute several program models in a
single system thread. It means that program model code can be suspended and
then it can be resumed from the very point is was suspended. Such suspension
is performed by a simulation library and no special constructs have to be added
to a program model.
This approach runs into a problem of correct error tracing because control
flow changes vastly. So some effort is required to make error traces and stack
traces looking as if control flow is unchanged.
Some modern and progressive programming languages, that use virtual ma-
chines for program execution, have the continuations approach built in. Classic
languages have libraries implementing this approach but these libraries require
an after-compilation program instrumentation.
Instrumentation of library program models is not a hard problem. But in-
strumentation of user program models can be a problem and it requires special
handling of simulation start.
Fig. 1. Continuations approach on multiple nodes
Nevertheless, applying this approach (fig. 1) allows to increase maximal num-
ber of model components running on a single node to make it operating sys-
35
tem independent. It means that more optimal distribution of model components
across simulation nodes can be achieved in comparison to the multithreaded
multinode approach.
3.2 Behavior Annex
As it was discussed above, support of specialized transition systems as one of
allowed types of behaviour model notations is a welcome feature for a simula-
tion tool aimed to analyze models across various stages of development process.
AADL has a standardized extension for defining such behaviour models called
Behavior Model annex.
AADL Behavior model annex represents behaviour of a component as an
extended finite state machine (FSM) of a specific kind. Actions on transitions
can contain data state changes, interaction with the outer world and time delays.
Transition conditions of such FSMs may depend on data state, external events
generated by other components and time events.
Keeping in mind that our program models use simulation library containing
operations for communication with environment and time, behavior model annex
machines are translated to program models that use the simulation library. This
translation is implemented in the MASIW AADL simulator.
Communication actions of the Behavior Model annex are implemented as
the simulation library calls. Time-related actions are also mapped to the library
calls. State changes (both FSM state and extended data state changes) are im-
plemented naturally in a program model.
3.3 Built-in libraries
MASIW is targeted to the avionics models development and analysis. That is
why during simulation we are running into behavioural aspects of different stan-
dards widely used in avionics.
For instance, the ARINC653 standard is widely used for organizing execu-
tion of software in the avioncs system. It defines both structural and behavioural
aspects of such systems.
Structural information can be represented by special standardized ARINC653
annex of AADL [10] and derived property set.
To ease development of ARINC653-based systems, a standarized behaviours
for processors and other components were implemented. They can be used as
a part of the behavioural model of a developed system. Moreover, library be-
haviours can be a base for user-defined behaviours.
AFDX network standard is a very important and widely used standard in
avionics systems. AADL standard does not have support for modelling properties
related to AFDX networks.
That is why we had to implement our own property set for defining structural
aspects of models using AFDX. It have been used in mentioned above MASIW
parts: static AFDX latency analyzer and AFDX network simulator.
36
We have implemented standardized behaviour of AFDX-specific network
parts (like AFDX switches and network devices) as library behaviours which
can be used in general AADL models simulation in MASIW. Also, some analyz-
ers for these behaviours were implemented such as switches buffers and queues
filling, counts of packets for different routes and links, statistics for packets drops
and reasons of them and etc.
Such behaviour libraries let the model developer to focus on project features
not paying much attention to how to model standard behaviour.
4 Related Works
Marzhin [5] is a proprietary simulator of AADL and AADL Behavior Annex
models that mostly targets to analyze schedulability properties. It is based on
existing multi-agent simulation kernel and it supports simulation of a subset of
AADL and AADL Behavior Annex. The main distinction of MASIW simulator
is support not only for Behavior Annex but for program models as well that
allows to describe and then to simulate much more complex behaviours. Also, it
is pretty easy to configure the MASIW simulator to manage and analyze various
properties of a model.
OSATE framework [1] provides several plugins for model development and
analysis. One of them called ADeS [12] is dedicated to analysis of behavioural
properties using simulation. But unfortunately, its development stopped in 2008
and so this simulator does not support the last version of AADL which really
differs from the supported first version.
AADS [13] is a translator of a subset of AADL with Behavior Annex to
SCoPE [3] representation. SCoPE implements POSIX-based API that enables it
to run appropriate software parts. Also, SystemC [6] is used for hardware simu-
lation. The approach has a lot of benefits. But it is intended to the simulation
of pretty accurate models to get accurate estimations. It seems to be not really
usable on early steps of the model development.
5 Conclusion
MASIW AADL simulator supports simulation for all stages of the model devel-
opment using the most appropriate behaviour model for each stage — program
models for complex behaviours in structurally abstract models and specialized
type of transition system called AADL Behaviour Model annex for other cases.
A conclusion from implementation of the simulator is that having the program
models support, it is quite natural and easy to implement a support of specialized
transition system like AADL Behavior Model annex.
This simulator is integrated to the MASIW framework that supports most
steps of the development and analysis process of AADL-models. This integration
allowed to perform pretty fast and accurate analysis of avionics models (including
models for the early validation).
37
Chosen behaviour model representation as a program model allows to model
errors in models naturally. But support of standardized ways like AADL Error
Model annex is a task for the future.
References
1. OSATE 2, https://wiki.sei.cmu.edu/aadl/index.php/Osate_2
2. Filesystem in Userspace, http://fuse.sourceforge.net/
3. SCoPE, http://www.teisa.unican.es/scope
4. Buzdalov, D., Zelenov, S., Kornykhin, E., Petrenko, A., Strakh, A., Ugnenko, A.,
Khoroshilov, A.: Tools for system design of integrated modular avionics. In: Pro-
ceedings of the Institute for System Programming of RAS. vol. 26, pp. 201–230
(2014)
5. Dissaux, P., Marc, O., Rubini, S., Fotsing, C., Gaudel, V., Singhoff, F., Plantec, A.,
Nguyen-Hong, V., Tran, H.N., et al.: The SMART project: Multi-agent scheduling
simulation of real-time architectures. Proceedings of the ERTSS 2014 conference
(2014)
6. IEEE Std 1666-2011 (Revision of IEEE Std 1666-2005): IEEE Standard for Stan-
dard SystemC Language Reference Manual (Jan 2012)
7. Khoroshilov, A., Albitskiy, D., Koverninskiy, I., Olshanskiy, M., Petrenko, A., Ug-
nenko, A.: AADL-based toolset for IMA system design and integration. In: SAE
2012 Aerospace Electronics and Avionics Systems Conference. vol. 5, pp. 294–299.
SAE Int. (2012)
8. Knuth, D.E.: The Art of Computer Programming vol. 1: Fundamental Algorithms,
pp. 193–200. Addison-Wesley, 3 edn. (1997)
9. Reynolds, J.C.: The discoveries of continuations. Lisp and Symbolic Computation
6(3-4), 233–248 (1993)
10. SAE International: Architecture Analysis & Design Language (AADL)
Annex Volume 2, SAE International standard AS5506/2 (2011),
http://standards.sae.org/as5506/2/
11. SAE International: Architecture Analysis & Design Language (AADL), SAE In-
ternational standard AS5506B (2012), http://standards.sae.org/as5506b/
12. Tilman, J.F., Schyn, A., Sezestre, R.: Simulation of system architectures with
AADL. In: Proceedings of 4th International Congress on Embedded Real-Time
Systems. ERTS 2008 (2008)
13. Varona-Gomez, R., Villar, E.: AADS+: AADL simulation including the behavioral
annex. In: Proceedings of the 2010 15th IEEE International Conference on Engi-
neering of Complex Computer Systems. pp. 379–384. ICECCS ’10, IEEE Computer
Society, Washington, DC, USA (2010)
38
Multi-core Code Generation from Polychronous
Programs with Time-Predictable Properties
Zhibin Yang, Jean-Paul Bodeveix, and Mamoun Filali
IRIT-CNRS, Université de Toulouse, France
{Zhibin.Yang,bodeveix,filali}@irit.fr
Abstract. Synchronous programming models capture concurrency in
computation quite naturally, especially in its dataflow multi-clock (poly-
chronous) flavor. With the rising importance of multi-core processors in
safety-critical embedded systems or cyber-physical systems (CPS), there
is a growing need for model-driven generation of multi-threaded code
for multi-core systems. This paper proposes a build method of time-
predictable system on multi-core, based on synchronous-model devel-
opment. At the modeling level, the synchronous abstraction allows de-
terministic time semantics. Thus synchronous programming is a good
choice for time-predictable system design. At the compiler level, the
verified compiler from the synchronous language SIGNAL to our inter-
mediate representation (S-CGA, a variant of guarded actions) and to
multi-threaded code, preserves the time predictability. At the platfor-
m level, we propose a time-predictable multi-core architecture model in
AADL (Architecture Analysis and Design Language), and then we map
the multi-threaded code to this model. Therefore, our method integrates
time predictability across several design layers.
Keywords: Synchronous languages, SIGNAL, Guarded actions, Veri-
fied compiler, Multi-core, Time predictability, AADL
1 Introduction
Safety-critical embedded systems or cyber-physical systems (CPS) distinguish
themselves from general purpose computing systems by several characteristics,
such as failure to meet deadlines may cause a catastrophic or at least highly un-
desirable system failure. Time-predictable system design [1, 21, 20] is concerned
with the challenge of building systems in such a way that timing requirements
can be guaranteed from the design. This means we can predict the system timing
statically. With the widespread advent of multi-core processors in this category
of systems, it further aggravates the complexity of timing analysis.
The synchronous abstraction allows deterministic time semantics. Therefore
synchronous programming is a good choice for time-predictable system design.
There are several synchronous languages, such as ESTEREL [5], LUSTRE [12]
and QUARTZ [16] based on the perfect synchrony paradigm, and SIGNAL [4]
based on the polychrony paradigm.
39
An integration infrastructure for different synchronous languages has gained
a lot of interests in recent years [6, 19]. A classical solution is to use an interme-
diate representation. Guarded commands [10], also called asynchronous guarded
actions by J. Brandt et al. [6], are a well-established concept for the descrip-
tion of concurrent systems. In the spirit of the guarded commands, J. Brandt
et al. propose synchronous guarded actions [8] as an intermediate representation
for their QUARTZ compiler. As the name suggests, it follows the synchronous
model. Hence, the behavior (control flow as well as data flow) is basically de-
scribed by sets of guarded actions of the form hγ ⇒ Ai. The boolean condition
γ is called the guard and A is called the action. To support the integration of
synchronous, polychronous and asynchronous models (such as CAOS or SHIM),
they propose an extended intermediate representation, that is clocked guarded
actions [6] where one can declare explicitly a set of clocks. They also show how
clocked guarded actions can be used for verification by symbolic model checking
(SMV) and simulation by SystemC. [7] presents an embedding of polychronous
programs into synchronous ones. The embedding gives us access to the methods
and tools that already exist for synchronous specifications.
Fig. 1. A global view of the relation between our work and related work
For a safety-critical system, it is required that the compiler must be verified
to ensure that the source program semantics is preserved. Our work mainly
focuses on the SIGNAL language. We would like to extract a verified SIGNAL
compiler from a correctness proof developed within the theorem prover Coq
as it has been done in the GENEAUTO project for a part of the SIMULINK
compiler. Our intermediate representation is a variant of clocked guarded actions
(called S-CGA), and currently the target is multi-core code. In [23], we have
already presented the compilation of sequential code and the proof of semantics
preservation of the transformation from the kernel SIGNAL to S-CGA. There
exist several semantics for SIGNAL, such as denotational semantics based on
traces (called trace semantics) [11], denotational semantics based on tags which
puts forward a partial order view of time (called tagged model semantics) [11],
structural operational semantics defining inductively a set of possible transitions
40
[4, 11], etc. In [22], we have studied the equivalence between the trace semantics
and the tagged model semantics, to assert a determined and precise semantics
of the SIGNAL language. The relation between our work and related work is
shown in Fig. 1.
The contribution of this paper is to propose a build method of time-predictable
system on multi-core, based on synchronous-model development. At the model-
ing level, synchronous programming is a good choice for time-predictable system
design. At the compiler level, the verified compiler from the synchronous lan-
guage SIGNAL to our intermediate representation (S-CGA, a variant of guarded
actions) and thus to multi-threaded code, preserves the time predictability. At
the platform level, we propose a time-predictable multi-core architecture model
in AADL (Architecture Analysis and Design Language) [15], and then we map
the multi-threaded code to this model.
The rest of this paper is structured as follows. Section 2 presents the abstract
syntax and the semantics of S-CGA. Section 3 gives the multi-threaded code
generation schema from S-CGA. The time-predictable multi-core architecture
model and the mapping from multi-threaded code to that model are presented
in Section 4. Section 5 gives some concluding remarks.
2 S-CGA
In papers such as [6], clocked guarded actions has been defined as a common
representation for synchronous (via synchronous guarded actions), polychronous
and asynchronous (via asynchronous guarded actions) models. It has a multi-
clocked feature. However, in contrast to the SIGNAL language, clocked guarded
actions can evaluate a variable even if its clock does not hold [6] for supporting
the asynchronous view. Since we focus on the polychronous view, we introduce
S-CGA, which is a variant of clocked guarded actions. S-CGA constrains variable
accesses as done by SIGNAL. In this section, we first present the syntax of S-
CGA, and then we give the denotational semantics of S-CGA based on the trace
model.
S-CGA has the same structure as clocked guarded actions, but they have
different semantics.
Definition 1 (S-CGA). A S-CGA system is represented by a set of guarded
actions of the form hγ ⇒ Ai defined over a set of variables X. The Boolean
condition γ is called the guard and A is called the action. Guarded actions can
be of the following forms:
(1) γ ⇒ x = τ (immediate)
(2) γ ⇒ next(x) = τ (delayed)
(3) γ ⇒ assume(σ) (assumption)
where
– the guard γ is a Boolean condition over the variables of X, their respective
clocks (for a variable x ∈ X, we denote its clock x̂), and their respective
initial clocks (denoted init(x̂)),
41
– τ is an expression over X,
– σ is a Boolean expression over the variables of X and their clocks.
An immediate assignment x = τ writes the value of τ immediately to the
variable x. The form (1) implicitly imposes that if γ is defined1 and its value is
true, then x is present and τ is defined. Moreover, init(x̂) exactly holds the first
instant when x is present.
A delayed assignment next(x) = τ evaluates τ in the given instant but
changes the value of the variable x at next time clock x̂ ticks.
The form (3) defines a constraint. It determines a Boolean condition which
has to hold when γ is defined and true. All the execution traces must satisfy this
constraint. Otherwise, they are ignored.
Guarded actions are composed by using the parallel operator k.
An S-CGA example 2 (Example 1) is shown as follows.
true ⇒ assume(yˆ1 = x̂) ẑ ∧ z ⇒ s1 = f (y1 )
init(yˆ1 ) ⇒ y1 = 1 sˆ2 ⇒ s2 = s1 + 1
yˆ1 ⇒ next(y1 ) = x sˆ1 ⇒ assume(sˆ2 )
true ⇒ assume(yˆ2 = x̂) sˆ3 ⇒ assume(ẑ ∧ (not z))
init(yˆ2 ) ⇒ y2 = 2 ẑ ∧ (not z) ⇒ s3 = f (y2 )
yˆ2 ⇒ next(y2 ) = x sˆ4 ⇒ s4 = s3 + 2
true ⇒ assume(x̂ = ẑ) sˆ3 ⇒ assume(sˆ4 )
sˆ1 ⇒ assume(ẑ ∧ z)
Definition 2 (Trace semantics of S-CGA). The trace semantics of a S-
CGA system is defined as a set of traces, that is JSCGAK = {S | ∀scga ∈
SCGA, JscgaKS = true}. We have the following semantics rules,
(1) Jγ ⇒ x = τ KS =
c
∀i ∈ N, JγKS,i ∧ JγKS,i
c
→ (JxK cK ∧ JxKS,i = Jτ KS,i )
∧ Jτ
S,i S,i
(2) Jγ ⇒ next(x) = τ KS =
∀i1 < i2 ∈ N,
c 0 ) ∧ JγK
((∀i0 ∈ N, i1 < i0 < i2 → ¬JxK c
S,i S,i1 ∧ JγKS,i1 )
c
→ (JxK cK
∧ Jτ c
∧ (JxK → JxKS,i = Jτ KS,i ))
S,i1 S,i1 S,i2 2 1
(3) Jγ ⇒ assume(σ)KS =
c
∀i ∈ N, JγK c
S,i ∧ JγKS,i → JσKS,i ∧ JσKS,i
– Rule (1): when γ is present, and the value of γ is true, x and τ are both
present, and the value of x is that of τ .
– Rule (2): when γ is present and the value of γ is true at instant i1 , x and τ
are present at i1 , and if i2 is the next instant where x is present, then the
value of x at i2 is that of τ at instant i1 .
1
An expression is said to be defined if all the variables it contains are present.
2
If two guarded actions update the same variables, the guards must be exclusive.
42
– Rule (3): when γ is present, and the value of γ is true, σ is present and true.
The semantics of S-CGA composition is defined as Jscga1 k scga2 KS =
Jscga1 KS ∧ Jscga2 KS .
In [23], we have already presented the translation rules from the kernel SIG-
NAL to S-CGA, and give the proof of the semantics preservation in Coq.
3 From S-CGA to Multi-threaded Code
The SIGNAL compilation process contains one major analysis called clock cal-
culus from which code generation directly follows. Moreover, the clock calculus
contains several steps, such as the synchronization of each process, i.e., an e-
quation system over clocks; the resolution of the system of clock equations; the
construction of a clock hierarchy on which the automatic code generation strong-
ly relies. Our goal here is to adapt the clock calculus to S-CGA.
Based on the semantics of S-CGA, we can get the equation system over
clocks. The general rules are given as follows.
S-CGA Clock Equations
γ⇒x=τ γ̂ ∧ γ → x̂ ∧ τ̂
γ ⇒ next(x) = τ γ̂ ∧ γ → x̂ ∧ τ̂
γ ⇒ assume(σ) γ̂ ∧ γ → σ̂ ∧ σ
init(x̂) → x̂ (∀x ∈ X)
As a first step, we just consider the endochrony property 3 , namely we can
construct a clock hierarchy based on the resolution of the system of clock equa-
tions. The clock hierarchy of Example 1 (with three clock equivalence classes
C0, C1, and C2) is shown in Fig. 2. In the figure, for instance clk x denotes x̂.
Fig. 2. Clock hierarchy
Moreover, we construct the data-dependency graph (DDG, as shown in Fig.
3) based on the variables reading and writing.
Finally, the multi-threaded code generation is based on both the clock hi-
erarchy and the data dependency graph. First, we map the guarded actions to
threads (i.e. partitions, as shown in Fig. 3). As presented in Fig. 4, we would like
to treat the partition methods generally, this means different partition methods
(such as the vertical way [2] for a concurrent execution, the horizontal way [3]
3
The weak endochrony [14] property will be considered in the future.
43
Fig. 3. Data dependency graph
Fig. 4. The proof idea
for a pipelined execution, etc) don’t affect the proof (here we don’t consider
performance). Second, in each thread, we organize the guarded actions based on
the clock hierarchy. For example, the two guards in Thread2 belong to the same
clock equivalence class, so they are merged inside the same control condition
in the generated code. Third, we add wait/notify synchronization among the
threads. A code fragment of Thread2 is given as follows.
/ ∗ T hread 2 ∗ /
void step()
{
wait(T hread1);
if (C1){
s1 = f (y1 );
s2 = s1 + 1; }
notif y(T hread4);
}
4 Mapping Multi-threaded Code to Multi-core
To allow for static prediction of the system timing, we need time-predictable
processor architectures, thus we know all the architecture details such as the
pipeline and the memory hierarchy to analyze the execution time of programs.
44
Furthermore, the mapping from multi-threaded code to multi-core architectures
should be also static and deterministic.
4.1 A time-predictable multi-core architecture model
With the advent of multi-core architectures, interference between threads on
shared resources further complicates analysis. There are some recommendations
from R. Wilhelm et al. [21, 20], i.e., the better way is to reduce the time inter-
ference: (1) pipeline with static branch prediction and with in-order execution;
(2) separation of caches (instruction and data caches); (3) LRU (Least Recently
Used) cache replacement policy; and (4) access of main memory via a TDMA
(Time Division Multiple Access) scheme. In the EC funded project T-CREST 4 ,
M. Schoeberl et al. [18, 17] propose a new form of organization for the instruc-
tion cache, named method cache (MC), and split data caches (including stack
cache (SC), static data cache (SDC), constants data cache (CDC), and heap al-
located data cache (HC)), to increase the time predictability and to tighten the
WCET. The method cache stores complete methods and cache misses occur only
on method invocation and return. They split the data cache for different data
areas, thus data cache analysis can be performed individually for the different
areas. In our work, heap is avoided to be used because we don’t use dynamic
memory allocation in our multi-threaded code.
Based on these existing work, we would like to model a time-predictable
multi-core architecture in AADL. AADL is an SAE (Society of Automotive
Engineers) architecture description language standard for embedded real-time
systems, and supports several kinds of system analysis such as schedulability
analysis. Moreover, we have already worked on the semantics of different AADL
subsets such as [24]. So we envision how to validate semantically the mapping
from the language level to the architecture level.
Our multi-core architecture model is illustrated in Fig. 5. Inside the core,
we consider static branch prediction and in-order execution in the pipeline. A
simplified instruction set (get instruction, compute, write data, and read data)
is used. As a first step, we just consider a first level cache (i.e. without L2 and
L3). Each core is associated with a method cache, a stack cache, a static data
cache, and a constants data cache. However, the same principle of cache splitting
can be applied to L2 and L3 caches. The extension of the timing analysis for a
cache hierarchy is straight forward. Moreover, TDMA-based resource arbitration
allocates statically-computed slots to the cores.
As proposed by [9], a core is associated with an AADL processor component
and a multi-core processor with an AADL system component containing mul-
tiple AADL processor subcomponents, each one representing a separate core.
This modeling approach provides flexibility: an AADL system can contain other
components to represent cache, and shared bus, etc. For that purpose, we define
specific modeling patterns with new properties (such as Multi Core Properties).
A part of AADL specification is given in Fig. 6.
4
Time-predictable Multi-Core Architecture for Embedded Systems
45
Fig. 5. A time-predictable multi-core architecture model
processor core
features
MC : requires bus access cache_bus ;
SC : requires bus access cache_bus ;
SDC : requires bus access cache_bus ;
CDC : requires bus access cache_bus ;
end core ;
processor implementation core . impl
properties
M u l t i _ C o r e _ P r o p e r t i e s :: B r anc h_Pr edi cti on = > Static ;
M u l t i _ C o r e _ P r o p e r t i e s :: Execution_Order = > In_Order ;
end core . impl ;
system multicore
features
ExtMem : provides bus access shared_bus . impl ;
end multicore ;
system implementatio n multicore . impl
subcomponents
Core1 : processor core . impl { M u l t i _ C o r e _ P r o p e r t i e s :: Core_Id = > 1;};
Core2 : processor core . impl { M u l t i _ C o r e _ P r o p e r t i e s :: Core_Id = > 2;};
Cache_MC1 : memory method_cache . impl { M u l t i _ C o r e _ P r o p e r t i e s :: MC_Id = > 1;};
Cache_MC2 : memory method_cache . impl { M u l t i _ C o r e _ P r o p e r t i e s :: MC_Id = > 2;};
...
SBus : bus shared_bus . impl ;
C2CBus1 : bus cache_bus ;
C2CBus2 : bus cache_bus ;
connections
bus access C2CBus1 -> Core1 . MC ;
bus access C2CBus2 -> Core2 . MC ;
bus access SBus -> Cache_MC1 . Cache_Bus ;
bus access SBus -> Cache_MC2 . Cache_Bus ;
...
end multicore . impl ;
Fig. 6. A part of the AADL specification of the time-predictable multi-core architecture
4.2 The mapping method
To preserve the time predictability, we consider static mapping and scheduling.
Take the example shown in the last section. It generates a configuration file
(such as num of threads=4 ) in multi-threaded code generation. Moreover, we
have a manual configuration file for the time-predictable multi-core architecture
46
model, for example num of cores=4. Thus, we can generate a static mapping
and scheduling, for instance:
– Thread1 7→ Core1, Thread2 7→ Core2, Thread3 7→ Core3, and Thread4 7→ Core4.
– Thread1: notify(Thread2), notify(Thread3);
Thread2: wait(Thread1), notify(Thread4);
Thread3: wait(Thread1), notify(Thread4);
Thread4: wait(Thread2), wait(Thread3).
Based on the simplified instruction set (considered in the architecture model),
the multi-core code can be generated. Thanks to the mechanizations such as
method cache, split data caches, TDMA and static scheduling, the execution
time of the multi-core code can be bounded.
5 Conclusion and Future Work
With the widespread advent of multi-core processors in safety-critical embedded
systems or cyber-physical systems (CPS), it further aggravates the complexity of
timing analysis. This paper proposes a build method of time-predictable system
on multi-core, based on synchronous-model development. Our method integrates
time predictability across several design layers, i.e., synchronous programming,
verified compiler, and time-predictable multi-core architecture model. Interac-
tion among cores might also arm software isolation layers, such as the one defined
in ARINC653. Thanks to the existing work such as [9] and [13] on AADL model-
ing on multi-core architectures and their association with ARINC653, we would
like to associate our work with partitioned architectures in the future.
Acknowledgments: This work was supported by the RTRA STAE Foun-
dation in France (http://www.fondation-stae.net/).
References
1. P. Axer, R. Ernst, H. Falk, A. Girault, D. Grund, N. Guan, B. Jonsson, P. Mar-
wedel, J. Reineke, C. Rochange, M. Sebastian, R. V. Hanxleden, R. Wilhelm, and
W. Yi. Building timing predictable embedded systems. ACM Trans. Embed. Com-
put. Syst., 13(4):82:1–82:37, Mar. 2014.
2. D. Baudisch, J. Brandt, and K. Schneider. Multithreaded code from synchronous
programs: Extracting independent threads for OpenMP. DATE ’10, pages 949–952,
2010.
3. D. Baudisch, J. Brandt, and K. Schneider. Multithreaded code from synchronous
programs: Generating software pipelines for OpenMP. In M. Dietrich, editor,
MBMV, pages 11–20. Fraunhofer Verlag, 2010.
4. A. Benveniste, P. L. Guernic, and C. Jacquemot. Synchronous programming with
events and relations: the signal language and its semantics. Science of Computer
Programming, 16:103–149, 1991.
5. F. Boussinot and R. de Simone. The esterel language. Proceedings of the IEEE,
79(9):1293–1304, 1991.
47
6. J. Brandt, M. Gemünde, K. Schneider, S. K. Shukla, and J.-P. Talpin. Repre-
sentation of synchronous, asynchronous, and polychronous components by clocked
guarded actions. Design Automation for Embedded Systems, pages 1–35, 2012.
7. J. Brandt, M. Gemunde, K. Schneider, S. K. Shukla, and J.-P. Talpin. Embedding
polychrony into synchrony. IEEE Trans. Software Eng., 39(7):917–929, 2013.
8. J. Brandt and K. Schneider. Separate translation of synchronous programs to
guarded actions. Internal Report 382/11, Department of Computer Science, Uni-
versity of Kaiserslautern, 2011.
9. J. Delange and P. Feiler. Design and analysis of multi-core architecture for cyber-
physical systems. In 5th Embedded Real Time Software and Systems, ERTS’14,
February 2014.
10. E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of
programs. Commun. ACM, 18(8):453–457, 1975.
11. A. Gamatié. Designing embedded systems with the SIGNAL programming language.
Springer, 2010.
12. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow
programming language lustre. Proceedings of the IEEE, 79(9):1305–1320, 1991.
13. J. Hugues. AADLib, a library of reusable AADL models. In SAE Aerotech 2013
Congress & Exhibition (Montreal, Canada), September 2013.
14. D. Potop-Butucaru, B. Caillaud, and A. Benveniste. Concurrency in synchronous
systems. Formal Methods in System Design, 28(2):111–130, 2006.
15. SAE. AS5506A: Architecture Analysis and Design Language (AADL) Version 2.0.
2009.
16. K. Schneider. The synchronous programming language quartz. Internal report,
Department of Computer Science, University of Kaiserslautern, Germany, 2010.
17. M. Schoeberl. A time predictable instruction cache for a Java processor. In
R. Meersman, Z. Tari, and A. Corsaro, editors, On the Move to Meaningful In-
ternet Systems 2004: OTM 2004 Workshops, volume 3292 of Lecture Notes in
Computer Science, pages 371–382. Springer, 2004.
18. M. Schoeberl, B. Huber, and W. Puffitsch. Data cache organization for accurate
timing analysis. Real-Time Systems, 49(1):1–28, 2013.
19. J.-P. Talpin, J. Brandt, M. Gemünde, K. Schneider, and S. Shukla. Constructive
polychronous systems. In Logical Foundations of Computer Science, volume 7734
of Lecture Notes in Computer Science, pages 335–349. Springer, 2013.
20. L. Thiele and R. Wilhelm. Design for timing predictability. Real-Time Syst.,
28(2-3):157–177, Nov. 2004.
21. R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley,
G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschn-
er, J. Staschulat, and P. Stenström. The worst-case execution-time problem:
Overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst.,
7(3):36:1–36:53, May 2008.
22. Z. Yang, J.-P. Bodeveix, and M. Filali. A comparative study of two formal se-
mantics of the SIGNAL language. Frontiers of Computer Science, 7(5):673–693,
2013.
23. Z. Yang, J.-P. Bodeveix, M. Filali, H. Kai, and D. Ma. A verified transformation:
From polychronous programs to a variant of clocked guarded actions. In Inter-
national Workshop on Software and Compilers for Embedded Systems (SCOPES),
SCOPES ’14, pages 128–137. ACM, 2014.
24. Z. Yang, K. Hu, D. Ma, J.-P. Bodeveix, L. Pi, and J.-P. Talpin. From AADL
to timed abstract state machines: A verified model transformation. Journal of
Systems and Software, 93:42–68, 2014.
48
Modeling Shared-Memory Multiprocessor
Systems with AADL
Stéphane Rubini1 , Pierre Dissaux2 , and Frank Singhoff1
1
Université de Bretagne Occidentale, UMR 6285, Lab-STICC, Brest, France
2
Ellidiss Technlogies, Brest, France
{stephane.rubini,frank.singhoff}@univ-brest.fr
pierre.dissaux@ellidiss.com
Abstract. Multiprocessor chips are now commonly supplied by IC man-
ufacturers. Real-time applications based on this kind of execution plat-
forms are difficult to develop for many reasons: complexity, design space,
unpredictability, ... The allocation of the multiple hardware resources to
the software entities could have a great impact on the final result.
Then, if the interest to represent the set of hardware computing resources
inside an architectural model is obvious, we argue that other hardware
elements like shared buses or memory hierarchies must be included in the
models if analyze of the timing behavior is expected to be performed.
This article gives guidelines to represent, with AADL, shared-memory
multiprocessing systems and their memory hierarchies while keeping a
high-level model of the hardware architecture.
Keywords: Multiprocessor, Architecture Description Language, Mem-
ory Hierarchy
Introduction
The growth potential for computing power supplied by general purpose mono-
processor (GPU) systems, is quite decreasing. New gains are related to complex
hardware structures and to very advanced fabrication technologies. Especially
in the embedded system context, the additional power consumption to paid for
increasing the instruction rate is high.
Today, the main answer to that problem is to multiply the number of process-
ing units in VLSI chips. Less aggressive internal core designs allow for increasing
the hardware efficiency and reducing the thermal problems (hot spots).
Moreover, as the execution units are multiple, it becomes possible to special-
ize some of them for dedicated usages. As an example, System-On-Chips like TI
OMAPs include multiples GPUs, a DSP and an image processing unit.
These Programmable Heterogeneous Multiprocessors (PHMs) are now exe-
cution platforms that the designers must consider when they develop new prod-
ucts. The focus should not be only on the individual processing units, but on
the whole hardware system. An early knowledge of some non-functional details
of the execution target might be a condition to lead a project to completion.
49
A meaningful performance analysis cannot be conducted without considering a
realistic model of the platform, and the data flow. The challenge is to eliminate
low-level complexity, while the functional or non-functional behaviors remain
close to the reality of the execution environment. The complexity of both the
hardware execution platform and the software application requires that designers
develop high-level models of their systems.
At the same time, system design space exploration requires to apply separation-
of-concerns principles and to distinguish the application model from the architec-
ture platform one. This approach requires that a deployment step maps software
entities onto the hardware resources, statically or dynamically like for instance
in the case of multi-processor scheduling decisions.
The aim of the paper is to propose a level of abstraction of the hardware
for complex shared-memory multi-processor platforms. The section 1 focuses on
the modeling of the processing resources based only on the functional point of
view. The usefulness of such models are tested for the allocation of software
entities on processors through deployment processes. The section 2 develops
these descriptions to include memory hierarchy models, as a major structuring
entities by considering the information flow into the system. In the next section,
we apply those modeling guidelines to a real board. Hence, examples of tools
that work or could work from the modeling level that we propose are given.
Finally, after the description of related works, we conclude on some uncovered
features of the hardware platform that could enrich our modeling guidelines.
1 Resource allocations
When a hardware platform provides multiple execution units, the design process
must include an allocation or a placement strategy. The system model defines
what software entities are assigned to hardware resources. Such assignments may
be done by the mean of a component-containment hierarchy[1]. However AADL
addresses the placement of software on a hardware resources through property
values. Such binding properties form a deployment or an allocation layer in the
model (Fig. 1).
Fig. 1. Layered model
The next two paragraphs illustrate the usage of binding properties for allo-
cating tasks and logical partitions to processors.
50
Processing unit modeling and allocation In multi-processing systems, the pro-
cessing units may be implemented as a separated chip (a processor), or grouped
into a single chip (a core). Finally, the data path of a core or a processor may be
shared to execute concurrently several execution threads (physical threads)[2].
A way to model the system is to enumerate, at the same level, all the pro-
cessing units without consideration of their actual implementation. The model of
the Fig. 2 represents the available processing units of a PHM as arrays of AADL
processors which group together those compatible with the same instruction set.
processor i s a 1 end i s a 1 ;
processor implementation i s a 1 . p r o c end i s a 1 . p r o c ;
processor implementation i s a 1 . c o r e end i s a 1 . c o r e ;
processor implementation i s a 1 . p h y s t h r e a d end i s a 1 . p h y s t h r e a d ;
processor i s a 2 end i s a 2 ;
system mpHardSystem end mpHardSystem ;
system implementation mpHardSystem . impl
subcomponents
PU isa1 : processor i s a 1 [N ] ;
PU isa2 : processor i s a 2 [M] ;
end mpHardSystem . impl ;
Fig. 2. Hardware layer (layer C of Fig. 1): set of processing units. N and M parameters
are constant fixed in the model. isa2 processing unit implementations are not exposed.
The ability of this model to express the allocation of the hardware execution
resources to the software tasks is shown Fig. 3.
A l l o w e d P r o c e s s o r B i n d i n g => ( r e f e r e n c e ( e x e c . PU isa1 ) )
applies to app . t h r s ;
A l l o w e d P r o c e s s o r B i n d i n g => ( r e f e r e n c e ( e x e c . PU isa2 ) )
applies to app . d e d i c a t e d T h r ;
A c t u a l P r o c e s s o r B i n d i n g => ( r e f e r e n c e ( e x e c . PU isa1 [ 1 ] ) ,
r e f e r e n c e ( e x e c . PU isa1 [ 4 ] ) )
applies to app . t h r s [ 2 ] ;
Fig. 3. Software placement (deployment layer B). exec is a component of type
mpHardSystem. app, thrs and dedicatedThr are respectively a process, an array of
threads and a singular thread. thrs[2] may be scheduled on processor units 1 and 4.
As the processing units of an array are homogeneous, all tasks, which are
abstraction of executable codes for an ISA, can be allocated on all of them.
The Allowed Processor Binding property expresses this in the model. Then,
51
thee Actual Processor Binding properties allocate threads onto one or a set
of processors.
Process and partition allocations The same basic principle of allocation schemes
can be applied to processes to define the visibility space of data in the context
of partitioned systems. On the model of the Fig. 4, a process part may be used
by two processing units following the operational mode: in normal mode, only
PU isa1[0] has the right to access it, whereas PU isa1[1] is activated in an
escape state.
system implementation main . redundant
subcomponents
p a r t : process p a r t i t i o n . impl ;
e x e c : system mpHardSystem . impl ;
modes
normal : i n i t i a l mode ;
redundant : mode ;
properties
A l l o w e d P r o c e s s o r B i n d i n g => (
r e f e r e n c e ( e x e c . p r o c U n i t s [ 0 ] ) , r e f e r e n c e ( e x e c . PU isa [ 1 ] )
) applies to p a r t ;
A c t u a l P r o c e s s o r B i n d i n g => ( r e f e r e n c e ( e x e c . PU isa1 [ 0 ] ) )
in modes ( normal ) applies to p a r t ;
A c t u a l P r o c e s s o r B i n d i n g => ( r e f e r e n c e ( e x e c . PU isa1 [ 1 ] ) )
in modes ( redundant ) applies to p a r t ;
end main . redundant ;
Fig. 4. Partition allocations (adapted from the OSATE github examples/core-
examples/multi-core/simple.aadl)
.
In [3], similar allocation scheme is used to model that an AADL virtual pro-
cessor can be hosted by several processing units. An implementation requirement
is that the context can migrate from one processing unit to the other one.
Discussion These examples, i.e. thread allocations in the scheduling field and
partition allocations in the Time-Space Partitioned field, are nearly similar, and
the modeling approach is homogeneous. The deployment layer represents spatial
allocations of the software entities. Temporal intervals where the resources are
actually used are not directly specified; property values assigned to hardware
resources may reference what are the rules to determine the dynamic sharing of
the resource.
At the hardware layer level, the architecture models enumerate the processing
units as a ”flat” structure; they abstract multi-processing architectures as a set
of available implementation-agnostic computing resources.
52
But a major problem with tightly coupled systems like shared-memory multi-
processors comes from the unexpressed sharing of resources at the level of mem-
ory hierarchy. Private cache memories locally separate the information flows near
the processing units, but some parts of the memory hierarchy remain shared be-
tween processors.
The programming model of shared memory multiprocessor platforms allows
communications of data or synchronizations between tasks through memory loca-
tions accesses. However, such a functional explicit sharing is generally secondary
with respect to the sharing of the main memory banks and buses which provides
all the memory words that the program execution requires.
For instance, [4] reports the effect of this resource sharing on a quad core
system (Intel Xeon) for programs of the SPEC2006 benchmark: when a core
executes a synthetic workload, another program running on the other core may
experience an impressive slowdown (up to a slowdown of 200%).
So, an AADL model of shared memory multiprocessor systems must rep-
resent the resources shared by the processing units, especially if the software
specification does not express this sharing as own.
2 Modeling of the memory hierarchy
The memory hierarchies can be complex subsystems, but they mostly expose, to
the software, the interface of a simple memory3 . Hence, designers must take at-
tention to memory hierarchy as its non-functional characteristics are significant.
The guidelines we propose are based on the modeling of the memory hierarchy
as a tree. The terminal nodes represent the processing units and the nodes
abstract the different sub-parts of the memory system. A node of the memory
hierarchy is characterized by the visibility of the memory words it contains; a
node is shared by the same set of processing entities. Data exchanges within the
memory hierarchy follow the paths of the tree.
The following rules may be applied to build the model:
– The memory entities used by a same set of processing units are declared in
a system component, as sub-components. If the memory entity is unique, a
single memory component may be substituted to the system component.
– A system component groups, as sub-components, a memory system, and the
processors and upper level memory systems which share the access to this
memory system.
– For the sake of simplicity, levels of memory hierarchy connected to only one
processor, i.e. processor’s private caches, may be modeled as sub-components
of this processor component.
– The memory system associated to the root node contains at least a memory
component representing the main memory.
3
We consider that the program or the operating system are aware of memory co-
herency problems.
53
When required for analyzing purposes, processors and composite memory
components may detail their internal structure. AADL bus connection features
can be used for that purpose. Information about the behavior of the each memory
entities are given by AADL properties or AADL memory classifiers, for instance
for distinguishing the main memory and the cache levels.
The Fig. 5 shows the modeling of the tree with a hierarchy of AADL compo-
nents. The memories associated to the My sub-system are used or shared by Pj
and Pk processors. Mx is the root memory system, including all the data that
could be addressed in the physical address space. The Mx memory is shared by
the Pi processor and My memory sub-system.
Fig. 5. ”Sharing” tree and its AADL representation.
3 Example
As an example, we apply the guidelines that we propose on the processor of a
VPX board from the company InterfaceConcept. The board VPX3a includes an
Intel core i7, a FPGA Xilinx Kintex7 and an IO Bridge. The core i7 2566LE
processor contains two cores, with an optional activation of multi-threading ca-
pabilities. Three levels of caches constitute the memory hierarchy; level 1 is
composed of two separated caches for instructions and data, level 2 and 3 are
unified ones. Only the level 3 of cache is shared between cores.
The Fig. 6 shows an high level model of the hardware architecture for the
VPX3a board, with emphasis on the processing units and the memory hierarchy.
We assume that the hyper-threading is enabled on the core number two.
The Fig. 7 and 8 show the structure of the memory hierarchy nodes. AADL
bus connections have been used to model the internal hierarchy of the implemen-
tation L1I L1D L2 of mem system. A similar modeling method can be applied to
the other memory systems.
Notice that the cache sharing may change during the design process, even on
a given execution platform. The activation of the multi-threading on a core or
54
system implementation e x e c . IC INT VPX3a
subcomponents
c o r e 1 : processor I n t e l 6 4 . c o r e s i n g l e t h r e a d ;
c o r e 2 : system Intel64 . core dual thread ;
mem : memory mem system . L3 main ;
end e x e c . IC INT VPx3a ;
system implementation I n t e l 6 4 . c o r e d u a l t h r e a d ;
subcomponents
pth1 : processor I n t e l 6 4 . p h y s i c a l t h r e a d ;
pth2 : processor I n t e l 6 4 . p h y s i c a l t h r e a d ;
mem : memory mem system . L1I L1D L2 ;
end I n t e l 6 4 . c o r e d u a l t h r e a d ;
Fig. 6. Model of the processor core i7 2566LE. The root subsystem mem is used directly
by the processor core1 and communicates with the subsystem core2. core2 contains
two physical threads which share the caches L1 and L2.
memory implementation mem system . L3 main
subcomponents
L3cache : memory c a c h e s y s t e m . L3 ;
main : memory shared memory . main ;
end mem system . l 3 m a i n ;
processor implementation I n t e l 6 4 . c o r e s i n g l e t h r e a d
subcomponents
L 1 I c a c h e : memory c a c h e s y s t e m . L1I ;
L1Dcache : memory c a c h e s y s t e m . L1D ;
L2cache : memory c a c h e s y s t e m . L2 ;
end I n t e l 6 4 . c o r e s i n g l e t h r e a d ;
Fig. 7. Structured memory subsystems and processor’s private memory resources. The
L2 cache is private to a core when hyper-threading is not activated. The L3 cache and
the main memory are shared by all the cores, and then are grouped into a unique node.
Fig. 8. Internal structure of the L1I L1D L2 composite memory system.
55
the operating system enabling of a level of cache are examples of modifications
that a designer could do to explore their impact on the system performance.
If such situations may exist, the component hierarchy can contain ”potentially
shared” nodes in the tree, currently used by only one processing unit.
4 Exploitation of the models
As shared-memory multiprocessor platforms become more complex and widely
used, designers of real-time systems need to have access to analysis tools in order
to assess their choices or dimension their systems. Such tools must work from
an architectural model of the execution platform; we think that the modeling
guidelines presented in this article set up a right level of abstraction for this
purpose. These AADL models may be used directly as a tool entry or as a
source for a model transform whether the tool uses a DSL language.
In the sequel, we give examples of tools which are or could able to handle
models compliant with the guidelines proposed in this article.
Scheduling analysis AADL Inspector from Ellidiss Technologies is a lightweight
framework allowing to apply different analysis on AADL models. One of the
analysis tools available with AADL Inspector is Cheddar[5], a scheduling anal-
ysis tool which deals with global multiprocessor scheduling [6]. AADL inspec-
tor transforms the significant AADL entities (components and properties) into
Cheddar-ADL components, in order to control the scheduling analysis [7]. Today,
the model transform does not deal with caches, but Cheddar includes some al-
gorithms to evaluate the cache related preemption cost when instruction caches
are defined in an architecture model [8].
Resource allocations The placement of software entities on hardware resources
may be complex if the number of tasks or virtual processors is high. The use of
optimization methods are sometimes necessary to perform these allocations. For
instance, Cheddar implements basic partitioning algorithms such as RM-Best-
Fit [9] to automatically allocate tasks to processors.
From an AADL model, Allowed Processor Binding can be used to supply
the set of candidate resources and allocation targets (e.g. processors). The results
of partitioning algorithms can then be expressed on the analyzed AADL model
by updating its Actual Processor Binding properties. AADL Inspector will
integrate such a function in its future releases.
Timing analysis In [10], the timing analysis begins by considering the processor
individually and isolated from the other ones. The tool conducts a first compu-
tation of WCET, completed by a cache analysis. A multilevel hierarchy of caches
is considered at this stage; the hierarchy ends with the first level of shared cache.
Then, the analysis assumes that all the possible conflicts happen with the
other processors for the shared cache usage. From this pessimistic analysis, the
worst case response times of all the tasks are computed, and the interferences
56
previously considered are kept if the task’s running times intersect. This process
is recurrently performed upto a fix point is reached.
These examples of tools and analysis show the interest of modeling multi-
processing platform and their memory hierarchy, as many analysis can be con-
ducted from that kind of models.
5 Related works
We describe in this section other modeling approaches used to guide performance
analysis on shared-memory multiprocessor systems.
In [1], Paul proposes a software-on-hardware performance modeling environ-
ment called MESH that founds the modeling and the simulation of single-chip
multiprocessors on a layered approach. A software and a hardware layer respec-
tively include the application threads and the hardware resources. An inter-
mediate layer represents the dynamic mapping of logical threads onto physical
resources through the scheduler decisions and associates thread’s logical events
to physical times. MESH models can include shared resources other than exe-
cution units; the simulation kernel applies time penalties of application threads
when access contentions are detected.
In the context of shared-memory multiprocessors, [11] abstracts the essential
features of the memory hierarchy in a formal model. A 3-tuple hpl , αl , σl i char-
acterizes a level l of memory caches, where pl is the number of cores sharing the
level l caches, αl the number of level l caches, and σl the size of one level l cache.
From the rules of a peddle game, the authors establish lower bounds on mem-
ory traffic between different levels of caches for computations represented as a
directed acyclic graph. Next, they base optimizations on this metric to improve
the implementation of some parallel algorithms.
The modeling of multicore execution platforms with Simulink has been pro-
posed by [12] to optimize the partitioning of tasks in soft real-time systems. The
Simulink model represents the cores, the core communication costs, and the task
set. But, the approach does not take into account the memory hierarchy in the
performance analysis; the behavior issued from the sharing of the caches cannot
be inferred from this model.
Conclusion and future works
This article presents an approach for modeling shared-memory multiprocessor
platforms. Basic entities that we have emphasized in this high-level model, are
the processing units, whereas the way they are implemented, and the different
levels of the memory hierarchy. We expect the architecture of the memory sub-
system is a key feature to perform timing analysis on multi-processing platforms.
The memory hierarchy is not the only challenge in the timing analysis on
multiprocessor platforms. Another topic is the multiplication of interconnection
buses, with various characteristics in term of throughput and latency. Multipro-
cessor SoCs use the capabilities of integrated circuit to implement a lot of buses
57
to connect the different functions available on the chip. One goal devoted to the
architectural models will be to document this structure, and guide tools and
designers to identify potential bottlenecks.
Another problem is to deal with PHMs. SoCs mix different types of proces-
sors, with different speeds or capabilities. How AADL models can represent all
these types of information must be investigated.
Acknowledgments This work is done in the context of the SMART project.
SMART and Cheddar are supported by the Conseil Régional de Bretagne, Bpifrance,
Conseil Général du Finistère and BMO. Cheddar is also supported by Ellidiss
Technologies, EGIDE/PESSOA n. 27380SA and Thales TCS.
References
1. J. M. Paul, D. E. Thomas, and A. S. Cassidy, “High-level modeling and simula-
tion of single-chip programmable heterogeneous multiprocessors,” ACM Trans. on
Design Automation of Electronic Systems, vol. 10, no. 3, pp. 431–461, 2005.
2. S. Rubini, C. Fotsing, P. Dissaux, F. Singhoff, and H. N. Tran, “Scheduling analysis
from architectural models of embedded multi-processor systems,” ACM SIGBED
Review, vol. 11, no. 1, 2014.
3. J. Delange and P. Feiler, “Design and analysis of multi-core architectures for cyber-
physical systems,” in Proceedings of the 7th European Congress Embedded Real
Time Software and Systems (ERTSS), Toulouse, France, Feb. 2014.
4. V. Babka, “Cache sharing sensitivity of SPEC CPU2006,” Distributed Systems
Research Group, Department of Software Engineering, Tech. Rep., 2009.
5. F. Singhoff, J. Legrand, L. Nana, and L. Marcé, “Cheddar: a Flexible Real-Time
Scheduling Framework,” ACM SIGAda Ada Letters, vol. 24, no. 4, Dec. 2004.
6. R. I. Davis and A. Burns, “A survey of hard real-time scheduling for multiprocessor
systems,” ACM Comput. Surv., vol. 43, no. 4, pp. 35:1–35:44, Oct. 2011.
7. P. Dissaux, O. Marc, S. Rubini, C. Fotsing, V. Gaudel, F. Singhoff, and H. N.
Tran, “The SMART project: Multi-agent scheduling simulation of real-time ar-
chitectures,” in Proceedings of the 7th European Congress Embedded Real Time
Software and System (ERTSS), Toulouse, France, Feb. 2014.
8. H. N. Tran, F. Singhoff, S. Rubini, and J. Boukhobza, “Instruction cache in
hard real-time systems: modeling and integration in scheduling analysis tools with
AADL,” in Proceedings of the 12th IEEE/IFIP International Conference on Em-
bedded and Ubiquitous Computing (EUC 14), Milan, Italy, August 2014.
9. Y. Oh and S. H. Son, “Tight performance bounds of heuristics for a real-time
scheduling problem,” Technical Report CS93-24, University of Virginia., 1993.
10. S. Chattopadhyay, A. Roychoudhury, and T. Mitra, “Modeling shared cache and
bus in multi-cores for timing analysis,” in Proceedings of the 13th ACM Interna-
tional Workshop on Software & Compilers for Embedded Systems, 2010, pp. 6–15.
11. J. E. Savage and M. Zubair, “A unified model for multicore architectures,” in
Proceedings of the 1st ACM International Forum on Next-generation multicore/-
manycore technologies, 2008, pp. 9–20.
12. J. Feljan, J. Carlson, and T. Seceleanu, “Towards a model-based approach for
allocating tasks to multicore processors,” in Proceedings of the 38th EUROMICRO
Conference on the Software Engineering and Advanced Applications (SEAA), Sep.
2012, pp. 117–124.
58
Executable AADL
Real Time Simulation of AADL Models
Pierre Dissaux1, Olivier Marc2
1
Ellidiss Technologies, Brest, France.
2
Virtualys, Brest, France.
pierre.dissaux@ellidiss.com
olivier.marc@virtualys.com
Abstract. The Architecture Analysis and Design Language (AADL) standard
[2] defines a default runtime semantic for software intensive Real Time sys-
tems. This includes support for multi tasking, network distributed architectures
and Time and Space Partitionning systems. A proper implementation of the
AADL runtime thus allows for the virtual execution of a system at a model le-
vel and contributes to the early verification of critical software applications.
This paper describes an implementation of the AADL runtime by the Marzhin
Multi Agent simulator that is embedded in the AADL Inspector tool [5].
Keywords. AADL, Simulation, Multi Agent
Introduction
The Architecture Analysis and Design Language (AADL) standard defines a default
runtime semantic for software intensive Real Time systems. This includes support for
multi tasking, network distributed architectures and Time and Space Partitionning
systems (TSP). A proper implementation the AADL runtime thus allows for the virtu-
al execution of a system at a model level and contributes to the early verification of
critical software applications in the development life-cycle.
This paper firstly summarizes the definition of the default AADL runtime, then de-
scribes one of its implementations that has been performed to develop the Marzhin
Multi Agent simulator, and finally explains how it can be used in practice within the
AADL Inspector tool.
1 The AADL Runtime
The AADL Language is an international standard of the SAE (AS-5506B) [1]. The
standard defines in particular a default execution model that specifies the way the
various components interact at run-time. This enables a precise timing analysis and
simulation of AADL models.
59
A typical AADL model is composed of one or several execution resources (Proces-
sors) that can communicate via Buses. The software application is composed of one
or several memory address spaces (Processes) that contain concurrent Threads and
shared Data. Various inter-threads communication paradigms are supported.
1.1 Processors
In AADL, the Processor represents the association of a hardware computation re-
source and a scheduler. It must declare a Scheduling_Protocol property whose value
corresponds to one of those that are actually supported by the analysis, simulation or
code generator. Typically supported Scheduling_Protocols are:
• Rate Monotonic protocol (RM), based on the period of the Threads.
• Deadline Monotonic protocol (DM), based on the deadline of the Threads.
• POSIX 1003 (HPF), based on the predefined priority of the Threads.
• ARINC 653, for the static scheduling of partition slots.
In the case of a partitioned system, the Processor computation resource is shared be-
tween several Virtual Processors, each of them being associated with a set of Threads
located in an AADL Process. Virtual Processors must also define their own Schedul-
ing_Protocol property. This is typically what happens when the ARINC 653 Annex of
the AADL standard is used.
1.2 Threads
The default behavior of AADL Threads is specified in the standard by a state-
transition automaton.
Fig. 1. Runtime states for AADL threads
60
A Thread must have a Dispatch_Protocol property that defines when it is ready to
execute. Supported protocols are:
• Periodic: the thread is periodically triggered by a system clock.
• Aperiodic: the thread is triggered upon arrival of an event on one of its ports.
• Sporadic: same as Aperiodic with a minimum inter-arrival time.
• Timed: same as Aperiodic with an additional timeout event.
• Hybrid: the thread is triggered by event ports and the system clock.
• Background: the thread is triggered when the execution resource is free.
Thread interfaces contain Features that are used to implement communication
channels. They can be:
• Data Ports: allows for point to point data exchange
• Event Ports or Event Data Ports: allows for events and message exchange
• Access to shared Data: allows for multi-points data exchange with concurrency
control.
• Access to remote Subprograms: allows for remote subprogram calls.
1.3 Shared Data
One particular way to exchange information between Threads is to let them have ac-
cess to the same shared data. Shared data are represented in AADL by Data subcom-
ponents to which Threads can have access through Data Access Connections.
It is possible to specify critical sections thanks to the AADL Behavior Annex. In
order to ensure mutual exclusion of all the threads accessing a given shared data com-
ponent, a Concurrency_Control_Protocol property can be set. A typical value for this
property is Priority_Ceiling_Protocol (PCP).
1.4 AADL Behavior Annex
The core definition of AADL deals with the architectural description of the system. It
specifies which components are instantiated and how they are connected and bound
together. The functional activity of Threads or Subprograms is summarized by a
Compute_Execution_Time property that must be given with its Min and Max values.
The Max value of this property thus corresponds to the usual WCET (Worst Case
Execution Time) that is used for scheduling analysis.
However, in order to perform precise timing analysis or simulations, it is necessary
to provide a more detailed description of the functional behavior of Threads and Sub-
programs. The AADL Behavior Annex is an action language that can be used to pro-
vide a simplified representation of the sequential source code structure (pseudo-code).
Examples of actions that can be defined with the AADL Behavior Annex are:
• p! : sending an event on port p (Put_Value and Send_Output)
• d!< : entering a critical section on shared data access d (Get_Resource)
• d!> : leaving a critical section on shared data access d (Release_Resource)
61
• computation(a..b) : use of the processor for a duration between the mini-
mum duration a and the maximum duration b.
2 The Marzhin Simulator
2.1 Principles of the Marzhin Simulation.
Marzhin is a simulation engine that is based on a multi-agent kernel which implies a
random order of activation of the execution units. Each agent can contain one or more
execution units that are invoked randomly during a simulation cycle. The agents can
be specified independently which highly facilitates the initial development and the
maintenance of the simulator. At the execution time, all the agents interact together to
exhibit a global behavior.
Fig. 2. Marzhin random execution principle
Each AADL entity that is managed by Marzhin is modeled by a specialized agent
containing the appropriate execution units to reflect the AADL runtime semantics.
2.2 The Marzhin Data Model.
The Marzhin agents have been defined so that they usually match the corresponding
AADL entities. However, in order to well distinguish them from their AADL equiva-
lent, the name of the Marzhin entities has been capitalized in the next paragraphs:
• THREAD: It has the Dispatch_Protocol, DispatchOffset, DispatchJitter, Period,
Priority, Deadline and Quantum properties. ThePriority is generally determined by
the Scheduling_Protocol property of the PROCESS containing the THREAD. It
maintains a list of instructions to be executed. They can be for example: event sen-
ding or conditional branches. Their different execution states are the same as those
of the AADL Threads as described in section 1.2.
62
• PROCESS: It represents the address space partitionning and the scheduler. In par-
ticular, it thus implements the Scheduling_Protocol that is specified by the AADL
Processor.
• PROCESSOR : it contains PROCESSes and manages their scheduling in case of a
multi-partition system.
2.3 Marzhin Simulation Cycle.
In the case of the execution of THREADs in a PROCESS, the Marzhin simulation
cycles run as follows:
Fig. 3. Marzhin simulation cycle
1. An execution unit starts the simulation cycle of the PROCESS (PB). This allows
for updating the priority of each THREAD at each simulation cycle if needed.
2. Execution in a random order of the election process for all the THREADS (T1, T2,
T3) in order to update their current internal state and determine the highest priority
THREAD that will be executed.
3. An execution unit ends the simulation cycle of the PROCESS (PE) and actually
executes the current instruction of the selected THREAD.
In the case of a PROCESSOR containing several PROCESSes, the execution is de-
fined according to the partition slots. If a partition is not active, all the execution units
of involved entities (PROCESSs, THREADs ...) are disabled and are not taken into
account in the simulation cycle. Only the execution units of the active partition will be
activated during the cycle.
63
Fig. 4. Simulation of a multi-partition system
2.4 About Determinism in Marzhin.
Despites the intrinsic randomness of the Marzhin simulator, a deterministic behavior
is observed most of the times, thanks to the rigorous management of the THREAD
priorities. However, in some situations, it becomes possible to introduce a certain
level of non-determinism that can be useful for analysis purposes.
In the example below, randomness occurs with a Rate Monotonic scheduler when
several threads have the same period and therefore have the same priority:
Simulation configuration:
process1 : RATE_MONOTONIC_PROTOCOL
thread1 : DispatchProtocol=PERIODIC Period=10 WCET=3
thread2 : DispatchProtocol=PERIODIC Period=10 WCET=3
thread3 : DispatchProtocol=PERIODIC Period=10 WCET=3
Simulation trace:
THREAD process1.thread3 __|_|___|._||__|....|__|____|.
THREAD process1.thread2 _|_|_|....|_____||.._|____||..
THREAD process1.thread1 |_____||..___||___|.__|_||....
64
Caption:
. : THREAD_STATE_SUSPENDED
| : THREAD_STATE_RUNNING
_ : THREAD_STATE_READY
During the simulation cycle 0, the random routine selected thread1 whereas it is
thread2 in cycle 1, and so on. It is however possible to control this non-determinism
thanks to the Quantum and Dispatch_Order attributes. Quantum specifies the mini-
mum amount of time the currently selected THREAD will remain active without
being prempted and Dispatch_Order indicates how the current THREAD is selected
within the list (FIRST, LAST or RANDOM). The same example with a Quantum set
at 3 and a Dispatch_Order set at FIRST gives the following simulation trace:
THREAD process1.thread3 ______|||.______|||._____
THREAD process1.thread2 ___|||....___|||....___||
THREAD process1.thread1 |||.......|||.......|||..
The non-determinism of Marzhin can also be beneficial to manage the Global Asyn-
chronism of the simulation environment. It is thus possible to inject events or update
data values in incoming ports connected to remote input devices such as the operator
keyboard, a dedicated dialog box or an active widget in a 3D virtual reality simula-
tion.
The following example shows how an event can dynamically influence the behav-
ior of the simulation. The periodic THREAD thread1 sends an event to the sporadic
THREAD thread2. Such an event could also come from external interface of the
simulator:
process1 : RATE_MONOTONIC_PROTOCOL
thread1 : DispatchProtocol=PERIODIC Period=10 WCET=5
thread2 : DispatchProtocol=SPORADIC Period=4 WCET=3
EVT IN process1.thread2.evt .....................11......
THREAD process1.thread2 ......................|||....
THREAD process1.thread1 .|||||.....|||||.....|___||||
Caption:
1 : number of events in the incoming port queue.
3 Virtual Execution of AADL Models
3.1 AADL Inspector
AADL Inspector is a model processing framework composed of an AADL toolbox
and a customizable set of plugins. The AADL toolbox includes an AADL parser and
the LMP (Logic Model Processing) model processing environment [4] that is based
65
on the use of the prolog language. The LMP engine is used to perform queries on the
AADL declarative and instance models, to implement static model checkers and to
develop model transformations.
For Real Time analysis, two plugins are currently embedded in AADL Inspector:
Cheddar [1] that implements feasibility tests and a static simulator, and Marzhin for
dynamic simulation. The static simulator graphically reflects the deterministic out-
come of the scheduling analysis, whereas the dynamic simulator exhibits the behavior
of the multi-agent engine execution. The result of both simulators is displayed graphi-
cally in an advanced time lines viewer.
Fig. 5. AADL Inspector 1.4
Thanks to AADL Inspector, it is thus possible to load a complete AADL project
distributed on several files containing textual declarative statements, to analyse it in
order to build the corresponding instance model, to perform the proper model trans-
formation so that it can be processed by Marzhin, and to pilot its virtual execution
through a control panel.
3.2 Executing AADL models
Such a virtual execution of AADL models can efficiently complements the use of
more formal real time analysis tools such as Cheddar, as it does not require the input
model to satisfy restricted assumptions. It thus significantly extends the scope of
model driven real time analysis, especially in the direction of non-periodic activities.
Another use of virtual execution is to perform architecture trade-off studies by pro-
viding an immediate feedback showing the coarse grain dynamic behavior of the sys-
tem during the design phases.
66
Finally, the specific technical approach that has been chosen for the implementa-
tion of Marzhin enables an easy interaction with an asynchronous environment, such
as a human operator or a virtual reality simulation.
This approach can be operated early in the development process of the system to
support system and software real-time design activities, before the software coding
phases. Although the AADL Behavior Annex is used to describe the concurrent as-
pects of the system behavior, purely procedural actions are still expressed by their
computation time. Further work would be required to investigate the ways to enrich
this approach with automatic code generation capabilities.
Fig. 6. Use of Virtual Execution in the development life cycle
Conclusion and Future Work
The current implementation of the Marzhin simulator that is available as a part of the
AADL Inspector tool already supports a comprehensive subset of the AADL runtime
semantics that enables virtual execution of models for the purpose of Real Time ana-
lysis, exploration of design solutions and early demonstration of the behavior of a
future system.
This work is partly realized in the context of the SMART project [3] in collaborati-
on with the University of Brest and with the financial support of the Council of Brit-
tany, the Council of Finistère, BMO and BPI France.
The future improvements that are foreseen for this activity concern a more com-
plete implementation of the AADL Behavior Annex, improved support of distributed
systems and investigations around the possible benefit of the approach for system
safety analysis with a proper use of the AADL Error Annex. An additional topic could
be studying the possible implications for automatic code generation.
67
References
1. F. Singhoff, J. Legrand, L. Nana, L. Marcé. “Cheddar: a Flexible Real-Time Scheduling
Framework”, ACM SIGAda Ada Letters, 24(4):1-8, ACM Press. 2004
2. SAE International. “Architecture Analysis and Design Language (AADL)”, AS5506B.
2012
3. P. Dissaux, O. Marc, S. Rubini , C. Fotsing, V. Gaudel, F. Singhoff, A. Plantec, Vương
Nguyễn-Hồng, Hải Nam Trần. “The SMART Project: Multi-Agent Scheduling Simulation
of Real-time Architectures”, Proceedings ERTS conference. 2014.
4. P. Dissaux, P. Farail. “Model Verification: Return of experience”, Proceedings ERTS con-
ference. 2014.
5. Ellidiss Technologies. AADL Inspector site: http://www.ellidiss.fr
68
Automatic Derivation of AADL Product Architectures in
Software Product Line Development
Javier González-Huerta, Silvia Abrahão, Emilio Insfran
ISSI Research Group, Universitat Politècnica de València
Camino de Vera, s/n, 46022, Valencia, Spain
{jagonzalez, sabrahao, einsfran}@dsic.upv.es
Abstract. Software Product Line development involves the explicit management
of variability that has to be encompassed by the software artifacts, in particular
by the software architecture. Architectural variability has to be not only sup-
ported by the architecture but also explicitly represented. The Common Variabil-
ity Language (CVL) allows to represent such variability independently of the Ar-
chitecture Description Language (ADL) and to support the resolution of this var-
iability for the automatic derivation of AADL product architectures. This paper
presents a multimodel approach to represent the relationships between the exter-
nal variability, represented by a feature model, and the architectural variability,
represented by the CVL model, for the automatic derivation of AADL product
architectures through model transformations. These transformations take into ac-
count functional and non-functional requirements.
Keywords: AADL; Software Product Line Development; Architecture Deriva-
tion; Variability Representation.
1 Introduction
Software Product Line (SPL) development is aimed to support the construction of a set
of software products sharing a common and managed set of features, which are devel-
oped from a common set of core assets in a prescribed way [1]. Thus, in SPL develop-
ment variability must be defined, represented, exploited and implemented [2]. The ex-
ternal variability (relevant to customers), usually represented by a feature model [3],
should be realized by the internal variability (relevant to developers) of the software
assets used to build up each individual software product [4].
Software Architecture is a key asset in SPL development and plays a dual role: on
the one hand the product line architecture (PLA) should provide variation mechanisms
that help to achieve a set of explicitly allowed variations and, on the other hand, the
product architecture (PA) is derived from the PLA by exercising its built-in architec-
tural variation points [1].
In order to enable the automatic resolution of the PLA variation points is required
not only that the architectural description languages provide variation mechanisms, but
also to explicitly represent how the different variants realize the external variability
usually represented in feature models.
69
Although AADL [5] incorporates different variation mechanisms that allow describ-
ing variability in system families [6], the explicit representation of the variation points
and its variants is also required to cope with the problem of product configuration and
architecture derivation.
To tackle this problem, in previous works, we presented the quality-driven product
architecture derivation, evaluation and improvement (QuaDAI) method [7], which uses
a multimodel to guide the software architect in the derivation, evaluation and improve-
ment of product architectures in a model-driven software product line development pro-
cess.
The Common Variability Language (CVL) [8] is a language that allows the specifi-
cation of variability over any EMF-based, and supports the resolution of the variability
and automatic derivation of resolved models. CVL incorporates its own variability
mechanisms (e.g., fragment substitution) that can be used to extend those provided by
the ADLs.
In this paper, we extend the multimodel approach to incorporate the explicit repre-
sentation of the architectural variability, by using CVL, and to establish relationships
among architectural variants and variation points with: i) the features that represent the
SPL external variability; ii) the non-functional requirements and iii) the quality attrib-
utes. Once the application engineer has selected the features and non-functional require-
ments (NFRs) and the priorities of the quality attributes that together conform the prod-
uct configuration, the relationships defined in the multimodel allow us to automatically
derive the product AADL specification from the PLA.
The remainder of the paper is structured as follows. Section 2 discusses existing
approaches that deal with the explicit representation of architectural variability and the
derivation of product architectures in SPL development by using CVL. Section 3 pre-
sents our approach for the derivation of AADL product architectures by introducing the
explicit representation of the architectural variability with CVL. Finally, Section 4
drafts our conclusions and final remarks.
2 Related work
AADL incorporates different architectural variation mechanisms that support the de-
velopment of system families (e.g., multiples implementation of a system specification,
component extension or the configuration support through alternative source code files)
[6]. However, in a real SPL scenario is difficult to manage the derivation of the archi-
tectural specification of a product (PA), especially when the SPL allows a wide range
of variability. To cope with the problem, in the last years, several approaches had been
presented that support the representation of architectural variability and the derivation
of product architectures in SPL development by using CVL (e.g., [9], [10], [11]).
Nascimento et al. [10] present an approach for defining product line architectures
using CVL. They apply the Feature-Architecture Mapping Method (FArM) to filter the
feature models in order to consider only the architectural-related features. These fea-
tures will form the CVL specification that will allow obtaining the COSMOS* archi-
tectural models. They do not define relationships between the external variability model
70
(features model) and the architectural variability expressed in CVL and thus the deri-
vation of the product architecture taking as input the configuration is not supported.
They explicitly omit the non-functional requirements when applying the FArM method.
Svendsen et al. [11] present the applicability of CVL for obtaining the product mod-
els for a Train Control SPL that are defined using a DSL. They only consider the ex-
plicit definition of the internal variability and consequently, the configuration should
be made directly over the CVL specification of the internal variability.
Combemale et al. [9] present an approach to specify and resolve variability on Re-
usable Aspect Models (RAM), a set of interrelated design models. They use CVL to
resolve the variability on each model and then compose the corresponding reusable
aspects by using the RAM weaver. They also consider just the internal variability, and
the configuration should be made over the CVL specification.
In summary, none of the aforementioned approaches establish relationships among
the SPL external variability and the architectural variability, even though some of them
acknowledge that is a convenient practice in variability management [9]. Establishing
connections between the SPL external variability, expressed by means of feature mod-
els, the non-functional requirements, represented in the quality model, and the archi-
tectural variability, represented by using CVL allows us:
i) To configure the product by using the feature model and the quality view-
point;
ii) To check its consistency by using the constraints defined on the features
model, on the quality viewpoint and on the multimodel;
iii) To solve the architectural variability automatically by using model trans-
formations.
3 A Multimodel Approach for the Derivation of AADL Product
Architectures
QuaDAI is an approach for the derivation, evaluation and improvement of product ar-
chitecture that defines an artifact (the multimodel) and a process consisting of a set of
activities conducted by model transformations. QuaDAI relies on a multimodel [12]
that allows the explicit representation of different viewpoints of a software product line
and the relationships among them. In this section, we focus on the representation of the
architectural variability, its resolution and the derivation of the software architecture of
the product under development.
3.1 Illustrating Example
The approach is illustrated through the use of a running example: a SPL from the auto-
motive domain that comprises the safety critical embedded software systems responsi-
ble for controlling a car. This SPL is an extension of the example introduced in [13],
and was modified in order to apply, among others the variation points described in [14].
71
This SPL comprises several features such as Antilock Braking System, Traction Con-
trol System, Stability Control System or Cruise Control System. The Cruise Control
System feature incorporates variability. This variability is resolved depending on other
selections made on the features model (i.e., the selection of the cruise control together
with the park assistant implies the positive resolution of an extended version of the
cruise control1). Fig. 1 shows an excerpt of the features model that represents the SPL
external variability.
VehicleControlSystem
Attributes
[1..10]
[0..1]
[0..1] [0..1] [1..1] [0..1]
CruiseControl ParkAssistant AutoPark MultimediaSystem GPS
[0..1] Attributes Attributes Attributes Attributes Attributes
[1..2]
[0..1] EstabilityControl
Attributes
[0..1]
Color_OnboardComputer
TractionControl [0..1]
Attributes
[1..1] Attributes
[0..1] B_W_OnboardComputer
ABS [0..1]
Attributes
Legend
Attributes GPS
Feature Feature Group
FM_CD FM_CD_Charger Attributes
Attributes Attributes
Optional Implies
Mandatory Excludes
Fig. 1. SPL External Variability
3.2 A Multimodel for Representing Architectural Variability
In QuaDAI, a multimodel permits the explicit representation of relationships among
entities in different viewpoints. A multimodel is a set of interrelated models that repre-
sent the different viewpoints of a particular system. A viewpoint is an abstraction that
yields the specification of the whole system restricted to a particular set of concerns,
and it is created with a specific purpose in mind. In any given viewpoint it is possible
to produce a model of the system that contains only the objects that are visible from
that viewpoint [16]. Such a model is known as a viewpoint model, or view of the system
from that viewpoint. The multimodel permits the definition of relationships among
model elements in those viewpoints, capturing the missing information that the separa-
tion of concerns could lead to [12].
The problem of representing and automatically resolving the architectural variability
taking into account functional and non-functional requirements requires (at least) three
viewpoints:
The variability viewpoint represents the SPL external variability express-
ing the commonalities and variability within the product line. Its main ele-
ment is the feature, which is a user-visible aspect or characteristic of a sys-
tem [3] and it is expressed by means of a variant [15] of the cardinality
1 The whole specification of the example is available at http://users.dsic.upv.es/~jagonza-
lez/CarCarSPL/links.html
72
based feature model (shown in Fig. 1).
The architectural viewpoint represents the architectural variability of the
Product Line architecture that realizes the external variability of the SPL
expressed in the variability viewpoint. It is expressed by means of the Com-
mon Variability Language (CVL) and its main element is the Variability
Specification (VSpec). We only represent in the multimodel the PLA archi-
tectural variability, the PLA is represented in an AADL base model, which
is referenced by the CVL specification. A base model, under the CVL ter-
minology, is a model on which variability is defined using CVL [8]. The
base model is not part of CVL and can be an instance of any metamodel
defined via MOF [8]. Fig. 2 shows an example of the CVL variability spec-
ification on an AADL base model, allowing to express whether some
AADL elements should exist or not in the resolved model (e.g., the ABS)
and to configure some internal values (e.g., the range value assignment).
The quality viewpoint represents the hierarchical decomposition of quality
into sub-characteristics, quality attributes, metrics and the impacts and con-
straints among quality attributes. Is expressed by means of a quality model
for software product lines [17], which extends the ISO/IEC 25010
(SQuaRE) [18] and allows the representation of NFRs as constraints affect-
ing characteristics, sub-characteristics and quality attributes.
CVL Variability Control System
Specification Tree
Distance Sensors
Wheel Sensor Brake Actuator ABS System
Frontal Sensor Rear Sensor
Legend
Rear Sensor
range: int
Architectural variant
Variability Points
:ObjectExistence :ObjectExistence :ObjectExistence :ObjectExistence :SlotValueAssignment :ObjectExistence
:ObjectExistence Variation point nature
Base Model ABS Control System Distance Sensor
Wheel Sensor Brake Actuator Braking_pedal_sensor Object_distance Doppler Sensor Doppler Sensor
Wheel_sensor Speed
Pulse Brake_signal Range Distance Distance AADL model element
Brake_actuator_signal
Fig. 2. CVL Variability Specification on an AADL Base Model
The multimodel also allows the definition of relationships among elements on each
viewpoints with different semantics as is_realized_by [19] or impact relationships [12].
An excerpt of these relationships is shown in Fig. 3.
We can describe in the multimodel: i) how the ABS feature is_realized_by a set of
VSpecs (e.g., the WheelRotationSensor); ii) how the user_safety NFR is_realized_by a
set of features (e.g., the ABS or the Stability Control); iii) how the selection of a given
feature VSpec impacts positive or negatively on a quality attribute; or iv) how the pos-
itive resolution of a given VSpec impacts positive or negatively on a quality attribute.
These relationships are used to check the consistency of the configuration and to decide
73
which variation points should be resolved positively in the CVL resolution model driv-
ing the derivation of the AADL product architecture.
Relationships Used during Derivation
Architectural Variation Point Non-Functional Requirement
WheelRotationSe...
Feature Non-Functional Requirement NFR_i
RotationSensor <>
ABS Maturity Level
NFR_i
Attributes <>
UserSafetyLevel1 Architectural Variation Point Feature
WheelRotationSe...
ABS
v Feature RotationSensor
Quality Attribute <> Attributes
ABS
Qj
<> Attributes Architectural Variation Point
v
Memory Consumption Quality Attribute WheelRotationSe...
Qj RotationSensor
<>
FaultTolerance
Fig. 3. Multimodel Relationships
3.3 Automating the Derivation of Product Architectures
The QuaDAI derivation process for obtaining AADL product architectures based on
the functional and non-functional requirements comprises two main activates: the prod-
uct configuration and the architecture instantiation. Fig. 4 shows an excerpt of the
specification of the activities with the main input and output artifacts using the Software
& Systems Process Engineering Meta-Model (SPEM) [20].
Application Application
engineer architect
1 2
Product Architecture
instantiation
Multimodel
Product Variability Quality Architectural AADL CVL
requirements viewpoint viewpoint viewpoint PL architecture transformation
in
in
in
in
in
in
Valid
Yes 2.1 2.2
Obtain Product Consistency CVL resolution model Product architecture
validation generation instantiation
ou
ou
ou
in No in in
t
t
t
AADL Product
CVL resolution architecture
model
Fig. 4. SPEM specification of the QuaDAI Derivation Process
In the product configuration activity, the application engineer selects the features
and NFRs that the product must fulfill and establishes the quality attributes priorities in
the obtain product configuration task. Those priorities will be used during the deriva-
tion to choose from a set of architectural variants that having the same functionality
differ in their quality attribute levels. In the consistency validation activity, first we
check the variability viewpoint consistency (i.e., whether the selection of features ful-
fills the constraints defined in the feature model) and the quality viewpoint consistency
(i.e., whether the priorities of the quality attributes defined in the configuration satisfy
74
the impact and constraint relationships among them defined in the quality viewpoint).
Once the intra-viewpoint consistency is satisfied we check the inter-viewpoint con-
sistency (i.e., whether the configuration satisfy the is_realized_by and impact relation-
ships defined among elements on different viewpoints). The multimodel relationships
had been formalized and operationalized in OCL and are checked at runtime by using
the OCLTools validator [21]. This consistency checking mechanism allows us to assure
that the product configuration meets the SPL constraints facilitating the architecture
instantiation activity that focus on the resolution of the PLA architectural variability.
In the architecture instantiation activity, the application architect generates the
AADL product architecture by means of two model transformation activities. The first
transformation, CVL resolution model generation, takes as input a valid product con-
figuration and the multimodel (i.e., the relationships between the architectural view-
point with variability and the quality viewpoint) and, through a Query View Transfor-
mation (QVT) [22] model transformation, generates a CVL resolution model. With the
multimodel relationships, the QVT transformation decides which architectural variants
have to be positively resolved in each variation point. Finally, the product architecture
instantiation activity, through a CVL transformation, takes as input the CVL resolution
model and generates the AADL product architecture. This AADL product architecture
represents the resolution of the PLA architectural variability taking into account not
only the functional requirements and non-functional requirements selected in the con-
figuration. The use of CVL alleviates part of the computational complexity since it
allows us, at design time, to describe the PLA architectural variants and, in derivation
time, to only focus on the resolution of the PLA architectural variability. Fig. 5 shows
an outline of the AADL architecture derivation with the CVL resolution model gener-
ation and the AADL Product architecture instantiation.
CVL Resolution...
Model + AADL Produc Line Architecture
(as CVL Base Model)
VSpecResolution
VSpec1 ABS Control System
VSpec1
Brake_pedal_signal
NFR1 Rotation_sensor_signa
isRealizedBy
VSpecResolution
ABS VSpec2 Brake_actuator_signal
Reliability ABSControlSystem
Control System
Brake Signal
CVL resolution model
generation Brake Actuators Brake_actuators
VSpec
VSpec 4
VSpec2 3
VSpec1 QVT-Relations CVL
Featurea transformation transformation
isRealizedBy
ABS Product architecture
ABS Control System instantiation
VSpec4
Qa Brake pedal sensor AADL Product Architecture
impact
Latency ABS Control System
Rotation Sensor Brake
Time Brake_pedal_signal
Rotation sensor Brake_actuators
Rotation_sensor_signa
Wheel pulse Brake_actuator_signal Brake Signal
Fig. 5. AADL Product Architecture Instantiation
75
3.4 Tool Support
The approach is supported by a prototype2 that gives support to the configuration, con-
sistency checking and generation of the CVL resolution model. The prototype allows
importing feature models and CVL specifications defined using third party tools and to
establish the relationships among them described in the paper so as to automate the
AADL product architecture derivation.
The variability viewpoint consistency checking is carried out by transforming the
feature model and the features selection to the FAMA [23] metamodel and by calling
the FAMA validator. The quality viewpoint and the inter-viewpoint consistency check-
ing are carried out through OCL constraints checked at runtime by the OCLTools val-
idator. The tool is also capable of calling the QVT transformation that generates the
CVL resolution model.
Fig. 6(a) shows the call to the CVL resolution creation functionality. Fig. 6(b) shows
the resulting CVL resolution model when for a configuration formed by the feature
configuration features={Vehicle Control System, ABS, TractionCon-
trol, StabilityControl and FM_CD} (see Fig. 1) and the NFRs configu-
ration nfrs={EuroNCAP3}.
Finally, with the integration of the CVL supporting tool [24] the CVL transfor-
mation can be called so as to generate the resulting AADL product architecture.
Fig. 6. Generation of the CVL Resolution Model with the Prototype
2 The prototype is available for download at: http://users.dsic.upv.es/~jagonzalez/Car-
CarSPL/index.html
3 EuroNCAP is a voluntary EU vehicle safety rating system. In our example, the EuroNCAP
NFR is realized by the ABS, the Traction Control, and the Stability Control features.
76
4 Conclusions and Further Works
In this paper, we have presented an approach to explicitly represent architectural
variability on AADL architectural models by using CVL. We include the architectural
variability in a multimodel in which we also represent the SPL external variability in a
feature model, and the non-functional requirements in a quality model. In this multi-
model, we can establish relationships among elements on the CVL model, the feature
model and the quality model. This information is used to drive the model transformation
that resolves the architectural variability and obtains the AADL product architecture.
The approach is supported by a tool with which the user can edit a product configura-
tion, check its consistency and automatically derive the CVL resolution model. The
CVL resolution models allow us to obtain the AADL product architecture by using the
CVL supporting tool.
In this work, we apply model-driven engineering principles to provide a feasible
solution to an open, complex, error-prone and time-consuming problem in the software
product line development community, which is the derivation of product architectures
takin into account functional and non-functional requirements.
As further work, we plan to empirically validate the approach through controlled
experiments and case studies. We plan also to analyze how to incorporate more power-
ful CVL variation mechanisms (i.e., the use of VInterfaces that can be used to configure
CVL configuration units) and its possible use in combination with the AADL syntax.
Finally, although the approach has been initially defined for working together with
AADL, the use of CVL isolates the approach from the architectural description lan-
guage and we want to analyze its applicability to other MOF-based ADLs.
Acknowledgements. This research is supported by the Value@Cloud project
(MICINN TIN2013-46300-R) and the ValI+D fellowship program (ACIF/2011/235).
References
1. Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-
Wesley Professional (2001).
2. Van der Linden, F., Schmid, K., Rommes, E.: Software Product Lines in Action: The
Best Industrial Practice in Product Line Engineering. Springer Berlin Heidelberg
(2007).
3. Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-Oriented
Domain Analysis (FODA) Feasibility Study. , CMU/SEI-90-TR-21 ESD-90-TR-222,
Software Engineering Institute, Carnegie Melon University (1990).
4. Pohl, K., Böckle, G., van der Linden, F.: Software product line engineering. Springer,
Berlin (2005).
5. Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to
the SAE Architecture Analysis & Design Language. Addison Wesley (2013).
6. Feiler, P.H.: Modeling of System Families. , CMU/SEI-2007-TN-047, Software
Engineering Institute, Carnegie Mellon University (2007).
7. González-Huerta, J., Insfrán, E., Abrahão, S.: Defining and Validating a Multimodel
Approach for Product Architecture Derivation and Improvement. 16th International
77
Conference on Model-Driven Engineering Languajes and Systems. pp. 388–404. ,
Miami, USA (2013).
8. Object Management Group: Common Variability Language ( CVL ) OMG Revised
Submission. (2012).
9. Combemale, B., Barais, O., Alam, O., Kienzle, J.: Using CVL to operationalize
product line development with reusable aspect models. Workshop on Variability
Modeling Made Useful for Everyone. pp. 9–14. , Innsbruck, Austria (2012).
10. Nascimento, A.S., Rubira, C.M.F., Burrows, R., Castor, F.: A Model-Driven
Infrastructure for Developing Product Line Architectures Using CVL. 7th Brazilian
Symposium on Software Components, Architectures and Reuse. pp. 119–128. ,
Brasilia, Brazil (2013).
11. Svendsen, A., Zhang, X.: Developing a software product line for train control: a case
study of CVL. 14th Software Product Line Conference. pp. 106–120. , Jeju Island,
South Korea (2010).
12. González-Huerta, J., Insfran, E., Abrahão, S.: A Multimodel for Integrating Quality
Assessment in Model-Driven Engineering. 8th International Conference on the Quality
of Information and Communications Technology. pp. 251–254. , Lisbon, Portugal
(2012).
13. Hudak, J., Feiler, P.H.: Developing AADL Models for Control Systems : A
Practitioner ’ s Guide. , CMU/SEI-2007-TR-014, Software Engineering Institute,
Carnegie Mellon University (2007).
14. Shiraishi, S.: An AADL-based approach to variability modeling of automotive control
systems. 13h Model Driven Engineering Languages and Systems. pp. 346–360. , Oslo,
Norway (2010).
15. Gómez, A., Ramos, I.: Cardinality-Based Feature Modeling and Model-Driven
Engineering : Fitting them Together. International Workshop on Variability Modelling
of Software-Intensive Systems. pp. 61–68. , Linz, Austria (2010).
16. Barkmeyer, E.J., Feeney, A.B., Denno, P., Flater, D.W., Libes, D.E., Steves, M.P.,
Wallace, E.K.: Concepts for Automating Systems Integration. , NISTIR 6928, U.S.
Department of Commerce (2003).
17. González-Huerta, J., Insfran, E., Abrahão, S., McGregor, J.D.: Non-functional
requirements in model-driven software product line engineering. Proceedings of the
Fourth International Workshop on Nonfunctional System Properties in Domain
Specific Modeling Languages. pp. 1–6. , Innsbruck, Austria (2012).
18. ISO/IEC: ISO/IEC 25000:2005 Software Engineering - Software product Quality
Requirements and Evaluation (SQuaRE) - Guide to SQuaRE, (2005).
19. Janota, M., Botterweck, G.: Formal approach to integrating feature and architecture
models. 11th Conference on Fundamenteal Approaches to Software Engineering. pp.
31–45. , Budapest, Hungary (2008).
20. Object Management Group: Software & Systems Process Engineering Meta-Model
Specification (SPEM) v2.0. (2008).
21. Eclipse: Eclipse OCL, http://projects.eclipse.org/projects/modeling.mdt.ocl.
22. Object Management Group: Meta Object Facility (MOF) 2.0 Query / View /
Transformation Specification. (2008).
23. ISA Research Group: Fama Tool Suite, http://www.isa.us.es/fama/.
24. Haugen, Ø., Moller-Pedersen, B., Olsen, G.K., Svendsen, A., Fleurey, F., Zhang, X.:
Consolidated CVL language and tool. , MoSiS Project, D.2.1.4., SINTEF, Univeristy
of Oslo (2010).
78
Towards an Architecture-Centric Approach
dedicated to Model-Based Virtual Integration
for Embedded Software Systems
Huafeng Yu1 , Jean-Pierre Talpin2 , Sandeep Shukla3 ,
Prachi Joshi3 , and Shinichi Shiraishi1
1
TOYOTA InfoTechnology Center, U.S.A.
465 N Bernardo Avenue, Mountain View, CA 94043, U.S.A.
huafeng.yu@us.toyota-itc.com
2
INRIA Rennes - Bretagne Atlantique,
Campus de Beaulieu, 263 Avenue Général Leclerc, 35042 Rennes, France
3
Virginia Polytechnic Institute and State University
Falls Church Campus, 7054 Haycock Rd., Falls Church, VA 22043, USA
Abstract. Current embedded systems are increasingly more complex
and heterogeneous, but they are expected to be more safe, reliable and
adaptive. In consideration of all these aspects, their design is always a
great challenge. Developing these systems with conventional design ap-
proaches and programming methods turns out to be difficult. In this
paper, we mainly present the informative background and the general
idea of an ongoing yet young research project, including the model-
based design and an architecture-centric approach, to address previous
challenges. Our idea adopts a formal-methods-based model integration
approach, dedicated to architecture-centric virtual integration for em-
bedded software systems, in an early design phase. We thus expect to
improve and enhance Correct By Construction in the design. The consid-
ered formal methods consist of timing specification, design by contracts,
and semantics interoperability for models to be integrated in the system.
The application domains of our approach include automotive and avionic
systems.
Keywords: Virtual integration, model-based design, AADL, timing spec-
ification, design by contract, semantics interoperability
1 Introduction
Current embedded systems are increasingly more complex and heterogeneous,
but they are expected to be more safe, reliable and adaptive [8] [16]. In consid-
eration of all these aspects, their design is always a great challenge. Complexity
in the design and implementation is a common issue for current avionic and
automotive systems. In the current system design, verification and validation
(V&V) is also a key concern, particularly for safety-critical systems. These sys-
tems generally require great V&V effort to avoid unexpected system behavior.
79
Moreover, the design is expected to be validated as early as possible due to the
huge cost of correction in the late-phase implementation. Design validation in
an early phase has become one of the key solutions to reduce the overall V&V
cost.
In this paper, we mainly present the informative background and the gen-
eral idea of an ongoing yet young research project, including the model-based
design and an architecture-centric approach, to address previous challenges. Our
idea adopts an formal-methods-based model integration approach, dedicated to
architecture-centric virtual integration for embedded software systems, in an
early design phase. By applying formal methods in an early design phase, we
expect to improve and enhance correct by construction. The formal methods to
be considered consist of timing specification, design by contracts, and seman-
tics interoperability for models to be integrated in the system. The application
domain of our approach include avionic and automotive systems.
2 Research Challenges
High-level modeling has been widely adopted as a promising solution to ad-
dress the system complexity issue [33]. High-level modeling languages, such
as UML[27], SysML[1] and MARTE[26], have been widely adopted, thanks to
its standardization for modeling. AUTOSAR[2] and EAST-ADL[9] are domain-
specific languages for automotive systems. AADL[32] (Architecture Analysis and
Design Language) is an SAE standard dedicated to architecture description and
modeling for avionic and automotive systems. AADL provides an industry stan-
dard, textual and graphic notation with precise semantics to model applica-
tions and execution platforms and is supported by commercial and open source
tool solutions—including Open Source AADL Tool Environment (OSATE) [28].
Matlab/Simulink[21] is a dataflow language for modeling, simulating and analyz-
ing dynamic systems. Modelica[23] is an object-oriented modeling language for
component-based complex systems. These high-level languages enables domain
specific modeling and analysis of complex embedded systems. SCADE [12] is
an integrated design environment dedicated to rigorous design of safety-critical
systems[4].
Multi-paradigm modeling
All the languages mentioned previously are considered as candidate languages
in high-level modeling for embedded systems. Multi-languages can be used in
the same design because of system modeling from different views, for example,
software, architecture, etc.; and different purposes, such as analysis, verification,
and evaluation. Furthermore, different languages may adopt different formalism,
e.g., state machines, dataflow, communicating sequential processes, differential
equations, as backstage support. So the first challenge at the modeling language
level is how to harmonize multiple paradigm modeling [24] [25] in the same
80
design, particularly, when we consider a reliable integration followed by using
formal techniques for analysis and V&V at the system level.
An avionic co-modeling example. Co-modeling for the system-level de-
sign has been explored in [37] [36], where AADL was used to model the archi-
tecture part and Simulink was used to model the behavior part of an avionic
case study, called simplified Airbus A350 doors management system. However,
semantic difference of the two models makes the integration problematic. In or-
der to have a clear and unambiguous integration, a formal model of computation
(MoC), called Polychrony [17], was adopted as an intermediate model. This MoC
is based on the synchronous/polychronous timing semantics. The later formal
analysis, verification, and scheduling were mainly performed on the basis of the
same MoC.
Integration frameworks
In Polychrony, the integration is performed at the polychronous MoC level[36].
Polychrony provides model transformations from AADL and Simulink (via Ge-
neAuto[35]) to the polychronous MoC. In order to keep the semantics coherent,
both AADL and Simulink models adopt the polychronous semantics. Based on
the same polychronous semantics, the composed model can used for analysis,
verification, and simulation or be translated into other formal models for formal
verification and scheduling. So in this integration scheme, the core polychronous
model provides formal semantics support and its environment provides tool con-
nection. Model-based system integration has also been discussed in [34] with
regard to cyber-physical systems, [6] for tool integration platform, [31] based
on SOA (Service of Architecture), [10] for heterogeneous models integration,
and [29] for real-time software engineering. AUTOSAR[2] aims at component-
level integration for automotive systems. System Architecture Virtual Integra-
tion (SAVI) program [30] [13] aims at creating an architecture-centric model
repository to support analysis of virtually integrated system models related to
performance, safety, and reliability, and so on. It also enables to discover system-
level faults at the early design phase, thus reduce risk, cost, and development
time.
3 A Model-Based Architecture-Centric Virtual
Integration Framework
Based on the previous exploration of design issues and the state of the art of
solutions in research, we find an architecture-centric model-based integration
framework is necessary for the next-generation design of automotive software
systems. The framework is expected to provide the following advantages: reliable
model integration, fast and early-phase design validation, architecture optimiza-
tion enabling, easy access to current matured software development tools and
environment, etc. With this objective in mind, we first propose a model-based
81
architecture-centric virtual integration approach, in the framework of model-
based systems engineering [11], for the design of next-generation automotive
systems. This approach is involved in mostly correct by construction technolo-
gies, rather than a posterioriVerification & Validation in the implementation
phase. We adopt different modeling languages with regards to different views
of the system, for example, AADL for architecture modeling and Simulink for
behavioral modeling, etc. The main research topics in the project include: tim-
ing specification [5], design by contracts and semantics interoperability for the
purpose of a reliable model integration, which are explained in the following
subsections.
Timing specification
With all the concerns in the embedded system design, timing is one of the most
significant ones. In general, the timing issue becomes more explicit when ar-
chitecture is considered and the system is integrated, due to the gap between
software and architecture design. In our project, we consider high-level, formal-
ized timing constraints to be defined, observed and analyzed based on software
architecture, specified in AADL. From this point of view, an architecture cen-
tric approach is adopted for the model integration in our project. Considering
abstraction in the system design, we advocate the modeling of synchrony and
time as software and hardware events, which are related to synchronization in
an architecture specification. Compared to real time, synchronous logical time,
applied on both software and architecture, provides an algebraic framework in
which both event-driven and time-triggered execution policies can be specified.
In the framework of our project, we define the semantics and algebra with
regard to logical timing constraints and specification, and support the submis-
sion of a timing-related annex to the SAE standard AADL[32]. This annex will
define a synchronous and timed specification framework to formally model time
domains pertaining to the design of embedded architectures, including the speci-
fications of automotive software architectures. The behavior annex of AADL are
considered as the vehicle to implement this model, together with a timing annex
(TA), as a mean to represent abstractions of these behavior annexes using clock
constraints and regular expressions.
Design by contract
Design by contract [22] [15] is also adopted in our approach in the project.
Contracts play a significant role in the safe and reliable model integration in our
approach. We first analyze high-level requirements from automotive or avionic
systems, from which formalizable requirements are then extracted according to
the technical formalizability and verifiability. These requirements are expressed
in formal languages so that they can be used to build the contracts for the
integration of models that implement corresponding functionality. The contracts
are expected to consider different criteria for safety, performance, cost, timing
constraints, and so on. A mathematical framework will then be built to define the
82
composition of these models, together with the contracts on them, in a formal
way. The contracts and their associated models will be checked by modeling
checking technologies [14] [19] [7] .
Semantics interoperability
One of the main issues in the composition of models is semantics difference
between heterogeneous models and different formalism. One of the feasible solu-
tions to this issue is to have a common model as the intermediate formal model,
and all other models are translated into the common model. An example can
be found in [37]. The intermediate model provides the formal semantics, based
on which, expected properties of the original models and their integration are
checked. However, this requires a semantics preservation in the model transla-
tion, which is not practical in most cases. Another solution is related to formal
semantics interoperability. Some work can be found in [3] [20], [18]. Our current
research topic is focusing on the study of differences between the models, which
can lead to issues in the model translations, from the point of view of model se-
mantics, particularly timing semantics and operational semantics. The expected
result of this research is intended to provide a foundation of the previous two
research topics.
4 Conclusion
In this position paper, we have presented several important issues in current
system design related to embedded systems, such as multi-paradigm modeling,
integration framework, and formal semantics issues. A brief survey of corre-
sponding research topics was also presented. We, hence, propose a model-based
architecture-centric integration approach, considering timing specification, de-
sign by contract and semantics interoperability as main topics of research. Based
on these research, a model-based integration framework is expected to be built,
which is dedicated to model-based systems engineering for next-generation au-
tomotive systems.
Acknowledgment
The authors appreciate the valuable advices from Ryo Ito and Kazuhiro Kajio
(Toyota Motor Corporation).
References
1. Systems Modeling Language (SysML). http://www.sysml.org/specs.
2. AUTOSAR (AUTomotive Open System ARchitecture). http://www.autosar.org/.
3. A. Benveniste, B. Caillaud, L.P. Carloni, P. Caspi, and A.L. Sangiovanni-
Vincentelli. Composing Heterogeneous Reactive Systems. ACM Transactions on
Embedded Computing Systems, 7(4), 2008.
83
4. A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic, and R. de
Simone. The Synchronous Languages Twelve Years Later. Proceedings of the
IEEE, 2003.
5. L. Besnard, E. Borde, P. Dissaux, T. Gautier, P. Le Guernic, and J.-P. Talpin.
Logically timed specifications in the aadl : a synchronous model of computation
and communication (recommendations to the sae committee on aadl. Technical
Report 446, INRIA, 2014.
6. M. Broy, M. Feilkas, M. Herrmannsdoerfer, S. Merenda, and D. Ratiu. Seamless
Model-Based Development: From Isolated Tools to Integrated Model Engineering
Environments. Proceedings of the IEEE, 98:526–545, 2010.
7. Darren Cofer, Andrew Gacek, Steven Miller, Michael W Whalen, Brian LaValley,
and Lui Sha. Compositional Verification of Architectural Models. In NASA Formal
Methods, 2012.
8. DARPA. Adaptive Vehicle Make (AVM) Project.
http://www.darpa.mil/Our Work/TTO/Programs.
9. EAST-ADL. http://www.east-adl.info.
10. J. Eker, J.W. Janneck, E.A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer,
S. Sachs, and Y. Xiong. Taming Heterogeneity - the Ptolemy Approach. Pro-
ceedings of the IEEE, 91(1):127–144, 2003.
11. J.A. Estefan. Survey of Model-Based Systems Engineering (MBSE) Methodologies.
Technical report, INCOSE MBSE Initiative, 2008.
12. Esterel Technologies. SCADE Suite. http://www.esterel-
technologies.com/products/scade-suite/.
13. P. Feiler, J. Hansson, D. de Niz, and L. Wrage. System Architecture Virtual
Integration: An Industrial Case Study. Technical report, Software Engineering
Institute, Nov. 2009. CMU/SEI-2009-TR-017.
14. A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A Tool for
Automatic Verification of Probabilistic Systems. In Proceedings of the 12th Inter-
national Conference on Tools and Algorithms for the Construction and Analysis of
Systems, TACAS’06, pages 441–444, Berlin, Heidelberg, 2006. Springer-Verlag.
15. J.-M. Jézéquel and B. Meyer. Design by Contract: The Lessons of Ariane. Com-
puter, 30:129–130, 1997.
16. Xiaoqing Jin, Jyotirmoy Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts.
Challenges of Applying Formal Methods to Automotive Control Systems. In NSF
National Workshop on Transportation Cyber-Physical Systems, 2014.
17. P. Le Guernic, J.-P. Talpin, and J.-C. Le Lann. Polychrony for System Design.
Journal for Circuits, Systems and Computers, 12:261–304, 2002.
18. E. A. Lee and A. Sangiovanni-Vincentelli. A Framework for Comparing Mod-
els of Computation. IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems, 17(12):1217–1229, 2006.
19. A. Legay, B. Delahaye, and S. Bensalem. Statistical model checking: An overview.
In Runtime Verification, 2010.
20. D. Mathaikutty, H. Patel, S. Shukla, and A. Jantsch. Modelling Environment for
Heterogeneous Systems based on MoCs. In Forum on specification and Design
Languages (FDL), pages 291–303, 2005.
21. MathWorks. The MathWorks: Matlab/Simulink.
http://www.mathworks.com/products/simulink/.
22. B. Meyer. Applying ’design by contract’. Computer, 25(10):40–51, Oct 1992.
23. Modelica and the Modelica Association. https://www.modelica.org.
84
24. P. J. Mosterman and H. Vangheluwe. Computer automated multi-paradigm mod-
eling: An introduction. SIMULATION: Transactions of the Society for Modeling
and Simulation International, 80(9):433–450, 2004.
25. K.D. Müller-Glaser, G. Frick, E. Sax, and M. Kühl. Multiparadigm Modeling in
Embedded Systems Design. IEEE Transactions on Control Systems Technology,
12(2):279–292, 2004.
26. Object Management Group (OMG). The UML Profile for MARTE:
Modeling and Analysis of Real-Time and Embedded Systems.
http://www.omg.org/spec/MARTE/1.1/PDF, June 2011.
27. OMG. Unified modeling language (uml). www.uml.org/.
28. OSATE. OSATE V2 Project. https://wiki.sei.cmu.edu/aadl/index.php/Osate 2.
29. Maxime Perrotin, Eric Conquet, Julien Delange, André Schiele, and Thanassis
Tsiodras. TASTE: A Real-Time Software Engineering Tool-Chain Overview, Sta-
tus, and Future. In SDL 2011: Integrating System and Software Modeling, 2012.
Lecture Notes in Computer Science Volume 7083, pp 26-37.
30. D. Redman, D. Ward, J. Chilenski, and G. Pollari. Virtual integration for improved
system design,. In The First Analytic Virtual Integration of Cyber-Physical Systems
Workshop in conjunction with RTSS, 2010.
31. A. Rossignol. The Reference Technology Platform. In CESAR - Cost-efficient
Methods and Processes for Safety-relevant Embedded Systems. Springer, 2013.
32. SAE Aerospace (Society of Automotive Engineers). Aerospace Standard AS5506A:
Architecture Analysis and Design Language (AADL) . SAE AS5506A, 2009.
33. D.C. Schmidt. Model-Driven Engineering. IEEE Computer, 39:25–31, 2006.
34. J. Sztipanovits, X. D. Koutsoukos, G. Karsai, N. Kottenstette, P.J. Antsaklis,
V. Gupta, B. Goodwine, J.S. Baras, and S. Wang. Toward a Science of Cyber-
Physical System Integration. Proceedings of the IEEE, 100(1):29–44, 2012.
35. A. Toom, T. Naks, M. Pantel, M. Gandriau, and I. Wati. Gene-Auto: An Automatic
Code Generator for a Safe Subset of SimuLink/StateFlow and Scicos. In European
Conference on Embedded Real-Time Software (ERTS’08), 2008.
36. H. Yu, Y. Ma, T. Gautier, L. Besnard, J.-P. Talpin, and P. Le Guernic. Poly-
chronous Modeling, Analysis, Verification and Simulation for Timed Software Ar-
chitectures. Journal of Systems Architecture (JSA), 59(10):1157–1170, 2013.
37. H. Yu, Y. Ma, Y. Glouche, J.-P. Talpin, L. Besnard, T. Gautier, P. Le Guernic, A.
Toom, and O. Laurent. System-level Co-simulation of Integrated Avionics Using
Polychrony. In ACM Symposium on Applied Computing (SAC’11), 2011.
85