P Baudin

D Delmas

S Duprat

B Monate

Proving Temporal Properties at Code Level for Basic Operators of Control/Command Programs

Keywords: formal verification, theoremproving, static analysis, CAVEAT, embedded software

More and more control/command software is being generated automatically from highlevel graphical specifications. Such specifications are typically synchronous dataflow models, built on a set of external basic operators to be implemented in a lowerlevel language. The semantics of the overall model depends therefore on the semantics of the basic operators, which can be expressed in terms of temporal (inductive multicycle) definitions. In this paper, we describe a way to specify and verify these operators formally, using theoremproving techniques. We report on experiments conducted to prove multicycle properties on actual embedded basic operators written in C, using the CAVEAT static analyser with a dedicated method.

Introduction

Context

Many control/command programs, such as flybywire control software, as well as some other embedded reactive systems, are currently being developed in a modelbased approach. Most of their source code is generated automatically from highlevel synchronous dataflow specifications. As a consequence, their overall structure is the following: initialise state variables; loop forever read volatile input variables, compute output and state variables, write to volatile output variables; wait for next clock tick; end loop

The computations to be performed are described by system designers at modellevel in a graphical stream language such as SCADE™ or Simulink®, by means of external basic blocks. The semantics of the overall model relies therefore on the semantics of the basic operators. Designers only need to know their specifications, which are often expressed in terms of informal inductive definitions. These definitions are multicycle properties that describe the (discretetime) temporal behaviour of the operators with respect to the synchronous clock. The actual operators can be either provided together with the modelling tool, or implemented by the user in a lowerlevel programming language, for him to meet his specific needs exactly. The latter case occurs typically for safetycritical embedded avionics software to be certified according to the DO178B/ED12B international standard. Wellknown techniques are available to verify and validate designs at modellevel, e.g. modelchecking and simulation. Such Verification & Validation activities require systemlevel models for all basic blocks, and their results are only valid with respect to these models. For this kind of V&V to be considered representative with respect to the behaviour of the final generated program, one needs to be sure that each basic operator has the same semantics as the associate model. The traditional way to address this objective is to verify that each basic operator complies with its informal specification, by means of unit testing. However, this approach is both costly and unsound. In this paper, we describe an alternate way to verify these operators, based on theoremproving techniques. We report on experiments conducted to prove multicycle properties on actual embedded basic operators written in C, using the CAVEAT static analyser with a dedicated method. Then we state the successes obtained, and the limits of this approach, e.g. regarding potential runtime errors, accuracy of floatingpoint computations and functional correctness of the compiled program. Finally, we give complementary approaches currently investigated to address these issues for the complete program, by means of other specialised static analysis tools. The general form of the definition for the operator is:

S[0] = F 0 (E[0]) S[1] = F 1 (E[0], E[1]) ... S[N-1] = F N-1 (E[0], E[1], ..., E[N-1]) for all k N: ≥ S[k] = F(E[k-N],..., E[k-1], E[k])
In some cases, expressions involving previous outputs are used:

for all k<0: S[k] = 0 for all k N: ≥ S[k] = F(E[k], S[k-N],..., S[k-1])

Overview of the CAVEAT tool

The CAVEAT ([2]) static analyser is being developed by CEA LIST. It is a verification tool for programs written in a subset of the ISOC language. Being qualified as a verification tool according to DO178B/ED12B, it has been used industrially at Airbus for several years, in order to verify a 30000 line embedded software subset formally, instead of performing traditional unit testing ( [START_REF] Duprat | Formal verification workbench for airbus avionics software[END_REF]). CAVEAT aims at translating a C program and its formal specification into a set of firstorder logic formulas named "proof obligations" (POs). POs are generated thanks to a weakest precondition calculus "à la" FloydHoare ([1]). Therefore, the validity of the POs implies the conformity of the code to its specification. To establish the validity of the POs, a combination of automated theorem proving techniques and manual assisted formula transformations are being used. Fully automatic theoremprovers are known not to be very efficient at deciding inductive properties, and CAVEAT does not provide any direct support for inductive proofs. However, CAVEAT offers the possibility to define recursive logic functions, known as "lambda functions". No automatic proof strategy is available on these symbols, but bounded applications can be performed interactively. Formal specifications are described by properties inserted at specific program points. In order to introduce the different types of properties that can be proved with the tool, let us give a simple example of C function:

void div(int a, int b, int *q, int *r) { *q = 0 ; *r = a ; while (*r >= b) { *q = *q + 1 ; *r = *r b ; } } This integer division algorithm computes the quotient and remainder (q,r) of two positive integers a and b, such that a À b.

Let us write a formal specification for function div, inserting different types of properties at different program points:

• Preconditions: these properties are to be attached to the declaration of functions and give a formal relation between the formal arguments and the global variables. Preconditions are assumed to be verified whenever the function they are attached to is executed and are to be checked at each of its call sites. Preconditions for function div are: CAVEAT also has support for the following global properties:

• Logical definitions: logic functions can be defined and used to factorize repetitive formulas. They are denoted like in the following examples:

Const succ Ö int -> int = lambda x Ö int . x + 1 ; Const is_even Ö int -> Boolean = lambda N Ö int.
(N = 2 * (N div 2)) ;

• Tautology declaration: specific predicates can be declared to be always true, regardless of any specific program point. They can be used as lemmas to help the proof process, or as means to ensure the completeness of the formal specification. These properties are denoted as follows:

Always my_tauto : is_even(a) Î is_even(succ(a)) ; Many other kinds of properties are available in CAVEAT, but only the above properties are used in the present article.

A method to deal with multicycle properties

Practical setup

Overview

Let us describe a case study on a widelyused temporal operator: the "CONF" input confirmation operator, aiming at triggering an action only after some stimulus has been active for long enough.

CONF E 1 E 2 S 1

Functional requirements

An informal specification of this component is: "S 1 is on if and only if E 1 is on and has been on for the last E 2 ticks of the synchronous clock."

Figure 2 shows possible behaviours of the CONF operator with parameter E 2 =2.

Figure 2: a CONF timing diagram Let k≥0 be the current value of the synchronous clock, and

E 1 [k] (resp. S 1 [k]) be the value of E 1 (resp. S 1 ) at time k. Thus, S 1 [k] depends on E 1 [k], E 1 [k-1], ..., E 1 [k-E 2 ].
More precisely:

S 1 [k] = E 1 [k] Ï E 1 [k-1] Ï...Ï E 1 [k-E 2 ]
assuming the following convention:

E 1 [i]=0 for all i<0

Implementation constraints

The CONF operator is implemented in a C macro function with the following interface:

#define CONF(E1, E2, S1) Two hypotheses can be used to write the code for this operator:

1. The CONF operator is executed once at every tick of the synchronous clock;

2. all RAM variables have been initialised to zero before time k=0.

Proof Environment

As the informal specification of CONF refers to a synchronous execution model, we need to set up a representative environment. Therefore, we build our proof project as a C source file where the CONF macrofunction is being used inside the body of an infinite loop. The loop counter represents the synchronous clock. Besides, we need to store input/output values at all clockticks into history keeping variables. We use arrays for this purpose. Finally, as the CAVEAT tool is designed to prove properties on C functions (as opposed to macro functions), we use a function wrapper for the CONF macro.

void conf_iterate(void) { int i=0 ; while (1) { conf_call(i); i++; } } extern int E[], S[], NB; void conf_call(int k) { CONF(E[k], NB, S[k]); }
In the above C source file:

• the conf_iterate main function implements the infinite loop;

• the intermediate conf_call function is a wrapper for the CONF macrofunction;

• E 1 [k] (resp. S 1 [k]
) is stored in the element at offset k of the E (resp. S) array.

Formal specification

We may now formalise the specification of the CONF operator in terms of preconditions and postconditions of the conf_call wrapper, using the E and S history arrays as formal operands.

To do so, we separate the set of possible "use cases" of the operator into three disjoint conditions: We notice that these three conditions are combinations of two atomic propositions:

1 the current input E[k] is off; 2 E[k] is
a) The current input E[k] is on;

b) E has been on for NB clock ticks or more.

The former may be expressed directly, using the element at offset k of the E history array:

