Contract-based speci cation and analysis of AADL models . . . . . . . . . . . . . . . . . . . . . Ernesto Posse, Juergen Dingel An Extension for AADL to Model Mixed-criticality Avionic Systems Deployed on IMA architectures with TTEthernet . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Robati Tiyam, Amine El Kouhen, Abdelouahed Gherbi, Sardaouna Hamadou, John Mullins
Denis Buzdalov, Alexey Khoroshilov Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali Modeling Shared-Memory Multiprocessor Systems with AADL . . . . . . . . . . . . . . . . . Stphane Rubini, Pierre Dissaux, Frank Singho Executable AADL: Real-Time Simulation of AADL Models . . . . . . . . . . . . . . . . . . . . Pierre Dissaux, Olivier Marc Automatic Derivation of AADL Product Architectures in Software Product Line Development . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Javier Gonzalez-Huerta, Silvia Abrahao, Emilio Insfran Towards an Architecture-Centric Approach dedicated to Model-Based Virtual Integration for Embedded Software Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Huafeng Yu, Jean-Pierre Talpin, Sandeep Shukla, Prachi Joshi, Shin'Ichi Shiraishi 1 3 4 14 28 39 49 59 69 79 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 requirements of reusability, interoperability, exibility and portability. These new dimensions favor the use of an architecture description language that o ers a global vision of the system, 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 e orts related to behavior modelling and model-based analysis of DRE systems.
Cyber-Physical systems (CPS) combine many challenges to meet requirements for reusability, interoperability, exibility or dependability. The use of architecture description language helps to integrate components before implementing the system. Such integration approach eases system design analysis and implementation, detects design errors and potential defects before development e orts, avoiding re-engineering costs and making the system more robust and safe. This rst 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 { De nition of extensions for the design of speci c 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 Certi cation (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.
Keynote
Carnegie Mellon Software Engineering Institute 5 years ago the SAE AS-2C subcommittee started to work on the Architecture Analysis & Design Language (AADL) standard. AADL was targeted to address issues in mission and safety critical software-reliant systems, aka. Cyberphysical 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 architecture design, while 80% are discovered post-unit test. After a short history and summary of the challenges, the presentation highlights the expressive, analytical, 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 presentation 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 incremental verification and testing throughout the life cycle as assurance evidence. Peter Feiler is a 29 year veteran and Principal Researcher of the Architecture Practice (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 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 contracts 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 incremental and flexible application of specification and verification instead of requiring an all-or-nothing approach. It also helps improving the product 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
modeldriven approaches are often used. Such approaches often rely on modelling and
architecture description languages such as the Architecture Analysis and Design
Language, AADL [
Complex patterns of interaction between components pose a challenge to developers, making it difficult to understand how a system behaves and whether it satisfies its requirements and behaves correctly, e.g., satisfying safety and liveness constraints. In order to provide some relief to the developer, automatic formal verification techniques such as model-checking can help to analyze a system’s behaviour. Nevertheless, formal verification often faces the so-called stateexplosion 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 Centres of Excellence and Connect Canada.
An approach to deal with the state-explosion problem is the use of compositional 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 contracts where each component is annotated with a contract consisting of an assumption specifying how the component expects its environment to behave, and a guarantee specifying the behaviour guaranteed by the component if the assumptions 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 component whose contract conforms to or refines the first. Contract-based analysis uses the contracts to automatically establish whether a composition of components satisfy the contract of the composite component to which they belong.
Most approaches to assume/guarantee analysis (e.g., [
In this paper we address these shortcomings by we proposing an AADL
annex sub-language for annotating components with assume/guarantee contracts
and a prototype verifier that performs compositional analysis. In this
sublanguage we use the Property Specification Language, PSL, an IEEE Standard [
Another shortcoming of many formal approaches to analysis is that they
usually require an all-or-nothing commitment on the part of the developer, for
example 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 [
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
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 keyword). 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 **}; 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. 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;
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 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 possible 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;
An AGCL annex can contain multiple contracts, which can be verified independently. This allows the developer to add contracts as the design progresses, and define contracts which focus only on particular aspects of interest.
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 whenever 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 subcomponents 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: 1. G0 ⇒ G where G0 d=ef G1 ∧ G2, and 2. A ⇒ A0 where A0 d=ef (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 G0 d=ef G1 ∧ G2 ∧ · · · ∧ Gn and A0 d=ef ∧in=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;
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 K0 (or T 0) has contract C0 = (A0, G0) and it extends K (resp. T ) with contract C = (A, G), then conformance 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
between 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
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
machine. 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
specification from such state machine using standard transformations (e.g., automata to
regular expression, [
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 ([
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. 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 periodic 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 outlined 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 viewpoint or by component. When the result of a particular analysis fails, a counterexample is generated by the model checker. Our plug-in uses the NuSMV modelchecker 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 modelchecker 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 transitions 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 between 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
untractable, 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.
We have sketeched an approach to specify and verify assume/guarantee
contracts 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 [
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 methodology 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 syntax 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
safety, reliability and performance requirements. These systems have traditionally 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 hardware resources leading to mixed-criticality systems. Moreover, IMA architectures are distributed using a communication infrastructure, which should also be able to meet the same level of safety and performance requirements.
used as infrastructure for classic office systems but is increasingly supporting
industrial and embedded systems due to the high bandwidths it provides.
However, 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 [
architectures interconnected using TTEthernet. The advantages of this infrastructure 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 different performance and reliability requirements. However, these systems are on the other hand complex and the integration of diverse applications with mixedcriticality levels having strict real-time requirements is very challenging. In order to control the complexity of such systems, a model-based approach, which provides 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 sophisticated formal analysis techniques to verify safety and performance properties of the system.
time critical systems. AADL has been extended to support the modeling of IMA
with an Annex ARINC 653 [
a metamodel for the domain of IMA and TTEhernet. We provide a concrete
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 __|_|___|._||__|....|__|____|. _|_|_|....|_____||.._|____||.. |_____||..___||___|.__|_||.... 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 minimum 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 Asynchronism 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 simulation.
The following example shows how an event can dynamically influence the behavior 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 .|||||.....|||||.....|___|||| 1 : number of events in the incoming port queue. Caption: 3
Virtual Execution of AADL Models
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 [
For Real Time analysis, two plugins are currently embedded in AADL Inspector:
Cheddar [
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 transformation so that it can be processed by Marzhin, and to pilot its virtual execution through a control panel. 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 providing an immediate feedback showing the coarse grain dynamic behavior of the system during the design phases.
Finally, the specific technical approach that has been chosen for the implementation 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 aspects 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. 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 analysis, 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 [
The future improvements that are foreseen for this activity concern a more complete 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. 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 supported by the architecture but also explicitly represented. The Common Variability Language (CVL) allows to represent such variability independently of the Architecture Description Language (ADL) and to support the resolution of this variability for the automatic derivation of AADL product architectures. This paper presents a multimodel approach to represent the relationships between the external 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 account functional and non-functional requirements. 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
developed from a common set of core assets in a prescribed way [
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
architectural variation points [
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.
Although AADL [
To tackle this problem, in previous works, we presented the quality-driven product
architecture derivation, evaluation and improvement (QuaDAI) method [
The Common Variability Language (CVL) [
In this paper, we extend the multimodel approach to incorporate the explicit representation 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 attributes. Once the application engineer has selected the features and non-functional requirements (NFRs) and the priorities of the quality attributes that together conform the product 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 presents 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
development of system families (e.g., multiples implementation of a system specification,
component extension or the configuration support through alternative source code files)
[
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 features will form the CVL specification that will allow obtaining the COSMOS* architectural models. They do not define relationships between the external variability model (features model) and the architectural variability expressed in CVL and thus the derivation 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 models for a Train Control SPL that are defined using a DSL. They only consider the explicit 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 Reusable 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 models, the non-functional requirements, represented in the quality model, and the architectural variability, represented by using CVL allows us: i) To configure the product by using the feature model and the quality viewpoint; 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 transformations. 3
A Multimodel Approach for the Derivation of AADL Product Architectures QuaDAI is an approach for the derivation, evaluation and improvement of product architecture 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. The approach is illustrated through the use of a running example: a SPL from the automotive domain that comprises the safety critical embedded software systems responsible 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]. This SPL comprises several features such as Antilock Braking System, Traction Control 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.
[1.1]
ABS Attributes [0.1] [0.1] EstabilityControl Attributes
[0.1] CruiseControl Attributes [0.1]
FM_CD Attributes
VehicleControlSystem
Attributes [0.1]
FM_CD_Charger Attributes [0.1]
[1.1] MultimediaSystem
Attributes
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 represent 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 separation 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
expressing the commonalities and variability within the product line. Its main
element is the feature, which is a user-visible aspect or characteristic of a
system [
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
Common Variability Language (CVL) and its main element is the Variability
Specification (VSpec). We only represent in the multimodel the PLA
architectural variability, the PLA is represented in an AADL base model, which
is referenced by the CVL specification. A base model, under the CVL
terminology, is a model on which variability is defined using CVL [
CVL Variability Specificaiton Tree
ControlSystem Wheel Sensor
ABSSystem Variability Points
:ObjectExistence :ObjectExistence Base Model Wheel Sensor Brake Actuator
Pulse Brake_signal
ABS Control System
Braking_pedal_sensor Wheel_sensor
Brake_actuator_signal
:ObjectExistence Distance Sensor
Object_distance
Speed
Range :ObjectExistence :SlotValueAssignment :ObjectExistence
DistanceSensors Frontal Sensor Rear Sensor range: int
Doppler Sensor
Distance
Architectural variant :ObjectExistence Variation point nature Doppler Sensor
Distance AADL model element
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 positive 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 which variation points should be resolved positively in the CVL resolution model driving the derivation of the AADL product architecture.
Feature
ABS Attributes Quality Attribute
Qj Memory Consumption
Non-Functional Requirement
NFR_i <<is realized by>>UserSafetyLevel1
v <<Impact>>
Feature
ABS Attributes
Quality Attribute
Qj FaultTolerance
Relationships Used during Derivation Architectural Variation Point Non-Functional Requirement
WRhoetaetlRioontSaetinosnoSre.. <<is realized by>> MaturNiFtRy_iLevel Architectural Variation Point Feature
WheelRotationSe.. ABS RotationSensor <<is realized by>> Attributes v ArchiteWchtueerlaRloVtaatiroinaSteio..n Point
RotationSensor <<Impact>>
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 product 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].
1
Product
Product requirements ni in
Application engineer
Multimodel Variability Quality Architectural viewpoint viewpoint viewpoint Obtain Product out
Consistency validation in
Valid
No
Yes in 2.1 2 Architecture instantiation
Application architect
AADL CVL PL architecture transformation
in in CVL resolution model
AADL Product architecture CVL regseonleurtaiotinonmodel in out in
Product architecture instantiation out
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 derivation 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 fulfills 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 the impact and constraint relationships among them defined in the quality viewpoint). Once the intra-viewpoint consistency is satisfied we check the inter-viewpoint consistency (i.e., whether the configuration satisfy the is_realized_by and impact relationships 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 configuration and the multimodel (i.e., the relationships between the architectural viewpoint with variability and the quality viewpoint) and, through a Query View Transformation (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 configuration. 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 generation and the AADL Product architecture instantiation.
LaTtQiemanecy impacRtotation Sensor Fig. 5. AADL Product Architecture Instantiation
Brake Actuators
CVL transformation Product architecture instantiation
AADL Product Architecture ABS Control System
Brake_pedal_signal Rotation_sensor_signa
Brake_actuator_signal
Brake_actuators
Brake Signal 3.4 The approach is supported by a prototype2 that gives support to the configuration, consistency 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 checking are carried out through OCL constraints checked at runtime by the OCLTools validator. 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, TractionControl, StabilityControl and FM_CD} (see Fig. 1) and the NFRs configuration nfrs={EuroNCAP3}.
Finally, with the integration of the CVL supporting tool [24] the CVL transformation can be called so as to generate the resulting AADL product architecture. 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.
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 multimodel, 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 configuration, 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 powerful 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 language 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 10. 11.
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´en´eral 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 approaches 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 modelbased 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 embedded software systems, in an early design phase. We thus expect to improve and enhance Correct By Construction in the design. The considered 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
specification, design by contract, semantics interoperability
1
Current embedded systems are increasingly more complex and heterogeneous,
but they are expected to be more safe, reliable and adaptive [
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 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 semantics interoperability for models to be integrated in the system. The application domain of our approach include avionic and automotive systems.
dress the system complexity issue [33]. High-level modeling languages, such
as UML[27], SysML[
modeling for avionic and automotive systems. AADL provides an industry standard, textual and graphic notation with precise semantics to model applications and execution platforms and is supported by commercial and open source tool solutions—including Open Source AADL Tool Environment (OSATE) [28].
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[
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 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 design has been explored in [37] [36], where AADL was used to model the architecture 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 order 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
Polychrony provides model transformations from AADL and Simulink (via
GeneAuto[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
connection. Model-based system integration has also been discussed in [34] with
regard to cyber-physical systems, [
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
optimization enabling, easy access to current matured software development tools and
environment, etc. With this objective in mind, we first propose a model-based
architecture-centric virtual integration approach, in the framework of
modelbased systems engineering [11], for the design of next-generation automotive
systems. This approach is involved in mostly correct by construction
technologies, 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:
timing specification [
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 architecture is considered and the system is integrated, due to the gap between software and architecture design. In our project, we consider high-level, formalized timing constraints to be defined, observed and analyzed based on software architecture, specified in AADL. From this point of view, an architecture centric 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 submission 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 specifications 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
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
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] [
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
solutions 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
translation, which is not practical in most cases. Another solution is related to formal
semantics interoperability. Some work can be found in [
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 corresponding research topics was also presented. We, hence, propose a model-based architecture-centric integration approach, considering timing specification, design 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 automotive systems.
Acknowledgment
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. SangiovanniVincentelli. Composing Heterogeneous Reactive Systems. ACM Transactions on Embedded Computing Systems, 7(4), 2008. 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. Proceedings 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.estereltechnologies.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 International 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´ez´equel and B. Meyer. Design by Contract: The Lessons of Ariane. Computer, 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 Models 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. 24. P. J. Mosterman and H. Vangheluwe. Computer automated multi-paradigm modeling: An introduction. SIMULATION: Transactions of the Society for Modeling and Simulation International, 80(9):433–450, 2004. 25. K.D. Mu¨ller-Glaser, G. Frick, E. Sax, and M. Ku¨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´e Schiele, and Thanassis Tsiodras. TASTE: A Real-Time Software Engineering Tool-Chain Overview, Status, 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 CyberPhysical 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. Polychronous Modeling, Analysis, Verification and Simulation for Timed Software Architectures. 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.