LET SUBCOND_INPUT_ON = (E'.[.(k)] Ä 0) ;
For the latter however, we need to create a formal expression that represents the number of ticks for which E has been on. We do it using the following recursive lambdafunction:

Const NB_CYCLES_ON Ö Tab&int -> int -> int = lambda input Ö Tab&int, n Ö int. if (n à 0) then 0 else( if (input.[.(n-1)]=0) then 0 else (1 + NB_CYCLES_ON(input, n-1)) );
The NB_CYCLES_ON function has an array input (input Ö Tab&int) and an integer input (n Ö int), and it returns the number of adjacent nonzero array elements before index n. We may visualise the value of NB_CYCLES_ON(E,k) on Figure 3. We may now express conditions 1, 2 and 3 formally:

LET COND_INPUT_OFF = ÕSUBCOND_INPUT_ON ; LET COND_INPUT_CONFIRMED = SUBCOND_INPUT_ON Ï COND_TIME_REACHED ; LET COND_INPUT_NOT_YET_CONFIRMED = SUBCOND_INPUT_ON Ï ÕCOND_TIME_REACHED ;
To make sure this specification is complete and unambiguous, we may also ask the tool to prove that:

• no execution condition is forgotten:

Always COND0 : COND_INPUT_OFF Î COND_INPUT_NOT_YET_CONFIRMED Î COND_INPUT_CONFIRMED ;
• conditions 1, 2 and 3 are exclusive: Recalling the E 2 constant parameter for the CONF operator is a nonnegative integer, we also define a precondition on the wrapper function:

FONCTION conf_call Pre COND_VAR1 : NBÀ0 ;

Formal Proof

Our goal is now to prove the three postconditions on conf_call. We thus run the CAVEAT tool on the formal specification and on the following implementation of the CONF macrofunction: On the other hand, RES_CONF2 and RES_CONF3 cannot be proved directly, unless some more properties are introduced. For both, we need to tell the tool about an implicit relationship between the value of the static count variable and the history of inputs: this variable stores the number of clock ticks for which E has been on. This fact can be expressed via the NB_CYCLES_ON lambdafunction that we have defined earlier:

#define CONF(E1, E2, S1)\ {\ static int count;\ \ if (
FONCTION conf_call Pre COND_SET1 : count=NB_CYCLES_ON(E, k) ;
In turn, this precondition for the conf_call function must be proved to be respected in its synchronous execution model. The way to do it is to make CAVEAT check this property results from a loop invariant of the the conf_iterate main function.

We therefore claim the following invariant for the main loop:

FONCTION conf_iterate Inv 1 I1_SET1: count=NB_CYCLES_ON(E', i) ;
This property holds because of an implementation hypothesis : all RAM variables have been initialised to zero before time k=0. Consequently, we need to add the following toplevel precondition:

FONCTION conf_iterate Pre H_INIT_RAM_0 : count=0 ;

For the tool to be able to prove the invariance of I1_SET1 in conf_iterate, it also needs to know about an extra postcondition of conf_call:

FONCTION conf_call Post ALGO_SET1: count=NB_CYCLES_ON(E, k+1);
Let us recall the complete formal specification :

--Definition of the number of clock ticks --for which the input has been on We also recall the additional properties: All these properties are proved with the CAVEAT tool.

Const NB_CYCLES_ON Ö Tab&int -> int -> int = lambda input Ö Tab&int, n Ö int. if (n à 0) then 0 else( if (input.[.(n-1)]=0) then 0 else (1 + NB_CYCLES_ON(input, n-1)) );
Figure 4 shows the dependences between postconditions, preconditions and invariants in the proof process. The arrows mean "can be proved thanks to".

Results obtained

Among the different types of basic operators defined in §1.2, the CAVEAT tools allows:

• automatic proofs on pure boolean/integer operators;

• semiautomatic proofs on pure temporal operators, using the same methodology as with the CONF case study;

• semiautomatic proofs on various combinations thereof.

Theoretical background

The CAVEAT tool is based on Hoare logic, which uses Hoare triples to reason about program correctness. The triple {P} code {Q}, where P and Q are predicates, means: "if P is true before execution of code, then Q will be true when execution of code is finished". Figure 5: Dependences between properties When there is a loop as here, the proof scheme may be invalid: if P relies on Q and Q relies (directly or not) on P, no valid proof has been found. In fact, there is also a whileloop inside the code of function conf_iterate, and proving the partial correctness of loops with invariants is very similar to proving the correctness of recursive programs via mathematical induction.

The tool is able to prove the following Hoare triple: {Pre l } code of conf_call {Post l } That means the validity of Post l relies on the validity of Pre l , which gives the conditions of use of the function conf_call.

The loop invariant of conf_iterate ensures that the precondition of conf_call holds for all iterations of the loop: {Inv 2 } jump to entry point of conf_call {Pre l } So, the respect of the conditions of use of the function conf_call relies on the correctness of the loop invariant. Like in a proof by induction on the number of loop iterations, the proof of the invariant is decomposed into two proof obligations (PO): 1. one PO to show the invariant is stated; 2. one PO to show the invariant is maintained.

Limitations and complementary approaches

Typical control/command programs use a lot of numerical operators.

Unfortunately, CAVEAT provides very limited support for floatingpoint computations. It cannot be used so far to derive sound proofs of properties of numerical operators. That is the reason why we are considering improving the tool to fully support floatingpoint numbers, with the semantics of mathematical real numbers only (precision issues will not be addressed). This will make it possible to analyse C functions performing floatingpoint computations, provided some complementary numerical precision analysis is carried out. This analysis will be performed with the FLUCTUAT ( [START_REF] Goubault | Static AnalysisBased Validation of FloatingPoint Computations[END_REF]) abstract interpretation ( [START_REF] Cousot | Basic Concepts of Abstract Interpretation[END_REF]) based static analyser, a dedicated tool for studying the propagation of rounding errors in floatingpoint computations. On the other hand, most operators can only be accurate with respect welldefined limited input ranges. For instance, multiplicative operators may yield floatingpoint overflows when used on incorrect inputs. As a consequence, we need to prove the complete program free from such runtime errors, as well as compute maximal input ranges for all operators, for our proofbased approach to be sound. The Astrée ( [START_REF] Cousot | The ASTREE analyser[END_REF]) abstract interpretation based static analyser has been shown to meet this ambitious objective on realworld control/command programs ( [START_REF] Delmas | Astrée: from Research to Industry[END_REF]). Moreover, all these analysis techniques work on C source code. They cannot replace testing completely, unless the subsequent compilation process is also proved correct. We are therefore working on a translation validation technology: prove that the source and the compiled program have the same semantics ( [START_REF] Rival | Symbolic Transfer Functionbased Approaches to Certified Compilation[END_REF]). Finally, it has to be proved that every instance of each temporal operator is actually used in a synchronous execution model, ie that the program can always be run completely on every tick of the synchronous clock. We thus use another static analysis tool to compute a safe and precise upper bound of its worstcase execution time ( [START_REF] Souyris | Computing the worstcase execution time of an avionics program by abstract interpretation[END_REF]).

Conclusion and future work

The experiments described in this paper show that the CAVEAT static analyser can be used to prove multicycle properties on basic operators of realworld embedded control/command programs. Moreover, this work has been an opportunity to sketch a proof methodology that makes it possible for nonexpert engineers from industry to perform this formal verification activity in a rather straightforward way. On the other hand, some work remains to be done for this proof technique to yield sound results on all types of operators: we need several complementary static analysis techniques to join forces. However, most necessary technologies are already available, and the rest will soon be. We will then be in a position to replace all (unsound) testing with (sound) static analysis for most basic operators.

Pre my_precond1 : b > 0 ;

 0 Pre my_precond2 : a À b ; • Postconditions: these properties are almost like preconditions but for the semantics. For all values of global variables and formal arguments that fulfil the precondition, postconditions must hold at the end of all normal executions of the function to which they are attached. Moreover, at each call site of the function, the postcondition is assumed. Postconditions for function div are: Post my_post1 : r.[*] < b ; Post my_post2 : a = b*q.[*] + r.[*] ; • Loop invariants: these properties are attached to loop bodies in functions, and may give formal relations between all visible program variables. They must hold at the beginning of the loop body they are attached to. Besides, each execution of the loop body has to preserve the property. Invariants for the loop number 1 of function div are: Inv 1 my_inv1 : r.[*] À b Ï b > 0 ; Inv 1 my_inv2 : a = b*q.[*] + r.[*] ;

Figure 1 :

 1 Figure 1: Interface of the CONF basic block As shown on Figure 1, this operator has the following interface: E 1 : boolean input variable; E 2 : nonnegative integer constant parameter; S 1 : boolean output variable.

Figure 3 :

 3 Figure 3: visualising function NB_CYCLES_ON on a CONF timing diagram Let us formalise proposition b) with NB_CYCLES_ON: LET COND_TIME_REACHED= (NB_CYCLES_ON(E',k) À NB);

  Finally, let us express the postconditions for the conf_call wrapper:

  of all execution conditions --for the CONF operator LETSUBCOND_INPUT_ON = (E'.[.(k)] Ä 0) ; LET COND_TIME_REACHED= (NB_CYCLES_ON(E',k) À NB);

  : count=NB_CYCLES_ON(E', i) ;

Figure 4 :

 4 Figure 4: Dependences between properties

Figure 5

 5 Figure 5 recalls the dependences between properties of figure 4, abstracting away the details of the CONF case study. It shows the way we prove multicycle properties on temporal operators.

  The precondition of conf_iterate guarantees the truth of Inv 2 the first time execution reaches the loop body:{Pre 2 } code from the beginning of conf_iterate to the while-loop {Inv 2 } That is the base case. Then, the invariant has to be maintained by the execution of the loop body. The inductive case {Inv 2 } loop body {Inv 2 } shows that if Inv 2 holds after k-1 iterations, then it also holds after k iterations. It can be decomposed in three Hoare triples: 1. {Inv 2 } jump to the entry point ofconf_call {Pre 1 } 2. {Pre l } code of conf_call {Post l } 3. {Post l } return from conf_call ;increment loop counter {Inv 2 } So, the dependence loop of Figure5is, in our case, sound. The proof of the postconditions of conf_call is valid for all values kÀ0 of the underlying synchronous clock.

1

  Hoare, C.A.R. An axiomatic basis for computer programming. Commun. ACM 12(10), pages 576580, 1969. 2 Patrick Baudin, Anne Pacalet, Jacques Raguideau, Dominique Schoen, Nicky Williams. Caveat : A tool


S Flores

P Le Meur

J F Renneson

Simulatorbased testing environment for avionics software: a feasibility study

Keywords: Integrated modular avionics, simulation, embedded software testing

published or not. The documents may come

Simulatorbased testing environment for avionics

software: a feasibility study

Introduction

Background

Embedded software development involves thorough testing phases. In the avionics industry the means of testing become almost as critical as the tests themselves because the whole development process is subject to certification by air navigation authorities, using the DO178B standard. This standard defines a set of criticality levels according to the consequences of a software failure, from level A (catastrophic consequences) to level E (no effects). A typical development cycle of airborne software includes unit and integration testing phases in which hardware targets are used to execute the tests. These hardware targets are the central part of the testing platforms that we currently use, named TargetBased Operating System Simulation (TBOSS). The TBOSS targets simulate an IMA airborne calculator and the operating system on it, and even though some of their components are not the same as those in the aircraft, certification authorities have controlled their representativeness.

Unfortunately, good representation comes at a price. Application developers are often very limited in essential aspects of the testing process such as debugging or even the physical availability of the testing platforms due to the small number of hardware targets. In our industrial environment in particular, we will also have to deal with other problems such as the lifespan of the hardware, the cost of licensing of the tools, and the technological dependence to the providers of the testing platform.

All these reasons made us consider the possibility of developing a new testing platform based on an existing IMA structure software simulator. This simulator called Software Workshop for IMA Modules (SWIM) is currently used by another entity in our organisation to validate flight calculators by integration test benches. It is also part of full flight simulators that are employed for pilot training. SWIM provides a given airborne application with an emulated behavior of its environment as if it interacted with its real operating system and underlying hardware. In the IMA architecture, the means of interaction with the operating system are defined by the ARINC 653 standard, which is thus implemented by SWIM. This simulator recreates the realtime behavior of a single IMA processing unit (CPIOM) and of the operating system that controls it (MACS2). This makes SWIM a host structure capable of executing complete IMA applications on a GNU/Linux operating system.

On the other hand, software unit and integration tests are a very controlled execution of a few components of the final application. In this tests several conditions such as time, return codes or initial values are often simulated or forced.

Our reasoning is that a simulator capable of executing complete applications might also be able to run verification tests of each one of their components, even though it was not designed for such a purpose, and even though the tests differ from complete application in many ways.

Motivation

A testing platform based on SWIM would be completely softwarebased, which would allow us to make it more available to developers (by simply copying it or launching several instances) than the hardwarebased platforms. The whole testing process would become easier and faster as there would not be a need to compile and load configuration sources for each test. In the long term, greater debugging features could be added to the new platform because we would have access to all of its source code; which would also allow us to use it without paying any license fees, or even to adapt it to our particular needs. Finally, creating our own testing platform would give us a better control of the testing process. This becomes increasingly important as we do not want to depend on a single provider of testing platforms.

Constraints

There are nonetheless some very important constraints to take into account. The first and most important is that the simulatorbased testing platform must be backwardscompatible with the previous one. This is an essential requirement to a full scale migration because there are several thousands of existing tests that support the reliability of different avionics applications currently in service, and modifying them would imply an enormous effort. This means that we must adapt the new simulator based testing platform to the existing tests and not the contrary. The execution of these tests should have the same results in both hardware and simulatorbased platforms and should be generated from the same sources.

The testing interface should remain the same to the application developer, so that the eventual migration is transparent to them.

We also want to keep modifications to SWIM to a strict minimum, as we wish to be able to evolve with the original simulator and take advantage of eventual new features.

Feasibility and problems

To all this constraints we add the fact that SWIM was not originally made to fulfill our testing needs.(mainly unit testing and integration testing for software verification).

Due to the complexity of the current hardwarebased platform and to the strong constraints we face, we decided to evaluate the feasibility of a total migration to a simulatorbased platform by creating a prototype of this platform. This prototype helped us:

• to identify the potential problems of the migration • to anticipate to these problems and to take into account their solutions from early stages of the creation of the new platform • to foresee any blocking conditions and eventually to decide about the feasibility of a full migration to the new platform.

The first part of our project was to identify the differences between the execution environments in SWIM and in the hardware targets. We present them here as a means to expose the problems that made us question the feasibility of a full scale migration.

Main purpose: the TBOSS targets were designed to test a single component of an application with representativeness being the most important feature. The ability of the application developer to simulate API calls is also important as it allows him to easily test different scenarios, for example forcing the execution of a certain branch of code. SWIM on the other hand was made to be the first simulation platform of complete IMA applications (as opposed to just components), providing them with all necessary operating system access services and behavior.

Executable Format and configuration: the TBOSS targets use the executable and linking format (ELF) for the PPC 755 processor. A single executable must be built outside the target and then loaded to it. The executable is constituted of a binary image of the system software (MACS2 OS and other drivers), a binary image of the application software (the test), a boot loader that copies everything in the right place on memory, and a binary image of the configuration table (configuration parameters for the MACS2 OS, drivers, RAM and communication means). Of course; we need to recompile the sources of most of this components for each test.

SWIM in contrast is an executable itself. Applications are loaded at runtime in the form of ELF shared objects (dynamicallylinked libraries). These shared objects just contain the application as the system software is provided (or rather emulated) by SWIM. All configuration in SWIM is done by regular files. One of the XML configuration files is particularly important because it describes the period used by the OS simulation's scheduler, the shared objects to be loaded and the communication channels to be used.

Communication Channels: An important term regarding communications in IMA applications is APEX port. These ports are the main internal communication mechanisms between IMA partitions, processes and external devices. If we must exchange information with an executing IMA application, we must connect with the APEX ports in some way. TBOSS and SWIM take different approaches to this. TBOSS targets use a set of tools to upload the executable into memory. Aside form this, all communication in and out the target is made by a special interface that lets us implement control programs by including a C header file and a static library. We will cover this in more detail later. We do not have access to the source code of any of these tools.

SWIM does not impose any means of communication : it just provides a communication interface. SWIM users can implement the communication stack the way they want, and compile it as a dynamic linked library. In fact, the current users of SWIM generate the code of this stack automatically from files describing the external interfaces of the hosted avionics applications.

Execution sequence: TBOSS targets execute applications 'stepbystep' in a basis of a period called minor frame (MIF). Roughly, this duration represents the minimal configurable time duration of the OS scheduler. As we will explain in further detail later, the execution of each MIF is conditioned to the reception of a specific command from the user. SWIM on the other hand executes applications continuously during a predefined (but configurable) number of MIFs. The execution will continue without stopping until this number of MIFs is reached.

Representativeness: the TBOSS targets ensure that the compiled code will behave as in the airborne calculators because it uses the real MACS2 OS, a very similar processor and a very similar memory scheme; as opposed to SWIM that executes on Intel x86 processors and just emulates the behaviour of the MACS2 OS on a GNU/Linux System.

Methods

In this section we present the development of our prototype as well as the problems we encountered, the solutions we implemented and the validation strategy. For simplicity, we will call our prototype and the existing hardwarebased platform 'the SWIM platform' and 'the TBOSS platform' respectively.

Imposed Architecture from TBOSS

As stated in section 1.3, a major requirement for a new simulatorbased testing platform is its capacity to execute existing tests without modification. This imposed a certain architecture to the SWIM platform as we needed to determine if we could reuse some of the components of the TBOSS platform. An overview of the architecture of the latter is shown in figure 1.

Figure 1. An overview of the TBOSS platform

In this architecture, the tests (1) are executed in a target which has no means of communication with the external world but a control interface (2) called 'Operating System Simulation Control Interface' (OSSCI). A set of programs (3) running on Solaris workstations control the test exclusively through this interface. All the information exchanged between the execution of the test and the developer is also transmitted by the OSSCI. We can see this as a communication layer between the execution target (4) and the control host (5). Its implementation remains completely inaccessible to us, as the only source code provided is a C header file that establishes the signatures of eleven functions (OSSCI commands) which must be called by control programs in order to interface with the test. The platform also includes several other tools (6) such as launch scripts, configuration management and revision control facilities, preprocessors, post processors and report generators. These tools constitute an interface to the developers and thus should remain unchanged. Some of these tools are provided by the developers, some others by our department, and some others by third parties. We do not have access to the source code of all of them.

Architecture of the SWIM Platform

The creation of the SWIM platform consisted of three main tasks:

• the implementation of a new OSSCI communication layer using a clientserver scheme.

• the implementation of the corresponding modifications on the original SWIM so that it would respond to the commands of the new OSSCI.

•

The integration of the new and ancient components. Of course, this tasks were not made sequentially but rather in parallel. We present the fundamental aspects of each one and then we present some interesting problems that we faced. The new OSSCI. It consisted in two static libraries, one to be linked to SWIM ('the server') and one to be linked to the control programs ('the clients'). We used an objectoriented approach to design this libraries. On the client side, we chose the simplest of the existing control programs to use within our prototype, simply linking it against our new client library and thus taking advantage of the hidden implementation of the OSSCI. We reimplemented some of the functions that allow a control program to interface with the test. Some others where not implemented because they were not immediately necessary for our feasibility study (as no control program used them). The details of the implementation of these functions are out of the scope of this document, but we would like to briefly highlight some of them:

• OSS_Init: initializes the hardware target and the OS. In our implementation it gets the current SWIM's APEX port configuration and establishes TCP/IP socket connections accordingly.

• OSS_Run: Asks for the execution of the test during a specified period of time. As we will explain more in detail later in this document, the fact that SWIM lacks this functionality made the reimplementation of this OSSCI command critical.

• OSS_End: Ends the execution of the test. In our implementation it closes all connections and frees temporary resources.

• OSS_Message_Input: asks for the transport of predefined messages from the control host to an APEX port in the application. We internally use TCP sockets to send these messages.

• OSS_Message_Output: asks for the transport of predefined messages from an APEX port in the application to the control host. We internally use our TCP sockets to send these messages. On the server side, the library executes its method serve to receive and treat the internal OSSCI messages that arrive from the client. Again, their implementation is out of the scope of this document but we highlight some of them: • serve: this method treats the received messages from the server and dispatch the corresponding actions, such as calling the methods above or continuing the execution of the test. We deliberately put this method at the end because we will talk more about it in the next section. Modifications on SWIM: as we previously stated, we wanted to keep SWIM free of modifications. But because SWIM was not originally designed to fulfill our testing needs, some modifications were necessary. We tried to minimize their impact by isolating them on a specific compilation option. The main change to the SWIM behavior was the inclusion of the OSSCI server's serve method call at the very beginning of the execution of each MIF. This method call is blocking, effectively preventing SWIM to continue the simulation of the test. Once in the method, the OSSCI server will wait for events and dispatch actions according to the messages from the OSSCI client. The method will not return until a special message sent by OSS_Run is received. This process can be seen in figure 2.

Figure 2. Simplified sequence diagram of a test

This modification to the SWIM behavior totally affects the realtime execution of the software. This is true because the execution of the applications (the tests) become synchronous to the arbitrary call of the OSS_Run function by the control programs. Nevertheless, this does not represent an obstacle to our purposes because the whole simulation is stopped upon the execution of the serve method, even the simulated flow of time. We achieve this by calling the serve method before any internal SWIM timer is initialized or incremented, so this suspension will not affect the effective execution time of the MIF. Integration of the components: as we explain in figure 3, the SWIM platform consisted in our modified version of SWIM in a GNU/Linux system (1) controlled by a Solaris host (2) through TCP sockets. The simplest of the control programs (3) was linked against our new OSSCI client library (4) which allows communication with the OSSCI server (5). The server itself has been incorporated to SWIM, that loads the shared object of the test (6) at runtime. It is important to mention that although we did not include all of the other components (7) of the ancient platform in our prototype, the interfaces to them were not changed. Until now, we have explained the architecture and the implementation of the SWIM platform according to the constraints we had. The next step was to test our prototype through validation tests. We will explain our validation strategy in further detail later, but first, we present some of the problems that we encountered during the testing phase and the steps we took to solve them. Differences between the executable formats in the TBOSS targets and SWIM: As we explained in section 1.4, SWIM and TBOSS take different executable formats. Our first problem to was to determine which sources to compile to generate the shared objects needed by SWIM. The build process itself was also very important because some tests made assumptions about the testing platform. For example, some tests could rely on the TBOSS hardware to clean certain areas of memory. Needless to say, these areas are not the same under the SWIM platform. The most interesting problem that we had, concerned the memory segment in which variables initialized to zero were stored. The default policy of the GNU C compiler (which we used to generate the shared objects of our tests) is to put variables that are initialized to zero into the BSS segment (the BSS segment is the memory zone in a process that contains the uninitialized global data structures). This can save space in the resulting code, but can cause problems with programs that explicitly rely on variables going to the data section. This was the case in some of our tests, and the result was that global variables explicitly initialized to zero had in fact different, random values. The solutions to all the problems related to different executable formats between SWIM and TBOSS was to carefully identify the necessary compiler options to generate machine code that would behave in the same way in both platforms. Endianness: The control host used in a TBOSS platform runs on Solaris/Sparc platforms. Besides, one of the control programs was specifically designed to be run on Solaris systems (it uses specific Solaris' shared memory mechanisms to communicate with simulated devices). Because of this, we decided to keep all of the control programs on that platform instead of porting them to GNU/Linux (which is the platform where SWIM runs). This brought some problems concerning the endianness of the data sent through the network: Solaris/SPARC platforms are bigendian while Linux/ia32 platforms are littleendian. The solution to this was simply to include proper treatment of the integers transmitted. Symbol resolution and overwriting: As we explained in section 1.4, TBOSS purpose is to be used in verification tests. The developer may want to force the execution of a certain branch within the tested code. To do this, developers use code stubs. These stubs are actually redefinitions of the functions called by the software undergoing tests. They exist to simulate the existence of the rest of an application for the specific part of software being tested. For example, if we are testing a module m and we know that m calls a function f (defined outside this module), we may want to simulate f so that we can force its return code to decide about something:

... // we know this code exists in the module m // which we are testing: rc = f(param1, param2, param3) if (rc == NO_ERROR) { // do something } else { // do something else } ... The developer just rewrites a very simple definition of f that returns the desired value instead of incorporating the code of the real f function into the executable. This is in fact very simple, but it becomes much more complicated when the developer needs to redefine a system call, like a service of the AIRBUS API (the ARINC 653 interface). Such service would then be defined twice in the same executable: once by the basic software (the OS) and then another time by the application's test. In practice, some of the tools of the TBOSS platform preprocess the sources to eliminate all duplicated symbols and obtain the desired effect (that of the developers' redefinition of the service). But we could not use the same tools for the SWIM platform because the execution environment is completely different. Only the interface between the components is the same. Every time that a test redefined a service of the ARINC 653 interface, we faced the problem of duplicated symbols in the execution of our tests in the SWIM platform. Because SWIM and its applications are compiled separately, no compiler warning was ever raised.

Besides, in a GNU/Linux system, the policy of the dynamic loader (the program that loads the shared object into memory) is simply not to load a symbol that has been already defined in memory, hence giving precedence to the first symbol and silently ignoring the second. The result was that many of the existing tests failed because they were calling the actual system service instead of the developer's stub. This problem is illustrated in figure 4. To overcome this obstacle we took advantage of the same dynamic loader policy. We slightly modified SWIM and its build process to encapsulate all the AIRBUS API services in a dynamic library. Then we forced the SWIM's main binary to load the shared object of the application before that of the system API, as seen on figure 5.

Validation Strategy

To validate our prototype, we took a subset (a module) of the Air Traffic Control software used on the A380 (ATC, a level C IMA application). The reliability of this subset is verified by several hundreds of unit tests, organized in 40 different groups. From each one of these groups, we generated a test executable in the form of a dynamic linked library that was then executed on the SWIM platform. Finally, we compared the results of the execution with those obtained with TBOSS targets.

Results

After solving the problems that we exposed, we were able reproduce the results of the TBOSS platform in our prototype for each one of the tests: all of the unit tests executed in the exact same way in both platforms, starting from the exact same sources, and giving us the same results, byte per byte. We created a prototype of a software simulator based testing platform. The prototype uses some of the components of the hardware based platform while some others were completely reimplemented. We also produced a set of new, modifiable, object oriented OSSCI libraries that implement an interface between SWIM and existing control programs. Finally, we obtained a modified instance of the SWIM simulator that is paced by the OSSCI and that executes IMA applications in a MIF basis, without interfering with the results because the realtime behavior is not compromised.

Discussion

Interpretation of the results

The identical results of the validation tests in both platforms and the minimal modification of control programs, suggest that a total, backwards compatible migration to a simulatorbased testing platform is possible in the short term. Although we have not formally evaluated if our prototype is a better testing platform than the one of TBOSS (see section 1.2 "motivation"), we can already tell some differences : The tests finish faster in our platform because we do not need to recompile the basic software for each test, or load the executables from an external host into the target's memory. The minimal modification of the control program, a central part of both of the testing platforms, shows that it is also possible to reuse most of the existing components. The modifications made to the control program of the SWIM platform concerns only the OSSCI. None of the interfaces with the rest of the platform were affected. We therefore believe that other control programs can be modified in the same way and that none of the other components of the existing platform must be modified to achieve full backwards compatibility with an eventual simulatorbased platform. Our new OSSCI libraries are not only an interface between SWIM and control programs but also an interface between existing tests and any other execution platform. The fact that they are object oriented will allow us use them easily with other execution simulators; in fact work is already being done on this subject. We also want to stress the open nature of these libraries. While the implementation of the OSSCI on the TBOSS platform is not accessible, we can freely use and modify these libraries according to our needs. We even use some Free Software internally, although we are not planning to release these tools.

Future work

Our results allow us to think of the implementation of a SWIMbased testing platform that could be widely used by developers during the test phases of their avionics software. The representativeness of such a platform could be questioned, but in any case the platform could be used to detect problems prior to execution in more representative environments. Much of the work done for our prototype can be directly exploited in a productionlevel SWIMbased testing platform. We will continue to explore the use of simulated environments to test avionics software, specifically the use of full hardware virtualization to achieve total representativeness.

Conclusion

This paper was a technical report of our experience developing a prototype of a testing platform for avionics software based on the SWIM IMA structure simulator. We used this prototype to identify problems that could prevent us from creating a backwards compatible, simulatorbased testing platform and to migrate to it. We identified several conditions that should be taken into account in the event of such a migration. Our results suggest that this migration is possible in the short term. MIF: Minor Frame: The minimal time unit in which application partitions can be configured in an IMA application.

Glossary

ARINC 653: Is a standard developed by Aeronautical Radio, Incorporated (ARINC) that defines the interface between an IMA application and the underlying operating system.

Airbus API: an implementation of the ARINC 653 standard that adds some extensions specifically for Airbus aircraft.

Free Software: software that can be used, studied, distributed and modified under certain legal restrictions stated in [START_REF]The Free software definition[END_REF].

•

  prepare_connections: called on reception of a message sent by OSS_Init, it sends the client the APEX port configuration of the current test and prepares all connections.• destroy: called on reception of a message sent by OSS_End, it destroys all connections and frees temporary resources.

•

  send_next: called on reception of a message sent by OSS_Message_Output, it sends the next ready message to the specified port.

•

  receive_next: called on reception of a message sent by OSS_Message_Input, it receives the next message waiting on the specified port.

Figure 3 .

 3 Figure 3. An overview of the SWIM platform

Figure 4 .

 4 Figure 4. Default symbol resolution in GNU/Linux

Figure 5 .

 5 Figure 5. Symbol resolution in the SWIM platform

  IMA: Integrated Modular Avionics. An architecture for sharing computing resources in a realtime airborne network. CPIOM: Core Processing and Input/Output Module -A single calculator in the IMA structure. SWIM: Software Workshop for IMA Modules -a software simulator of the IMA Structure TBOSS: TargetBased Operating System Simulation -a set of proprietary tools based on a hardware target to simulate the execution of IMA software with assured representativeness. OSSCI: Operating System Simulation Control Interface -a part of the TBOSS platform that enables external, bidirectional communication with the outer world.

Acknowledgements

We would like to thank Laurent Gillet, JeanBaptiste Jouve and Philippe Seraud for their technical and moral support during the development of this project.


P Cuenot

P Frey

R Johansson

H Lönn

M.-O Reiser

D Servat

R Tavakoli Kolagari

D J Chen

Developing Automotive Products Using the EAST-ADL2, an AUTOSAR Compliant Architecture Description Language

Keywords: Modeling, Abstraction, ADL, AUTOSAR

Current development trends in automotive software feature increasing standardization of the embedded software structure. But it still remains the critical issue of the overall engineering information management to control the system definition and manage its complexity. System modeling based on an Architecture Description Language (ADL) is a way to keep these assets within one information structure. The original EAST-ADL was developed in the EAST-EEA project (www.east-eea.org) and basic concepts were reused in the AUTOSAR standardization initiative. The original EAST-ADL is currently refined in the ATESST project (www.atesst.org) to EAST-ADL2. This paper presents the results of the language extension provided by the EAST-ADL2 domain model and focuses on its possible extension of the AUTOSAR standard to support decomposition of E/E automotive systems.

Introduction

Current development trends in automotive software feature increasing standardization of the embedded software structure, in particular manifested by the AUTOSAR standardization initiative. The AUTOSAR consortium [START_REF]AUTOSAR Development Partnership[END_REF] defines a generic software architecture platform by standardization of its infrastructure and a communication layer suitable for distributed hardware architectures. The specification of application software components is standardized, such that these can be reused and integrated on the AUTOSAR platform by a third party. Software reuse is thus favored and implementation-specific dependencies between application software and hardware is avoided.

The AUTOSAR approach improves the OEM/supplier development relation and data interchange. Higher quality and dependability is foreseen and cost and complexity can be managed appropriately.

The AUTOSAR standard for E/E architectures is becoming more and more mature; its release 3.0 has been completed in December 2007. Automotive OEMs are planning to use AUTOSAR for series production and all new development of embedded automotive software will in future be compliant to it.

But there are still some numbers of issues outside the scope of this standardization initiative that are necessary for managing the engineering information and its assets attached to system definition.

System modeling based on an architecture description language (ADL) is a way to keep the engineering information in a well-defined information structure. In the context of the ATESST project we have reused and extended the original EAST-ADL language primarily developed in the EAST-EAA project. We consider that Model Based Development (MBD) as supported by the EAST-ADL is complementary to the AUTOSAR approach. Through this combination, it is possible to support system modeling down to the componentization level (AUTOSAR). It is thus a means for efficient development and management of the complexity of automotive embedded systems: Concepts from MBD and CBD reinforce one another [START_REF] Törngren | Componentbased Development vs. Model-based Development: A Comparison in the Context of Vehicular embedded Systems[END_REF]. We will demonstrate how EAST-ADL2 solves the challenge of the full integration of the two, by describing engineering information supported by the EAST-ADL2 language.

The important complements to AUTOSAR represented by the automotive domain specific language EAST-ADL2, are:

• requirements modeling and tracing including capability for specific adaptation, • feature modeling including concepts to support product lines,

• structural and behavioral modeling of functions and hardware entities in the context of distributed systems, and • other information, such as a definition of function timing and failure modes, support of system analysis.

A main result of the ATESST project is the EAST-ADL2 domain model, released as a public UML2 profile. The following sections describe the EAST-ADL2 with reference to the AUTOSAR standard and how this combination allows modeling of E/E automotive systems.

Section 2 presents the structural view of the language constructs including structural relation to AUTOSAR. Section 3 gives details on behavioral modeling including behavioral relation to AUTOSAR. Section 4 describes requirements modeling being orthogonal to the other models. Section 5 addresses applied product line techniques and variability modeling essential for the automotive domain. Section 6 describes timing modeling support of the language. Section 7 provides error modeling overview for analysis of failure propagation. Finally, conclusions are drawn with consideration of the designers' and end-users' perspectives.

Structural view of EAST-ADL2

The following section describes the organization of EAST-ADL2 with respect to structural view to describe how to capture system information and how models are related to each other.

EAST-ADL2 structural overview

EAST-ADL2 is an architecture description language defined as a domain-specific language for the development of automotive electronic systems. It includes modeling entities to describe features, requirements, variability, software and hardware components, and specific annotations associated to models to support the analysis of the system.

The core concept of the structural organization of EAST-ADL2 is the description of the models in different abstractions levels (see Figure 1). The electronic functions/features are described at different levels of abstraction, reflecting the details of the architecture and implicitly different stages in the engineering process. The different artifacts drive the functional decomposition of the functions from abstract models down to implementation in software components and hardware elements of the system architecture.

Modeling of the electronic systems of a vehicle starts with capturing the functions at the Vehicle level with product line organization and description.

These functions are realized at the Analysis level by abstract entities describing models of software functions (such as "ADLFunction") and devices (such as "FunctionalDevice") that interact with the vehicle environment. The Analysis level captures the principal interfaces and the behavior of the subsystems of the vehicle.

On the Design level, models are refined with more implementation-oriented aspects that allow a subsequent software decomposition of the functional architecture. Devices are split into elements of the hardware architecture such as sensors or actuators, and the software parts for signal transformation (such as "LocalDeviceManager"). Middleware is modeled to project the platform specific services and functionality to the functional level The hardware architecture is introduced in parallel to capture the hardware entities as abstract elements (e.g.

Relation EAST-ADL2 -AUTOSAR

As described above, the structural relation between EAST-ADL2 and AUTOSAR is complementary.

EAST-ADL2 provides modeling artifacts for functional modeling supporting a refinement process for decomposition of features to artifacts, such as software and hardware elements, while keeping track of the system architecture description. Software implementation details are not captured as AUTOSAR provides lower level implementation mechanisms to support full description of software components and related information and techniques for deployment in the AUTOSAR standardized platform.

The "ADLFunction" introduces a degree of freedom for the AUTOSAR software implementation architecture, via the dedicated association "ADLBehavioralMapping" to map "ADLFunction" to "Runnable Entities" of AUTOSAR. This mechanism allows packaging multiple "ADLFunction" entities to software components and to optimize various aspects during implementation.

"LocalDeviceManager" is the interface functionality for sensors and actuators and is realized by the "SensorActuatorSoftwareComponent" of AUTOSAR.

The port concept of EAST-ADL2 is inherited from SySML for data descriptions (such as "ADLFlowPort") and service interaction (such as "ADLClientServerPort"). The entities match the AUTOSAR "SenderReceiver" and "ClientServer" ports. However, AUTOSAR port configuration and RTE services include mechanisms abstracted on the level of EAST-ADL2.

The hardware architecture of EAST-ADL2 is complementary to the AUTOSAR system topology and ECU resource definition and configuration. AUTOSAR focuses on the impact of software implementation based on the required configuration of the various software elements (bus topology including communication signal allocation, "Runnable Entities" allocation to task from operating system, driver configuration in relation to ECU pins ...). EAST-ADL2 entities abstract the overall hardware topology to capture physical elements of the vehicle electronic architecture and wiring harness. Some elements are present on both sides but with abstract representations: "ECU", "IOPort" and "Communication" bus as elementary entities are not decomposed at this level. A more complex relation is abstracted with hardware ports of EAST-ADL2 (as "ADLHWPort"). This entity is realized by platform "HAL" service to map software IO driver and hardware pin configuration at AUTOSAR Level.

Finally, interfaces of complex device drivers and AUTOSAR platform services independent of hardware allocation are captured by "ADLFunction" entities in middleware.

Behavior models

The goal of EAST-ADL2 with respect to behavior is to describe how model components (from different tools, in different modeling languages, or just representing code) are related to each other in order to capture behavior and algorithms of the vehicle systems as well as the environment. A report publicly available summarizes the work conducted during the ATESST project (see [START_REF]Report on behavioral modeling within EAST-ADL2, D3.2 deliverable[END_REF]). Two main issues are accounted for here: 1) behavioral semantics of the "ADLFunction" entities and 2) mapping to AUTOSAR behavioral constructs.

EAST-ADL2 behavioral semantics

In EAST-ADL2, behavior modeling relies on the definition of a set of elementary functions that are executed based on the assumption of synchronous run-to-completion execution (read inputs from ports, compute, and write outputs on ports). This was chosen to enable analysis and behavioral composition and to make the function execution independent of behavioral notations: inside each function, the data transformation could be described according to various languages and paradigms, and various legacy tools including general UML tools and domain-specific tools (e.g. Simulink, ASCET).

The triggering of each function is defined by time or an event on one of the input ports. A precedence constraint construct allows definition of any constraint that needs to be honored when the scheduling and task allocation is made.

Figure 2: "ADLFunction" entities and triggering aspects

There are two types of "ADLFunction" entities, time discrete and time continuous (see Figure 2). Each time the function is invoked, the read-execute-write pattern is performed, i.e. all inputs are read at the same time and outputs are written at the same time.

For discrete functions, this is done after a computation delay, "ExecutionTime". Time continuous functions ("ADLContFunction") define the transfer functions from input to output, and the computation rate is infinite. In practice, invocations are implicitly defined by the solver tool used to simulate or analyze a set of connected functions. In order to allow different behavioral definitions, all inputs are read simultaneously, and all outputs are written simultaneously.

Time

discrete "ADLFunction" entities, "ADLDiscFunction", have an explicitly defined invocation pattern. Functions may be time-triggered, in which case time alone causes execution to start. Event triggered functions may be invoked due to data arrival or calls on the input ports. This is defined by the "TrigPolicy" attribute. "TriggerPeriod" defines the time between invocations for time trigged functions or the inter-arrival time between invocations for event-triggered functions. Offset is the offset of invocations relative to a nominal period for time trigged functions. It is not applicable to event triggered functions A textual/OCL "TriggerCondition" rule may be used to define the conditions for when the function is invoked. For example, a port value has to exceed X or data must arrive on more than one port. In order for offsets and periods to be meaningful, the assumption regarding synchrony has to be declared. This is done with the "TimeBase", which lists all "ADLFunction" entities that share the same time base (not shown on figure). This may be realized by co-allocation to the same ECU, or coallocation to a set of ECUs with a shared clock (e.g. based on FlexRay).

Functions own an "ADLBehavior" that is refined in "ExternalBehavior", when definition is made in external tools (e.g. Simulink, ASCET, etc.) and "NativeBehavior", when definition is made according to the behavioral semantics of EAST-ADL2.

These concepts are implemented as stereotypes applicable to UML classes and UML behavioral constructs such that information can be shown both in composite structure diagrams and behavioral diagrams, such as activity diagrams. "ExternalBehaviors" are mapped to the UML "OpaqueBehavior", which features both a language and body attributes (holding references to the type of external tool and language used, e.g. Simulink, ASCET, etc.). "NativeBehaviors" are mapped directly to UML "Behaviors" such that "StateMachines", "Activities", or "Interactions" -depicted as sequence diagrams -can be used w.r.t to modeling needs. The application of EAST-ADL2 stereotypes on these UML concepts alters UML2 semantics such that among other things, triggering policies and run-tocompletion assumption hold (see [START_REF]Report on behavioral modeling within EAST-ADL2, D3.2 deliverable[END_REF]).

Relation EAST-ADL2 -AUTOSAR

As said previously, AUTOSAR concepts are organized as the implementation level of EAST-ADL2. Elementary "ADLFunction" entities are to be mapped to AUTOSAR behavioral units, which are the "RunnableEntities" contained in "AtomicSoftwareComponents" (SWC). Different mappings can be made, depending on the implementation configuration. It is also possible to leave out the traceability to "RunnableEntities", if this level of detail is unnecessary, or if component internals are yet unknown or confidential.

The ports of EAST-ADL2 models are transformed into ports on the AUTOSAR SWC. One or several EAST-ADL2 ports may be realized by one AUTOSAR port, as these may have several "signals" or data elements per interface.

Figure 3 below shows an example on how elementary "ADLFunction" entities are mapped to three AUTOSAR SWCs. Each elementary "ADLFunction" has its own logical execution thread and no internal concurrency. It therefore maps well to a "Runnable". Note that the ports follow the elementary "ADLFunction" entities to the AR SWCs, and that this is one out of several possible mappings. The execution of "RunnableEntities" managed by AUTOSAR RTE configuration can thus be specified by the semantic properties of the "ADLFunction". AUTOSAR runnable may exhibit more complex behavior as well, but this is excluded from the EAST-ADL2 behavioral semantics in order to preserve analyzability.

Requirements models

Requirements are captured in EAST-ADL2 according to the principles of SysML [START_REF]SysML Partners. Systems Modeling Language (SysML) open source specification project[END_REF]: Requirements are separate entities that are associated to its target elements with a specific association, "ADLSatisfy".

Requirements are related to each other to support traceability between requirements. Typically, requirements on the higher abstraction levels of EAST-ADL2 are refined to more detailed requirements on lower abstraction levels.

Verification and Validation is supported through the concept of Verification& Validation Cases. A "VVCase" is linked to requirements and target entities, in order to show how a certain requirement is verified in the context of a specific model entity. EAST-ADL2 distinguishes between the model entity that is verified to meet the requirement, from the target system.

An important aspect of traceability is the possibility to follow which requirements are the results of safety concerns. This is needed to comply with the upcoming automotive standard for safety, ISO 26262 [START_REF]International Organization for Standardization: ISO Working Draft 26262 Baseline 10[END_REF]. EAST-ADL2 also supports this standard by providing support for safety case, safety integrity levels and error propagation (see further section 7).

The Requirements Interchange Format (RIF) [START_REF]HIS, Specification Requirements Interchange Format (RIF)[END_REF] has been considered in the ATESST project to represent Requirements from external tools. RIF is a general standard that supports the interchange of requirements, but also other engineering information. Due to this generality, an ADL such as EAST-ADL2 cannot support the full RIF without loosing stringency, and a subset is chosen instead.

Variability models

In order to give an overview of variability management in EAST-ADL2, we examine two questions:

• In what development situations and contexts is variability management needed? Or: For what parts of EAST-ADL2 is variability management support provided?

• What is the basic modeling means used for variability modeling and to which of these development situations/contexts are they applicable?

Needs

First, variability management starts on the Vehicle Feature Level, where model range features and variability is viewed. At this point, the purpose of variability management is to provide a highly abstract overview of the variability in the system such as the complete system together with dependencies between these variabilities. A "variability" in this sense is a certain aspect of the complete system that changes from one variant of the complete system to another. "Abstract" here means that for an individual variability it is not the idea to define how the system varies with respect to this variability but only that the system shows such variability. For example, the front wiper may or may not have a rain sensor. On vehicle level the impact of this variability on the design is not defined; only the fact that such variability exists is defined by introducing an optional feature named 'RainSensor'. This is later validated and refined during analysis and design.

While the details of how variability is actually realized in the system are largely suppressed on the vehicle level, they are just the focus of attention when managing variability on other areas of the development process. In fact, certain variability may lead to modifications in any development artifact, such as requirements specifications, and functional models. With respect to EAST-ADL2, three areas are to be distinguished: (1) requirements, (2) the artifacts AnalysisArchitecture, DesignArchtiecture and ImplementationArchitecture and (3) test artifacts. Here, describing that certain variability occurs is not sufficient; it is necessary to describe how each variability concept affects and modifies the corresponding artifact.

Basic modeling means

Having answered question no. 1 above, we can now turn our attention to the second question: the basic modeling means provided as support for variability management in these different situations. They are: feature modeling, product decision modeling and multi-level feature trees.

The purpose of feature modeling is to define the commonalities and variabilities of the product variants within the scope of a product line. Usually feature models are used on a high level of abstraction, as described above for vehicle level variability. However, in EAST-ADL2, they are also used on design level and get a much more concrete meaning there. Product decision modeling on the other hand is aimed at defining configuration: The configuration of a feature model fa -i.e. the selection and deselection of its features -is defined in terms of the configuration of another feature model fb. A product decision model can thus be seen as a link from fb to fa that allows deriving a configuration of fa from a given configuration of fb. Finally, multi-level feature trees (see Figure 4) are a means to strategically manage two or more separate, independent product lines. With this instrument at hand, not all variants of the complete system need to be managed within a single, extremely complex global product line. It is instead possible to subdivide the product line into smaller, subordinate product lines (called product sublines) without loosing the possibility to manage them from a global perspective.

Variability management on the artifact level is driven by the variability captured on the VFM. This means that the main driver for variability and also variability instantiation is the Vehicle Feature Model. Variability on the artifact level essentially consists of the use of variation points and simple feature models (i.e. nonmulti-level feature models) at the public interface of functions.

The basic idea of the artifact level variability modeling is that whenever variability on the respective abstraction level occurs, a variation point is introduced (see Figure 5). The variation point is introduced and is linked via its variation point configuration to the possible variants, which may replace the variation point. The variation point can be replaced by either of the specified variants. If the variation point has the cardinality [0..1] the variation point as a whole can be deselected, meaning that the variation point is optional. The variation point in Figure 5 is not optional (marked by the cardinality [START_REF]AUTOSAR Development Partnership[END_REF]) and can only be replaced by one of its two variants. The variation point has one input port and two output ports. Variant 1 only needs one output port, whereas variant 2 needs two output ports. So the variation point has the superset of ports of all possibly replacing variants. But those ports that are not used in all circumstances are marked by the cardinality [0..1], meaning that they are optional. Also, the port expecting input from an optional output port is marked by the cardinality [0..1] (i.e. implicit optional) in order to reflect that this port cannot in all instantiations expect input from this port, which must be coped with in the behavior of the respective function.

Figure 5. An "ADLFunction" as a variation point with two variants.

To summarize the discussion on ports we can say:

• An optional port is a port in a variation point that is not used by all variants. • An implicit optional port is the port of a function that will always appear in the implementation, but it will not always be used:

• an implicit optional output port means: à data will always be sent; but there are cases when there is no other function that consumes this data.

• an implicit optional input port means: à data is always expected; but there are cases when there is no other function that actually sends such data.

By introducing implicit optional ports it is possible to reduce explicit variability modeling, because the function with an implicit optional port does not need to be variable as a whole.

As depicted in Figure 6, the starting point of variability modeling is on the VFM level. The core feature model of the VFM influences the instantiation of artifact variability. Each single artifact entity (especially "ADLFunction") has at its public interface a parameterized feature model that is a function feature model (see Figure 6), without being a multilevel feature model. These public interfaces describe internal variability of the functions. This is needed to have an adequate overview of the respective variability of the functions. Besides using feature models at the public interface of single modeling entities, feature models are used to describe the variability of a complete product subline at an artifact (e.g. FDA).

In order to make the development of individual subsystems independent from the whole system, artifact lines are introduced. This is of specific interest for suppliers because they use their own product line approach for the subsystems they develop. So the artifact line as a whole has an own feature model, whose instantiation is driven once again by the core feature model of the VFM level using product decisions.

In order to extend language elements of other languages or standards connected to EAST-ADL2 (like AUTOSAR, SysML) with the variability approach of EAST-ADL2, the respective element is enhanced by a generalized link to the "ADLVariableElement" (see Figure 7). Hence, the variability technique of EAST-ADL2 can also be used for these elements.

EAST-ADL2 Timing Modeling Support

Why automotive timing is important

Many automotive functions are control applications which often impose hard real-time requirements on their form of realization in the E/E system. Such control applications can mainly be found in the power-train domain (e.g. engine management, transmission control) and chassis domain (electronic stability program, antilock braking system), but also in the body domain where even non-control applications have timing requirements (indicator, window lifter). For control applications, it is important that the sensing of input data, actual control algorithm computations and output data actuation are in synchrony with the speed of the controlled plant and with its proceeding dynamics. In distributed embedded systems, the task of implementing potentially distributed control applications becomes truly challenging, especially when multiple sensors and multiple actuators are involved where determinism and consistency in both the time and value domain for the involved sensors and actuators are required.

Timing as integrated engineering information and relation to AUTOSAR

The EAST-ADL2 provides support to capture specific engineering information which is relevant for the timing of automotive functions. Conceptually, timing information can be distinguished into timing requirements (what is demanded), timing properties.

(what is offered), and timing contracts (what is negotiated between stakeholders). This is in-line with how OMG in the UML Profile for Modeling and Analysis of Real-time and Embedded Systems (MARTE) [START_REF] Omg | UML Profile for Modeling and Analysis of Real-time and Embedded Systems (MARTE), Beta1[END_REF], represents non-functional properties as of either required, offered or contract nature. The general notion is that the actual timing properties of a solution (=implementation, realization) must satisfy the specified timing requirements stemming from the automotive function specification.

Figure 8 presents an overview sketch how the considered timing information is perceived in general in the EAST-ADL2 system model. Note that the start of the arrows describes the origin of timing related engineering information, and the direction of the arrow (top-down or bottom-up) describes their interabstraction level relation. The concept of contract based timing is a way of decomposing the complex problem of end-to-end timing, which may depend on detailed implementation details from a number of different companies not willing to share too much data among each other. The timing contracts thus also enables complete verification on a higher level of abstraction, without having all implementation details on lower level of abstraction present. As EAST-ADL2 is still being developed, the language currently covers aspects of the timing requirements part on the two functional abstraction levels only (Analysis Level and Design Level in Figure 8).

Ensuring operational correctness

To ensure operational correctness with respect to timing, validation and verification activities (V&V) can be performed on every abstraction level. However, different techniques provided through different tools or a combination of those might have to be applied.

Note that these V&V techniques may require specific input in the form of execution time bounds which can be derived in different quality and by different techniques themselves (e.g. measurements, mathematical code analysis). The so derived timing properties of the system or function are checked against timing requirements which have been derived either directly from a contract or through refinement from the original function specification on higher levels of abstraction (Analysis and Design levels).

In the EAST-ADL2, timing requirements are distinguished into various kinds of delays (= latencies) as well as specific timing requirements for the temporal synchronization of input data or output data respectively. Delays can either be end-to-end delays from sensors to actuators or atomic delays or composed delays for the single time consuming modeling entities which are part of a timing chain. The latter type of delays are referred to as timingchain-segments of an end-to-end timing chain (=end-to-end delay). End-to-end delays are subject to segmentation along the functional decomposition track, i.e. when progressing from a functional model on Analysis Level to a refined functional model on Design Level to an implementation model in terms of AUTOSAR software component architecture on Implementation Level. Note that the level of end-toend timing delays is not automatically following the level of abstraction. For example can the number of elementary "ADLFunction" timing segments present on the Design level, be much higher than the number of (composed) software component timing segments on the (AUTOSAR) implementation level, when representing the same end-to-end timing.

User challenges

Clearly, the EAST-ADL2 users' challenge will be to perform a functional decomposition and refinement of top-level functions from Analysis Level to Design Level while considering the segmentation of the endto-end delays into single timing chain segments at the same time. By introducing well defined segments EAST-ADL supports the concept of timing contracts, thus fitting to the automotive world where the responsibility for fulfilling end-to-end timing requirements will continue to be split between a Car OEM and a number of TIER1s. The proposed EAST-ADL2 will have to prove its soundness and applicability in future evaluations. However, only recently the demand for additional levels of abstractions and separation of concerns has been raised and should not be overheard [START_REF] Sangiovanni-Vincentelli | Embedded System Design for Automotive Applications[END_REF].

The general concept of traceability of engineering information between multiple levels of abstraction, which is also applicable to timing information, enables sound and comprehensible design decisions which are documented in the overall system model.

EAST-ADL2 Error Modeling Support

Why error modeling is necessary

Automotive embedded systems are inherently safety critical due to the devices and dynamics under control. In other words, an error of such systems, if not detected and properly handled, could endanger human life and result in damages to environment and property. Currently, embedded software is increasingly introduced and integrated in modern automotive systems, accounting to a large portion of innovations and also to growing product complexity. Meanwhile, the competitive forces are also driving for short time-to-market, cost efficiency, configuration flexibility and accommodation of new technologies, etc. For these reasons, the design of safety in embedded automotive systems is posing an increasing challenge for the developers. While stateof-the-art safety analysis techniques providing analysis support for deriving the causes and consequences of errors, the difficulties remain in capturing and maintaining plausible errors, safety requirements, and other related information while performing design refinement, changes and evolution, and in providing arguments that a system is safe enough.

The overall objective of the EAST-ADL2 error modeling is to allow an explicit reasoning of functional safety and thereby to facilitate safety engineering along with an architecture design or maintenance process. As an overall system property, safety is concerned with the abnormalities (in terms faults, errors, and failures) and their consequences under given certain environmental conditions. Functional safety represents the part of safety that depends on the correctness of a system operating in its context [START_REF]International Electrotechnical Commission Functional safety of electrical/electronic/ programmable electronic safety-related systems -Part 0: Functional safety and IEC 61508[END_REF]. In other words, it addresses the hazardous abnormalities of a system in its operation (e.g., component errors and their propagations).

Error modeling as an analytical view extension to nominal architecture

EAST-ADL2 facilitates safety engineering in regards to the system modeling and information management. While supporting the safety design through its intrinsic architecture modeling and traceability support, the language allows the developers to explicitly capture the error logics in terms of component errors and the error propagations in an architecture error model through its error modeling support (see also Figure 9). The error modeling is treated as a separated analytical view orthogonal to the nominal architecture model. This separation of concern in modeling is considered necessary in order to avoid some undesired effects of error modeling, such as the risk of mixing nominal and erroneous behavior in regards to the comprehension, reuse, and system synthesis (e.g., code generation).

The EAST-ADL2 error modeling package extends a nominal architecture model, typically at the functional and design levels, with the information of failure semantics and error propagations. The failure semantics can be provided in terms of logical or temporal expressions, depending on the analysis techniques and tools of interest. Such analytical information, together with environmental conditions, forms the basis for identifying the likely hazards, reasoning about the causes and consequences, and thereby deriving safety requirements. The relationships of local error behaviors are captured by means of explicit error propagation ports and connections. Due to these artifacts, EAST-ADL2 allows advanced properties of error propagations, such as the logical and temporal relationships of source and target errors, the conditions of propagations, and the synchronizations of propagation paths. Hazards or hazardous events are characterized by attributes for severity, exposure and controllability. A hazardous event may be further detailed by e.g. use cases, sequence or activity diagrams. In an architecture specification, an error is allowed to propagate via design specific architectural relationships when such relationships also imply behavioral or operational dependencies (e.g., between software and hardware). In EAST-ADL2, a safety requirement derived from the safety analysis has attributes specifying the hazard to be mitigated, the safety integrity level (ASIL/SIL), operation state, fault time span, emergency operation times, safety state, etc [START_REF]International Organization for Standardization: ISO Working Draft 26262 Baseline 10[END_REF], [START_REF]International Electrotechnical Commission Functional safety of electrical/electronic/ programmable electronic safety-related systems -Part 0: Functional safety and IEC 61508[END_REF]. The safety requirement is then traced to or used to derive other nominal requirements such as in regards to safety functions and performance.

Analysis leverage through external tools and other engineering support

Given an error model, the analysis of the causes and consequences of failure behaviors can be automated through external tools. There is currently a (prototype) analysis plug-in in the Eclipse environment, allowing the integration of the HiP-HOPS tool (Hierarchically Performed Hazard Origin and Propagation Studies) [START_REF] Papadopoulos | Hierarchically Performed Hazard Origin and Propagation Studies[END_REF] for static safety analysis in terms of FFA, FTA, and FMEA. The analysis leverage includes fault trees from functional failures to software and hardware failures, minimal cut-sets, FMEA tables for component errors and their effects on the behaviors and reliability of entire system.

Further supports of EAST-ADL2 for safety engineering include the integration of safety case, referring to a technique that provides a structure for the qualitative argumentation about why a system is safe [11]. The integration, which is currently under development, aims to enable the development of safety case based on the architecture and error information captured in EAST-ADL2. This complements other standardization efforts such as in the ISO WD 26262 [START_REF]International Organization for Standardization: ISO Working Draft 26262 Baseline 10[END_REF] and in the MISRA safety guidelines [START_REF]Development Guidelines for Vehicle Based Software[END_REF], which emphasize the importance of safety case but provide no coverage on the content and implementation.

Conclusion

The ATESST project defining the EAST-ADL2 language has been running for the last two years (since beginning of 2006). During this period there have also been running two initiatives having a major impact on the development of automotive E/E systems: AUTOSAR [START_REF]AUTOSAR Development Partnership[END_REF] and the ISO working group on functional safety for road vehicles (ISO TC 22/SC 3/WG 16) [START_REF]International Organization for Standardization: ISO Working Draft 26262 Baseline 10[END_REF]. Both these are aiming at standardization and at enabling the development of safety-critical automotive E/E systems while the complexity of these systems are growing rapidly. The focus of safety in AUTOSAR has especially grown in its second phase starting 2007.

The implications of these two initiatives on the definition of EAST-ADL2 have been obvious. The applicability of an automotive ADL will be heavily dependent on its conformance to AUTOSAR and to the upcoming safety standard ISO/WD 26262. Thus, the evolvement of EAST-ADL2 has had a focus of being complementary to AUTOSAR, supporting modeling the more abstract levels, thus extending AUTOSAR in a consistent way.

In ISO/WD26262 there are requirements on the existence of a so called safety case. A safety case is a tool that provides structure to the qualitative argumentation about why a system is safe. This is done by separating the argumentation from the facts or justifications and providing an explanation of the relationships and dependencies between them.

EAST-ADL2 includes a meta-model for a safety case, thus enabling safety case development in close connection to the system model. Furthermore, modeling systems in EAST-ADL2 makes it possible to provide explicit descriptions of faults in functions, software and hardware, and the mechanisms by which they can propagate. Such descriptions in turn facilitate safety analysis techniques like FTA and FMEA, generating evidences for the safety cases.

In addition, the traceability, consistency and rigor required when developing safety-related systems are well supported by an ADL.

To conclude, EAST-ADL2 both supports the generation of a safety case as prescribed in ISO WD 26262, as the generation of its supporting evidence.

Having had the opportunity to define this architecture description language in parallel with the dynamic phases of the definitions of AUTOSAR and ISO WD 26262, EAST-ADL2 has a good potential to become a de facto standard as it fits well with the major critical needs of the automotive industry of today. To enable a wide spread use of EAST-ADL2, the domain model is now released as a public UML2 profile.

Acknowledgement

This work was supported by contribution of all the partners of the ATESST project consortium funded by the European Commission. We wish to acknowledge useful participation of all partners and feedback from the anonymous reviewers.

Figure 1 :

 1 Figure 1: EAST-ADL2 abstraction layers and relation to AUTOSAR.

Figure 1

 1 Figure 1 depicts the substitution of the implementation level of EAST-ADL2 by AUTOSAR, and how abstract EAST-ADL2 concepts match AUTOSAR: FunctionalDesignArchitecture defines application functionality of the AUTOSAR application software architecture, the Middleware Abstraction

FunctionModeling

Figure 4 .

 4 Figure 4. Reference model and referring models in the multi-level feature modeling approach.

Figure 6 .

 6 Figure 6. Function feature model at the public interface of a function.

Figure 7 .

 7 Figure 7. Extend AUTOSAR "RunnableEntity" to a variable element.

Figure 8 .

 8 Figure 8. Timing information as perceived in the EAST-ADL2 system model

Figure 9 .

 9 Figure 9. EAST-ADL2 Architecture Error Model as a separate architecture view extending the nominal architecture model and providing analysis leverage through external tools.