Dr Udo Brockmeyer

Guido Sandmann

Michael Beine

Formal Verification Techniques in a Model-Based Development Process based on TargetLink generated C-Code

The numbers of electronic devices in modern automobiles increased enormously within the last few years. Not only the raising number of the Embedded Control Units (ECUs) within one automobile is a challenge, but there is also a very strong increase in functionality in every single ECU. These facts lead to an exponential boost of complexity regarding intra-and inter-ECU behavior. Development of these systems is only manageable if accurate and sophisticated processes are implemented allowing development engineers to deal with this enormous complexity. Those processes provide a means to deliver the devices under hard time and cost constraints. The Model-Based Development process is an approach that allows engineers to graphically specify the behavior of a system and to simulate and execute it in a very early development stage. The tool environment MATLAB®/Simulink®/ Stateflow® offered by TheMathworks is a wide spread modelbased development tool for designing control applications for different industrial domains such as automotive, aerospace or rail systems. Once a model-based development process has been established, engineers are able to apply new technologies and tools to enhance and shorten product development cycles, e.g. by introducing Automatic Model Validation based upon formal verification technology and Automatic Production Code Generation.

Model-based Development Process

A very promising and quickly spreading approach for the development of embedded systems software is the so-called conceptual model-based design process as supported by the Matlab/Simulink/Stateflow Tools. Its nature is outlined in Figure 1. Requirements given, for instance in a requirements document, are translated first in a formal specification (Simulink/Stateflow Model) representing the system under design. Such specifications are still expressed in a very abstract fashion just capturing relevant functional and safety-critical requirements, but still hiding implementation details like physical characteristics of the concrete hardware or software instance, for example, of a prototype. By formally modeling and specifying a design, formal verification technologies can be used to completely validate whether this formal design specification meets its intended requirements. Hence, verification products such as EmbeddedValidator offer specialized formal-isms for expressing requirements like "the system produces certain output values three steps after having seen some input valuations" in a way a model checker understands them. Performing a formal verification task thus means validating a formalized requirement against a design's formal specification. When all listed requirements are met by a design's formal specification -the Simulink/Stateflow model -then this version of the model will be sometimes referred to as Reference-Model. Within a model-based design process, subsequent development steps then are based upon this Reference-Model. Such a formally verified Reference-Model shows some interesting characteristics.

• Only very few modeling flaws survive the formal verification activities • Formal verification requires consistent and unique requirements. Hence, requirement specifications will be of higher quality after this phase • The specification model will be much more complete and very mature The impact of putting emphasis on early development stages is well-understood in the meantime by airborne/automotive/train systems industries. Spending more time in early stages of a development processes increases quality of the overall product, makes subsequent design stages much more efficient, and in particular reduces overall costs in order to fix late-found bugs or to EmbeddedValidator uses the TargetLink production code generator from dSPACE for obtaining C-code which then is translated for use within the verification engine. Currently, this application of TargetLink is not completely hidden to the user. However, if a user already applies TargetLink in his process, this EmbeddedValidator approach is indeed beneficial, as formal verification can then be viewed also as production code verification, which is closer to the concrete instance of the ECU. To complete the discussion of Figure 1 above, a verified Reference-Model is a great artifact for the application of model-based Automatic Test case Generation (ATG). Test vectors computed from such a Reference-Model can be used to per-form automated functional as well as white-box testing of the software that implements the specification model. A more detailed discussion of this promising technology is beyond the scope of this paper. Just to mention here that formal verification and ATG nicely fit into processes in order to improve verification and validation activities. In contrast to conventional testing approaches, the model checking technology is fully automatic and complete even in mathematical sense, meaning that it can detect every logical design flaw and error within a model under consideration. Model checking analyzes a system regarding arbitrary input scenarios and can thus be viewed as a "complete test" that is performed against a formally specified requirement. Such requirements can be simple boolean expressions such as "an error state is never reached" or more sophisticated ones expressing temporal and causal properties like "an output is set only after certain input values have been observed before". The result of a model checking run is either "true", meaning that the model meets its specification, or it returns "false", meaning that the implementation violates the requirement under validation. In the latter case, the model checker also returns a witness trace representing this violation. EmbeddedValidator offers different visualization views for such traces. First to mention waveform displays, but also Matlab m-scripts allowing users to simulate a problematic situation in Matlab's simulation environment. If witness traces are found by a model checker then they have minimal length. This means that it uncovers errors with a minimal number of simulation steps and randomly picks an arbitrary

Automatic Model Validation

Automatic

Figure 2: Workflow of Automatic Model Validation by using EmbeddedValidator representative. A model checker explores the system in a forward manner, terminating whenever the first error is encountered. This is why shortest paths are returned.

Appling model checking will be mandatory in near future development processes coping with complex functional and safety critical systems, where high safety-integrity levels like SIL-3 and higher must be fulfilled due to certification reasons. Domain specific safety standards as DO-178B for Airborne Systems require al-ready today application of these technologies in order to produce products with very high reliability. But even in areas where lower safety levels apply, model-checking offers great benefits in order to achieve higher quality systems in shorter time and also containing less errors.

Use Cases for Automatic Model Validation

Currently, the debugging and analysis task of a model under development is a hard and timeconsuming process. The designer has to execute the model by using a simulator in order to provide the right input sequence to reach a critical design state. If a design is a complicated piece of software it is a hard job for a human being to set the right input sequences in order to reach the desired sys-tem state to debug the reactive system. Also, control dominated systems usually have deep dependencies which could not be fully captured by designers. The consequence of the enormous increase of complexity together with the increasing time-tomarket pressure is an inherent growing error rate. Due to the huge amount of functionality that is integrated in embedded control units today's designers and testers can not ensure the correctness under all environmental circumstances by just applying conventional testing methods. EmbeddedValidator supports different use cases concerning development of embedded control units with state-of-the-art validation techniques based on formal methods.

Robustness Checks & Standard Analyses

Robustness Checks and Standard Analyses subsume a list of predefined analyses that supports the user with the development of robust models. The Range-Violation-Check enables a user to dynamically check for range violations, i.e. if there exists a run in which an overflow respectively underflow for a certain variable occurs. This analysis is based on range constraints for variables as specified by a user. The Drive-to-capabilities allow a user to automatically compute an input vector that enters a given system state at its end, if this state is indeed dynamically reachable. EmbeddedValidator offers different possibilities to the user for specifying a desired system state. A general input scheme called Drive-to-Property allows users to specify any possible system state, which can be ex-pressed by a boolean formula ranging over variables, including interface objects, and Stateflow states of a model. After having defined a system state, it is a pure push button task to execute the analysis. Drive-to-Configuration check is another analysis possibility. Here, users do not define a boolean formula over arbitrary design objects but only Stateflow state variables. This capability allows checking whether a basic state configuration in a parallel and hierarchical model is dynamically reachable. As result of an EmbeddedValidator run, an executable Matlab m-script will be automatically generated driving a Simulink/Stateflow design in a desired state by using the Simulink/Stateflow-Debugger. Besides m-scripts, which use Simulink/ Stateflow simulation facilities a waveform visualization of detected traces is offered.

Model Certification

Formal verification of functional and safety requirements is the key motivation for introducing model checking based verification technology into a model-based development process. The qualitative argument for model checking against testing comes into play: only this mature technique will find all possible attacks against a Simulink/Stateflow design regarding specified requirements. By checking all possible input valuations a model checker tries to uncover design flaws even for border cases conventional tests might not have revealed. Most common functional and safety-critical properties can be formulated easily by using the provided pattern template library. Requirements a model checker should certify need to be formally specified. Particularly, such requirements must capture temporal aspects such as "three steps after feeding certain inputs to the system, some reactions on the output interface take place". There are several different ways to specify temporal requirements which have been proposed in the past. For ease of use in EmbeddedValidator, OSC offers a library of predefined patterns for requirement specifications. A pattern is intended to be selfexplaining by its name and the user is not confronted with internal implementation details of these patterns. Further, patterns are designed for broadening recognition of temporal requirements, shall prevent ambiguities in their interpretation, and are highly optimized for usage within a model checker.

The library itself captures a broad range of common and often used temporal requirements that can be instantiated by the user for applying them to their designs. Instantiations can simply be done by setting certain pattern-parameters and property bindings.

Automatic Code Generation

Next the existing model has to be transferred into C code and implemented on the ECU. Using automatic code generation for this step is natural and has be-come common practice once the software design is available as a model. In contrast to earlier versions of code generators today's methods of code generation are mature enough to bridge the gap between model based function de-sign and production quality ECU code.

Code generators like TargetLink are capable of generating highly efficient and reliable C Code from well developed models. Using automatic code generation can significantly reduce development times and at the same time increase software quality and eliminate common human programming errors. TargetLink, the production code generator from dSPACE, is seamlessly integrated into MATLAB and allows reliable conversion into C code of existing software de-signs that are available as Simulink/ Stateflow models.

Code-Characteristics

The code generated by TargetLink can well match human programmer's efficiency in terms of memory consumption and execution speed since TargetLink has been specifically designed and developed for production coding. Numerous benchmarks and user experience reports show that in most cases TargetLink is within a narrow range of what the human programmers produce. Still TargetLink code can be subjected to code inspections and reviews. Target-Link code is well readable and well commented, enabling the user to go back from the code to the model. Unnecessary macros, function calls, cryptic naming etc. are avoided. Comprehensive configuration options give the user full control over variable, function and file naming, as well as the flexibility of partitioning the code into functions and files to keep the structure logical and manageable.

Test and Verification

A major advantage of using model-based design methods and tools is the capability of early verification by means of simulation. TargetLink supports different simulation modes which allow the correctness of the implementation, i.e. the code generated by TargetLink, to be tested directly. This is done by comparing simulation results with results from reference simulations, frequently referred to as model-in-the-loop simulations. This verification can be performed stepwise:

• First, the generated code is compiled with a host compiler and executed on the host PC; this is also known as software-in-the-loop simulation. • Then simulation is performed on an evaluation board equipped with the target processor. Therefore the generated code is compiled with the actual target compiler; this simulation mode is called processor-in-the-loop simulation. In all simulation modes TargetLink allows signal traces of block outputs to be logged. These signal traces can be saved and plotted on top of each other, thus providing direct visual feedback and allowing further analysis. SIL and PIL simulation are complemented by code coverage analysis. The cover-age types currently supported are statement and decision coverage. All this means that extensive support is given to the unit or module testing phase, including model parts that are generated incrementally.

Conclusion

It is inevitable that embedded software industries in airborne, train, and automotive domains will eventually mature, and catch up with other industries such as the computer hardware industry. Soon, it will be state-of-the-art that model-based development processes are established and exercised. If we also consider that the current strong trend to automation of safety-critical functions requires stringent application of safety standardswhich in turn demand the application of formal methods in general and formal verification in particular -then it will become common practice for embedded software engineers and test engineers to develop and verify their software using model checking. Benefits of this technology are obvious: design flaws are detected early in the overall process. The quality of specification models increases. These improvements boil down to significant cost reductions in the development process. Formal verification is complemented by Automatic Code Generation. TargetLink as a state of the art production code generator allows producing efficient, reliable, and highly optimized code from the formal verified models by avoiding manual coding errors. The usage of both technologies is a big step towards error and cost reduction within the development process of embedded systems.

Figure 1 :

 1 Figure 1: Automatic Model Validation and Automatic Code Generation in a Model based

Figure 3 :

 3 Figure 3: Model-, Software-und Processor-in-the-Loop-Simulation


C Ferdinand

R Heckmann

Verifying Timing Properties of Safety-Critical Embedded Software by Abstract Interpretation

Keywords: Safety, Timing Validation, Schedulability Analysis, WCET (worst-case execution time) Prediction

  L'archive ouverte pluridisciplinaire

Introduction

Failure of a safety-critical application on an embedded processor can lead to severe damage or even loss of life. Also for non-safety-critical applications, software failure may necessitate expensive updates. Therefore, utmost carefulness and stateof-the-art machinery have to be applied to make sure that an application is working properly. To do so lies in the responsibility of the system designer(s).

Many tasks in safety-critical embedded systems have hard real-time characteristics. Real-time systems are typically composed of a set of tasks with specified deadlines (mostly dictated by the surrounding physical environment). Failure to meet deadlines may be as harmful as producing wrong output or failure to work at all. Therefore, a schedulability analysis (also called timing validation) has to be performed in order to guarantee that all timing constraints will be met [START_REF] Stankovic | Real-Time and Embedded Systems[END_REF]. It requires the worst-case execution time (WCET) of each task in the system to be known prior to its execution. Since this is not computable in general, estimates of the WCET have to be calculated. These estimates have to be safe, i.e., they must never underestimate the real execution time. Furthermore, they should be tight, i.e., the overestimation should be as small as possible.

Yet determining such good WCET estimates is a difficult problem because of the characteristics of modern software and hardware. Caches, branch target buffers, and pipelines are used in virtually all performance-oriented processors. Consequently the timing of the instructions depends on the execution history.

Hence, the widely used classical methods of predicting execution times are not generally applicable. Software monitoring and dual-loop benchmark change the code, what in turn changes the cache behavior. Hardware simulation, emulation, or direct measurement with logic analyzers cover only a tiny subset of the huge set of all possible executions. Moreover, if one takes into account the rate at which the size of typical avionics or automotive programs is increasing, maintaining the coverage of tests at the same level as today is increasingly expensive.

AbsInt's worst-case execution time analyzer aiT solves these problems by a combination of abstract interpretation and integer linear programming. It reads two kinds of input: the executable program containing the tasks to be analyzed, and user input providing additional information. This information falls into two main classes: global information like the clock rate of the microprocessor and the access times of memory, and local information addressing specific program points. This local information complements the results of the various static analyses performed by aiT. In the sequel, we shall introduce these analyses and the respective possibilities for user information. Before doing so, we explain how users may refer to program points.

Program Points

User information may be provided in two ways: as specifications in a separate parameter file called ERTS 2006 -25-27 January 2006 -Toulouse AIS file, or as special comments in the source code (see section 4). aiT is able to scan the source files for such comments, but it also works if no source is available; WCET analysis is based on the executable program.

Both kinds of user information need to refer to program points for various reasons, e.g., as points of reference or as branch targets.

• The simplest way to refer to a program point is by its absolute address in the executable. Yet this kind of program point specification is not very convenient. If the application is modified and then recompiled, the absolute addresses will change and need to be adapted in the user information. This is true even for unmodified routines since they may move to a different location in memory.

• These problems can be avoided to some extent by using relative addressing, e.g., "main" + 0x20 bytes describes a program point by an address relative to the entry of routine main. If the application is modified and then recompiled, only the relative addresses in the modified routines must be adapted.

• Program points may also be specified by symbolic descriptions. For instance, -"prime" + 2 loops is the beginning of the second loop in routine prime, -"find" + 3 reads is the third instruction reading from memory in find, and -"watch" + 1 call is the first call instruction in watch.

Further examples of symbolic descriptions will be presented in the next few sections.

• file 'Name' line Number refers to line Number in source file Name. The translation of this line into an address in the executable relies on the line information that is part of the executable (see section 4).

• The program point description here can only be used in source code annotations and then refers to the line where the annotation starts. This line information is translated to an executable address in the same way as the explicit line numbers presented above.

General Structure of aiT

aiT works on executables because the source code does not contain information on register usage and on instruction and data addresses. Such addresses There are aiT versions for several processor architectures: HCS12 / STAR12, ARM7 TDMI, C16x / ST10, TMS320C33, and Motorola PowerPC MPC 555/565/755. They share a common structure [START_REF] Ferdinand | Reliable and precise WCET determination for a real-life processor[END_REF] described in the following subsections (see Figure 1).

Decoding and Control-Flow Reconstruction

In the first step a parser reads the executable and reconstructs the control flow [START_REF] Theiling | Extracting Safe and Precise Control Flow from Binaries[END_REF]. This requires some knowledge about the underlying hardware, e.g., which instructions represent branches or calls. The reconstructed control flow is described as a combined call graph and control-flow graph, which serves as the input for micro-architecture analysis.

The decoder can find the target addresses of absolute and pc-relative calls and branches, but may have difficulties with target addresses computed from register contents. Thus, aiT uses specialized decoders that are adapted to certain code generators and/or compilers. They usually can recognize branches to a previously stored return address, and know the typical compiler-generated patterns of branches via switch tables. Yet non-trivial applications may still contain some computed calls and branches (in hand-written assembly code) that cannot be resolved by the decoder; these unresolved computed calls and branches are documented by appropriate messages and require user annotations. Such annotations may list the possible targets of computed calls and branches:

INSTRUCTION ProgramPoint BRANCHES TO Target 1 ,...,Target n ; ARM7 TDMI processors do not offer return instructions. Instead, various kinds of computed branches with the return address as target can be employed. aiT can recognize most of these branches as returns. The few remaining ones, mostly contained in library code, can be annotated as follows:

INSTRUCTION ProgramPoint IS A RETURN ;
The ProgramPoint, which refers to the computed call or branch instruction, and the Targets are points in the sense of section 2; they may be absolute or relative addresses or symbolic descriptions. A program point description particularly suited for CALLS and BRANCHES specifications is "R" + n COMPUTED which refers to the nth computed call or branch in routine R-counted statically in the sense of increasing addresses, not dynamically following the control flow. In a similar way, targets can be specified as absolute addresses, or relative to a routine entry in the form "R" + n BYTES or relative to the address of the conditional branch instruction, which is denoted by PC.

Example 1: The library routine C_MEMCPY in TI's standard library for the TMS470 consists of handwritten assembler code. It contains 2 computed branches whose targets can be specified as follows (keywords may be lower case or upper case):

instruction "C_MEMCPY" + 1 computed branches to pc + 0x04 bytes, pc + 0x14 bytes, pc + 0x24 bytes; instruction "C_MEMCPY" + 2 computed branches to pc + 0x10 bytes, pc + 0x20 bytes;

The advantage of such relative specifications is that they work no matter what the absolute address of C_MEMCPY is.

If the application contains an array P of function pointers, then a call P[i](x) may branch to any address contained in P. aiT tries to obtain the list of these addresses automatically: If the array access and the computed call in the executable are part of a small code pattern as it is typically generated by the compiler, aiT notices that the computed call is performed via this array. If furthermore the array contents are defined in a data segment so that they are statically available, and the array is situated in a ROM area so that its contents cannot be modified, then aiT automatically considers the addresses in the array as possible targets of the computed call.

If array access and computed call are too far apart or realized in an untypical way, aiT cannot recognize that they belong together. Similar remarks apply to computed branches via switch tables. In both cases, the array or table belonging to the computed call or branch can be declared by the user. The declaration starts like the ones described above:

INSTRUCTION ProgramPoint CALLS VIA ArrayDescriptor ; INSTRUCTION ProgramPoint BRANCHES VIA ArrayDescriptor ;
Here, the ArrayDescriptor describes the address and the format of the table that contains the call or branch targets. These targets are extracted from the table according to the given format rules.

Value Analysis

Value analysis computes safe lower and upper bounds for the values in the processor registers for every program point and execution context. In many cases, lower and upper bound are identical, i.e., value analysis can predict the exact value. Yet if it should happen that the precision of a value analysis result is not satisfactory, the user may increase it by providing better bounds or an exact value: The first specification says that the instruction at address 0x9110 is always entered with 0 in r3 and 0x10 ≤ r7 ≤ 0x1F. (The values may be entirely different after executing the instruction.) The second specification tells 0 ≤ r2 ≤ 20 when _prime is entered (for all calls of _prime).

INSTRUCTION

The results of value analysis are used for various purposes listed in the following subsections. Each purpose comes with possibilities for specifications better suited for that purpose than the general register-value specifications presented above.

Loop Bounds

WCET analysis requires that upper bounds for the iteration numbers of all loops be known. aiT tries to determine the number of loop iterations by loop bound analysis, a combination of value analysis and pattern matching, which looks for typical loop patterns. In general, these loop patterns depend on the code generator and/or compiler used to generate the code that is being analyzed. There are special aiT versions adapted to various generators and compilers that are quite successful in finding loop bounds automatically. Sometimes they rely on the assumption that generated code is well-behaved. For instance, a common type of loops in generated code is linear search in a sorted array, e.g., while (x > *(x_table++)) ... Here, there is the risk that x is greater than all table values so that the loop continues examining values beyond the end of the table in an uncontrolled way. Yet aiT assumes that the code generator has avoided this error situation by an extra test before the loop or by putting the largest possible value at the end of the table. Then the number of executions of the loop header is bounded by the size of the table. To be on the safe side, aiT issues a message asking the user to verify that the assumption is valid. Despite all sophistication built into loop bound analysis, there may be some loops that are too complicated for automatic analysis. Bounds for such loops must be provided by user annotations. A maximum iteration number of j is specified as follows:

LOOP ProgramPoint Qualifier MAX j ; A ProgramPoint description particularly suited for this purpose is "R" + n LOOPS which means the nth loop in routine R counted from 1. Qualifier is an optional information. It may be one of the following: begin indicates that the loop test is at the beginning of the loop, as for C's while-loops. end indicates that the loop test is at the end of the loop, as for C's do-while-loops. If the qualifier is omitted, aiT assumes the worst case of the two possibilities, which is begin where the loop test is executed one more time. The begin/end information refers to the executable, not to the source code; the compiler may move the loop test from the beginning to the end, or vice versa.

Example 3:

loop "_prime" + 1 loop end max 10 ;

specifies that the first loop in _prime has the loop test at the end and is executed at most 10 times.

Addresses of Memory Accesses

Using the values of the registers, value analysis tries to determine the addresses of memory accesses. These addresses are important for an analysis of the data cache and for determining the duration of the memory accesses. Value analysis usually works so good that only a few indirect accesses cannot be determined exactly. Address ranges for these accesses may be provided by user annotations of the form

INSTRUCTION ProgramPoint

ACCESSES Range ; Useful ProgramPoint formats for such specifications are simple instruction addresses and symbolic descriptions of the forms "R" + n READS and "R" + n WRITES meaning the nth instruction in routine R reading from memory and the nth instruction writing to memory, respectively.

A Range may be a single position in memory, or a range specified by a start and an end position, or an array name meaning the memory area covered by that array (this requires that the debug information in the executable contains the start address and the end address or the length of the array). A position may be an absolute address in memory or an address relative to the beginning of an array (this requires that the debug information in the executable contains the start address of the array).

Example 4:

Assume array TAB is mapped to memory area 0x8100-0x81FF, and the first read instruction in routine main has address 0x8500. Then the following specifications are equivalent: instruction 0x8500 accesses 0x8100 .. 0x81FF; instruction 0x8500 accesses "TAB"; instruction "main" + 1 read accesses "TAB"; The following specifications are also equivalent to each other, but different from the ones above because they refer to the start address of the array instead of the entire extent of the array: instruction 0x8500 accesses 0x8100; instruction 0x8500 accesses "TAB" + 0 bytes; instruction "main" + 1 read accesses "TAB" + 0 bytes;

These specifications are valid no matter whether the read instruction accesses the byte 0x8100 or the word starting at byte 0x8100.

Evaluation of Conditions

If a condition always evaluates to true or always to false, certain program paths are never executed. Therefore, their execution time does not contribute to the overall WCET of the program, and need not be determined in the first place. A similar effect is obtained by user annotations specifying the values of conditions:

CONDITION ProgramPoint IS ALWAYS TRUE ; CONDITION ProgramPoint IS ALWAYS FALSE ;

The ProgramPoint specified should be a conditional branch (not a compare instruction).

Example 5:

The following annotation specifies that no division by zero occurs in the library routine _ _rt_udiv of the ARM compiler for ARM7:

condition "_ _rt_udiv" + 0x4c bytes is always false;

Alternatively, a user may directly specify that a certain basic block is never executed:

SNIPPET ProgramPoint IS NEVER EXECUTED ;

where ProgramPoint refers to an arbitrary instruction in the block, e.g., by its address or by any other way presented in section 2.

Cache and Pipeline Analysis

Cache analysis classifies the accesses to main memory into cache hits, cache misses, or accesses that may be both [START_REF] Ferdinand | Cache Behavior Prediction for Real-Time Systems[END_REF]. Pipeline analysis models the pipeline behavior to determine execution times for sequential flows (basic blocks) of instructions [START_REF] Langenbach | Pipeline Modeling for Timing Analysis[END_REF]. The result is an execution time for each basic block in each distinguished execution context. Cache and pipeline analysis cannot be influenced by local annotations. The cache layout can be described by global specifications. For experimental purposes, there are also global specifications declaring that all memory accesses should be considered as cache hits, or as misses.

Path Analysis

Finally path analysis determines a worst-case execution path of the program from the timing information for the basic blocks. The program's control flow is modeled by an integer linear program [START_REF] Theiling | ILP-based interprocedural path analysis[END_REF] so that the solution to the objective function is the predicted worst-case execution time for the input program.

Path analysis takes into account user-given flow facts that consist of linear constraints for the execution counts of several program points. For instance, flow (0x100) + (0x200) <= 4 (0x300); means that the number of executions of the block starting at address 0x100 plus the number of executions of the block starting at 0x200 is at most 4 times the number of executions of the block starting at 0x300. As always, relative addresses or symbolic program point descriptions may be used instead of these absolute addresses.

Source Code Annotations

User information can be written into a separate parameter file, or inserted into C source code files as special comments marked by the key string ai: /* ai: specification 1 ; ... specification n ; */ The names of the source files are extracted from the debug information in the executable.

Source code annotations admit a special program point or target here, which roughly denotes the place where the annotation occurs (due to compiler optimizations the debug information is not always precise). More exactly, aiT extracts the correspondence between source lines and code addresses from the executable. A here occurring in source line n then points to the first instruction associated with a line number ≥ n. Since the line information in the executable is created by the compiler, it becomes invalid when lines are added or deleted in the source file. Therefore the application must be recompiled whenever lines are added while annotating.

For loop annotations, it is not required that here exactly denotes the loop start address. It suffices that it resolves to an address anywhere in the loop as in the following example: for (i=3; i*i <= n; i += 2) { /* ai: loop here end max 10; */ ... }

Other Annotations

Apart from the annotations described so far, many other properties can be declared in parameter or source files.

• To get any WCET results at all, you must specify upper bounds for the recursion depths of all recursive routines. These specifications are similar to the loop bound specifications described in section 3.

• aiT can be informed about the clock rate of the microprocessor. Knowing the clock rate, aiT can display its results in real time units such as milliseconds. Without this information, all results are displayed in processor cycles.

• End specifications instruct aiT to stop reading the executable at a certain program point. A possible application is for instance to inform aiT that an interrupt routine called by a software interrupt does not return.

• You may specify that a memory area is readonly or write-only, contains data or code. You may also specify which data it contains.

• You may exclude certain routines from WCET analysis and supply their WCET directly.

• You may specify that a routine never returns (like exit).

• You may exclude certain routines from analysis and specify their WCET by hand.

• Program points can be given symbolic names for later reference.

Related Work

In contrast to most approaches proposed in the literature [START_REF] Puschner | Calculating the Maximum Execution Time of Real-Time Programs[END_REF][START_REF] Ko | Supporting the specification and analysis of timing constraints[END_REF][START_REF] Kirner | The Programming Language WCETC[END_REF][START_REF] Ermedahl | A Modular Tool Architecture for Worst-Case Execution Time Analysis[END_REF], our annotations may refer to the source code, but do not extend the source language (annotations are comments), nor do they require a special compiler. Instead, aiT can analyze code generated by standard compilers. The correspondence between source code annotations and low-level object code is exclusively based on the debug information of the executable. Other than the annotations proposed elsewhere, ours cover the full spectrum between reference to source code lines (here) over symbolic descriptions (R + 1 loop) till routine-relative or absolute addresses, the latter being useful for annotating optimized code with instructions that cannot be attributed to a particular piece of source code.

The annotation languages proposed in [START_REF] Puschner | Calculating the Maximum Execution Time of Real-Time Programs[END_REF][START_REF] Ko | Supporting the specification and analysis of timing constraints[END_REF][START_REF] Kirner | The Programming Language WCETC[END_REF][START_REF] Ermedahl | A Modular Tool Architecture for Worst-Case Execution Time Analysis[END_REF] are generally restricted to loop bounds and flow constraints, while ours are more general in that they also admit the specification of targets of computed calls and branches, register values, and addresses of memory accesses. On the other hand, the specialized flow languages, in particular the one proposed in [START_REF] Ermedahl | A Modular Tool Architecture for Worst-Case Execution Time Analysis[END_REF], are more expressive and powerful than our flow constraints. Extensions in this direction are intended, but not yet realized to get a working system as soon as possible.

Conclusion

aiT allows to inspect the timing behavior of (timecritical parts of) program tasks. The analysis results are determined without the need to change the code and hold for all executions with arbitrary input. aiT is a WCET tool for industrial usage. It has been evaluated by Airbus on safety-critical avionics programs with encouraging results [START_REF] Thesing | An abstract interpretation-based timing validation of hard real-time avionics software[END_REF][START_REF] Souyris | Computing the worst case execution time of an avionics program by abstract interpretation[END_REF]. Information required for WCET estimation such as computed branch targets and loop bounds is determined by static analysis. For situations where aiT's analysis methods do not succeed, a convenient specification and annotation language was developed in close cooperation with AbsInt's customers. This effort has contributed to the good acceptance aiT has found among producers of realtime software. aiT enables development of complex hard real-time systems on state-of-the-art hardware, increases safety, and saves development time. At a stage when the software is already available, but working hardware is not, the tool can be used for a performance evaluation. Based on the contributions of the program parts to the WCET one can make design decisions, e.g., with respect to static scheduling or code/data placement. The effects on the cache and pipeline can be viewed using the visualization options of the tool. Causes for unexpected local timing behavior can be identified in this way.

Figure 1 :

 1 Figure 1: Structure of the WCET tool

ProgramPoint IS ENTERED WITH Register 1 =

 1 Range 1 , ..., Register n = Range n ; Registers are specified by name, and Range denotes the range of possible values as a closed interval, i.e., by specifying the smallest possible value n and the largest possible value N in the form n .. N or FROM n TO N. If you know an exact value (n = N), then you need only specify this value.


U Freund

P Braun

J Romberg

A Bauer

D Ziegenbein

P Mai

AutoMoDe -A Transformation Based Approach for the Modelbased Design of Embedded Automotive Software

Keywords: AutoFOCUS, ASCET, INTECRIO, Refinement, Embedded Software

The AutoMoDe approach manages the complexity of embedded automotive systems by employing a stream-based development paradigm which is specifically tailored to embedded automotive real-time systems. In this paper the tailoring process is explained by transforming a traction control system from a stream-based model to an embedded real-time software model and afterwards integrating the software model on an embedded automotive rapid development hardware.

Introduction

The amount of automotive electronics has grown considerably in the last forty years. However, the resulting complexity has reached a level which can hardly be handled by current modeling means. The impact of the complexity to automotive software design has been foreseen more than a decade ago. Several projects have been started since then trying to define methods and tools to manage the complexity of embedded automotive control software by using high-level software structures. For example, ten years ago DaimlerChrysler started to tailor ROOM concepts for body electronic systems in the TITUS project [START_REF] Eisenmann | Entwurf und Implementierung von Fahrzeugsteuerungsfunktionen auf Basis der TITUS Client Server Architektur[END_REF]. In 1998, the French automotive industry started the AEE 1 project [START_REF] Migge | Embedded Electronic Architecture, 3 rd. OSEK/VDX Workshop[END_REF] which was finished in 2001. Both projects resulted in a common European research effort called EAST/EEA [START_REF] Thurner | The EAST-EEA project -a middleware based software architecture for networked electronic control units in vehicles[END_REF]. This project finished in summer 2004 and provided as one of the results an automotive architecture description language (ADL) [1]. Last but not least, the AUTOSAR development partnership [14] provides with the software component description a framework for high-level software description. The described approaches for high-level design, along with commercially available tools for detailed (control) software design, provide a wealth of proven abstraction mechanisms for all layers of the embedded software design chain. Unfortunately, each modeling approach is currently restricted to particular aspects of embedded automotive software design like networks, control-algorithms, or software architecture. An accepted and mature modeling framework integrating the different aspects of embedded software development is still missing. Hence, there still remains a lot of manual integration work to be done when designing an ECU-network. The manual integration work is centered around the questions how to integrate new functionality in existing E/E-architectures or how to optimize an E/Earchitecture for a given number of functions. As a rule, designing an E/E-architecture appears as a mixture of both.

AutoMoDe is a joint research project consisting of members of the Software & Systems Engineering group at the Technische Universität München, Validas AG, ETAS GmbH, Robert Bosch GmbH, and BMW AG. The overall goal of the project is to tackle the integration challenge in model-based automotive development, and develop an integrated methodology for automotive control software based on custom, problem-specific design notations with an explicit formal foundation.

AutoFOCUS Concepts

The concepts developed in the AutoMoDe project are integrated and reflected in the modeling & development framework AutoFOCUS. In this section we briefly detail its semantics and the employed description techniques.

Semantics

Generally, the AutoFocus tool provides an embedded systems specific realization of the FOCUS framework [START_REF] Broy | Focus : Specification and Development of Interactive Systems[END_REF]. Since its conception in 1996, it has been successfully used for modeling a large number of case studies, including, e.g., an automotive body-electronics system described in [START_REF] Braun | Development of a Car Seat: A Case Study using AutoFocus, Doors, and the Validas Validator, in OMER -Object-oriented Modeling of Embedded Real-Time Systems[END_REF]. AutoFOCUS uses a so-called stream-based approach where a system is considered as components exchanging messages explicitly over streams. Basically, a stream is an ordered set of typed messages. Messages in turn are time stamped with 1 Architecture Electronic Embarque respect to a global, discrete time base, as indicated in the lower part of Figure 1.

Figure 1: AutoFocus Execution Scheme

Because the discrete time base of AutoFocus abstracts from implementation details such as concrete timing or communication mechanisms, the use of additional, explicit timing information below the chosen granularity of observable discrete clock ticks is avoided. Examples of for such additional detailed assumptions include, for instance, the exact ordering of message arrivals within a time slot, or the precise duration and delays of transfer. Real-time intervals of the implementation are therefore abstracted by the logical-time intervals. In our opinion, this discrete-time and stream-based programming model, with dedicated timing and typing assumptions, suits the needs of automotive embedded software modeling better than modeling and programming approaches based on sequential languages, like C/C++. However, in order to support the dominating implementation platforms in the automotive field, stream-based models have to be transformed during the design process to OSEKbased real-time systems, with threads programmed in a sequential language. Furthermore, AutoFOCUS implements the main properties of an architecture description language (ADL). These are components, connectors, typed interfaces, and hierarchies. Data Flow Diagrams (DFD), see Figure 3, Figure 4, and Figure 14 -Figure 16, define an algorithmic computation of a component. Graphically, DFDs are similar to SSDs. DFDs are built from individual blocks with ports connected by channels. Typing of ports is dynamic, using type inference properties of operators. A block may be recursively defined by another DFD. The behaviour of atomic DFD blocks is given either through a STD, or directly through a textual expression (function) in AutoFocus' base language. An example of such a function is shown in Figure 5. It is possible to define adequate block libraries for discrete-time computations with this mechanism.

In contrast to the delayed composition primitives in SSDs, the semantics of DFD composition is "instantaneous", in the spirit of synchronous languages [START_REF] Benveniste | The Synchronous Languages Twelve Years Later[END_REF]. In the AutoFOCUS tool, instantaneous communication primitives are accompanied by a causality check for detecting instantaneous (or causal) loops. Note that computations "happening at the same time" on the level of logical time are perfectly valid abstractions of sequential, timeconsuming computations on the level of real-time implementation if the abstract model's computations are observed with a delay, that is such as the delays which are automatically introduced by SSD composition. The duration of the delay then defines the deadline for the sequential computation.

The message-based time-synchronous communication model does cater to both periodic and sporadic communication as required for a mixed modeling of time-triggered and event-triggered behavior. As shown in Figure 1, each channel in the abstract model either holds a message represented by an explicit value or the "√" ("tick") value indicating the absence of a message in that time instant. Thus modeling of event-triggered behavior is naturally covered by the AutoFOCUS notation by reacting explicitly depending on the presence (or absence) of a message. The extended AutoFOCUS notation is described in more detail in [START_REF] Bauer | AutoMoDe -Notations, Methods, and Tools for Model-Based Development of Automotive Software[END_REF].

The frequency of signals as well as event patterns are represented in the AutoFOCUS notation as clocks: That is, each message flow in AutoFOCUS is associated with such a clock. For a given flow, the flow's clock indicates either the frequency of message exchange (periodic case), or a condition describing the event pattern (aperiodic case). Syntactically, a clock is simply a Boolean expression evaluating to logical "true" whenever a message is present on the clock's flow. For comfortable modeling, clocks are supported by an inference system, similar to type inference in programming languages. Communication between differently clocked partitions of the model is supported by appropriate sampling operators.

Example for AutoFocus modeling

A Simple Traction Control System

The AutoMoDe Methodology will be demonstrated by means of a Traction Control (TC) System. As a rule, a traction control system compares the wheel speeds of the driven wheels with the actual vehicle velocity. If the wheel speed is above the actual vehicle velocity, then there is slip which is introduced by the engine torque. In this case, two typical actions are taken.

1. If just one of the driven wheels currently experiences slip, the brake caliper might be actuated actively.

2. If both wheels are currently under slip, the engine torque will be reduced. In a gasoline engine, this might be achieved by manipulating the ignition or the throttle valve.

In this example, we consider the second case only and have chosen the throttle manipulation algorithm. Wheel-and vehicle speed signals are also used in Antilock-Braking-Systems (ABS) which also provides caliper interaction. Therefore, TC systems often come along with an ABS system, doing engine management interaction by means of a CAN-Bus.

The Traction Control Model

Figure 14 shows the traction control algorithm as AutoFOCUS model in its functional environment, namely the ABS system components as well as the throttle controller. The ABS-components shown are reference-velocity (Referenzgeschwindigkeit) determination, wheel-slip and acceleration-control (Bremsschlupf and Beschleunigungsregelung) as well as a coordination of both control strategies. The result of the coordination is a pressure request (Druckanforderung) to the hydraulic valves which manage the fluid supply to the calipers.

From the wheel-speed signals a reference velocity will be calculated against which the actual wheel speeds is compared. The resulting slip is normalized w.r.t. the vehicle velocity and then classified. In this example this means that two different slip values are reached. The slip-determination is shown in Figure 2 while the slip-classification is shown in Figure 3. The rightmost block of Figure 15 influences the current throttle position by a certain amount if the wheel slip of both wheels is outside the limits. The amount of throttle actuation is calculated in the throttle control block as shown in top-leftmost block of Figure 16. This amount is compared with the actual throttle position and the driver wish (targetposition). The result of this comparison drives the throttle-valve. The throttle-valve is itself a dynamic system which has to be controlled. This is done by a PID-control algorithm which limits the throttle-angle.

The actual control value for the throttle drives a motor via PWM-signals. PWM-signal generation is part of the hardware abstraction and is delivered in this example as a graphical representation of a rapid-development system's I/O-boards. The same is done for the wheelspeed-sensors and the throttlevalve sensor. According to the vehicle dynamics, the traction control system is sampled with different rates. For example, the wheel-and vehicle speed determination might run in 6 ms, while the traction control might run in 12 ms. Throttle-control is done every ms. In the stream-based model, the rates are described as different clocks while in the embedded software-model, the differently clocked model partitions will be assigned to disjoint preemptive tasks, each task triggered at a rate corresponding to the clock in the model.

Refinement to ASCET/INTECRIO

Using the stream-based design approach of AutoFOCUS and applying model based checks to the control algorithm is just one crucial part of embedded automotive software development. The properties shown on model level should be retained in the realtime execution scheme too. This execution scheme consists of Interrupt-Service Routines (ISR), Tasks which run so-called processes in a sequential manner, so-called messages as inter process communication (IPC) mechanisms, clusters, modules, and sequence calls. Furthermore, there are I/O devices realizing the interface with the pysical world.

To transform the TC-system from the stream-based world to the real-time world an AutoMoDe refinement chain is introduced which incorporate the ETAS tools ASCET [START_REF]ASCET User Guide V 5[END_REF], RTA-OSEK [START_REF] Livedevices | RTA-OSEK User Guide V 4.0[END_REF], and INTECRIO [START_REF]INTECRIO User Guide V 1[END_REF]. This refinement chain is shown in Figure 4. On the left side, there is the stream-based TC model defined in AutoFOCUS. Its components are transformed to realtime modules, processes, messages and clusters in ASCET, shown in the top-middle. The ASCET codegenerator will transform the clusters to C-code which are then integrated on a Rapid-Development target (as shown in the lower right part). Target integration comprises the implementation of an OS-schedule. The OS-schedule will be derived from the AutoFocus clock-scheme but taking into account furthermore the interrupts as generated by the I/O-boards. The schedule is checked with the analysis feature of the RTA-OSEK configuration tool. The target integration step is shown in the center of Figure 4. In the remainder of this section, the applied transformation steps are described in detail:

• Module-Identification • Sequence-Call-Generation • Cluster-Definition • Software-System Construction • Target-Integration • OS-Configuration.
ASCET modules group processes and messages. Processes perform the algorithmic work by executing sequence calls which are to some extend equivalents to assignments in sequential programming languages, i.e. there are operations and variables. To exchange information with other processes (either of the same or an other module) they read and write to messages. After codegeneration messages are realized as consistent IPC variables. Processes are linked to operating systems tasks therefore performing the actual work.

Module-Identification & Sequence-Call-Generation

The currently used AutoMoDe refinement algorithm transforms the hierarchically lowest level of AutoFocus DFDs to ASCET modules. The notation used for showing the bottom-level DFD clusters in AutoFocus is called Cluster Communication Diagram (CCD), and is detailed in [START_REF] Bauer | AutoMoDe -Notations, Methods, and Tools for Model-Based Development of Automotive Software[END_REF]. Within each DFD, the elementary AutoFocus blocks which are described as terms in a textual language, will be transformed to ASCET sequence calls. An example for this transformation is the function which tests whether the actual slip is above the limit lambda2 as shown in the upper right block of Figure 3. The function of this block is shown in the lowest line of the block properties of Figure 5. The corresponding sequence call in ASCET is shown in Figure 6. The slipclassification component of Figure 3 [START_REF] Schätz | Checking and Transforming Models with AutoFocus[END_REF]. The ODL is a first-order logic language which allows the definition of tests and transformations. Within an ODL expression user interaction is possible. For example a particular clustering algorithm may ask the user to provide a clock and some components using this clock. Afterwards the algorithm transforms the AutoFocus model by inserting appropriate clusters including the necessary rerouting of the communication. These clusters are the base for the next step.

Software System Construction

After all ASCET modules have been clustered to ASCET projects, the ASCET-code generator using the INTECRIO target is applied to all clusters. The result is the C-code per cluster as well as a code description using the SCOOP-IX format. Both description establish an INTECRIO module, not to be mistaken for an ASCET module. The result of all clustering steps is shown in Figure 9 . Sensor-and actuator modules are shown in the left-and right side of the software system directly connected to ports. E.g., the wheel speed calculation is done by edge detection. These ports will interface the modules representing the I/O-boards of an ES-1000 rapid prototyping system. Such a system is shown in Figure 10.

Cluster-Definition

The next refinement step is the clustering of ASCET modules to ASCET projects. ASCET project clustering is a step that is performed semiautomatically and requires user-interaction. For example, the reference speed calculation being mandatory for the anti-lock-bracking system as well as for the traction control is composed of five clusters in AutoFocus and hence are represented by five modules in ASCET. As can be seen in Figure 8, each connector is represented by messages which are shown conceptually in ASCET. Since after appropriate grouping to clusters, all the DFD blocks defining a given cluster are on the same clock, and because the vehicle velocity is used by other functions as well, it is sensible to cluster these components together which means they have to run on the same µC in an ECU and its processes are scheduled in the same OS-task. This clock scheme will be translated to a real-time system where the throttle-controller cycle time is set to 1 ms. In combination with the clock-schemes, there will be a 1ms, a 6ms and a 12ms task. The processes of the INTECRIO modules will be allocated to the appropriate tasks. This is shown in Figure 12. Scheduling algorithms typcially need the worst case execution time (WCET) as input for their calculations. Though there are some promising results for the WCET estimation, the AutoMoDe project still uses heuristic approaches based on the process allocation to obtain very first coarse grain WCET estimates of the tasks. In [START_REF] Bauer | Model-Based Deployment in Automotive Embedded Software: From a High-Level View to Low-Level Implementations[END_REF], a correct-byconstruction method for implementation of timesynchronous AutoFocus programs based on ratemonotonic scheduling is described. The approach uses a double buffering technique for communication from low-frequency to high-frequency tasks. For analyzing this default configuration in the context of the TC example system, we use the planner feature of the tool RTA-OSEK [START_REF] Livedevices | RTA-OSEK User Guide V 4.0[END_REF] which implements algorithms described in [2]. The result of this analysis using rough estimates of the WCET is shown in Figure 13. In the case that the simple topdown, rate-monotonic approach of [START_REF] Bauer | Model-Based Deployment in Automotive Embedded Software: From a High-Level View to Low-Level Implementations[END_REF] is not sufficient for a particular situation, the algorithms described in [START_REF] Manucci | Correct by Construction Transformations across Design Environments for Model-based Embedded Software Development[END_REF] can ensure in a bottom-up fashion that the multiple clock scheme is appropriatly implemented by some given real-time OS schedule. The basic idea of this algorithm is to check whether all signals are read in the appropriate cycle and that a writer is not overtaken by the reader. Nevertheless, it is common automotive design practise to support this analysis by measurements on the real executing system [START_REF] Schäuffele | Automotive Software Engineering[END_REF] using dedicated measurement and tracing tools such as RTA-TRACE

Conclusion

This paper shows how embedded automotive control systems can be modeled in a crisp manner by using a stream-based approach. Systematic application of refinement steps incorporate model transformations that result in executable embedded software.

Acknowledgement

The AutoMoDe project is partly funded by the German ministry of research and education (BMBF) within the "Forschungsoffensive Software-Engineering 2006" program.

Figure 2 :Figure 3 :

 23 Figure 2: Inner View of the Slip Determination DFD

Figure 4 :

 4 Figure 4: AutoMoDe Refinement Toolchain

  is shown as ASCET block diagram in Figure 7. ASCET needs just three sequence calls instead of five because the parameter constructing blocks shown in the left part of Figure 3 are represented by specific blocks in ASCET.

Figure 5 :Figure 6 :

 56 Figure 5: Properties of the Above-Lambda2 Elementary DFD Block

Figure 7 :

 7 Figure 7: ASCET representation of the Slip Classification Component Figure 8: Reference Speed Calculation Cluster in ASCET These clustering algorithms as well as other model transformations are defined in AutoFOCUS with the help of the Operation Definition Language (ODL)[START_REF] Schätz | Checking and Transforming Models with AutoFocus[END_REF]. The ODL is a first-order logic language which allows the definition of tests and transformations. Within an ODL expression user interaction is possible. For example a particular clustering algorithm may ask the user to provide a clock and some components using this clock. Afterwards the algorithm transforms the AutoFocus model by inserting appropriate clusters including the necessary rerouting of the communication. These clusters are the base for the next step.

  For software system construction in INTECRIO, all clusters are imported as INTECRIO modules to INTECRIO and might be further clustered by INTECRIO functions.

Figure 9 :

 9 Figure 9: The Traction-Control System in INTECRIO

Figure 11 :

 11 Figure 11: The Traction Control System in INTECRIO refined to run on a RP-System 4.5 OS-Configuration

Figure 12 :

 12 Figure 12: The resulting OS-Schedule in INTECRIO

Figure 13 :

 13 Figure 13: OS-Schedule Analysis

[

Figure 14 :Figure 15 :Figure 16 :

 141516 Figure 14: AutoFOCUS DFD showing the Traction Control System with its Functional Environment

  and a given pre-condition is true, or, in case no signal is specified, the precondition alone is true. During the transition, internal variables of the assigned SSD can be manipulated as well as signals being sent via the associated ports.

	appropriate signal arrives
	1. In AutoFOCUS, components are called in
	AutoFOCUS System Structure Diagrams (SSD).
	Each SSD has directed ports for the sending
	and receiving of signals. Signals, i.e. messages,
	are typed and communication between SSD
	components deliberately composed with an
	implicit delay. Additionally, an SSD may contain
	local variables. An SSD can be refined by either
	other SSDs or by using an STD.
	2. Behavior is expressed in AutoFocus by State
	Transition Diagrams (STD) and Dataflow
	Diagrams (DFD).
	STDs represent extended finite state machines. As
	such, they perform a transition if either the

  1] Freund, U., et al.: The EAST-ADL: A Joint Effort of the European Automotive Industry to Structure

		Distributed Software. 2 nd Workshop on Embedded Real-Time Automotive Embedded Control
		Systems, Toulouse 2004.
	[2]	Tindell, K., Clark, J.: Holistic Schedulability Analysis
		for	Distributed	Hard	Real-Time	Systems,
		Microprocessing	and	Microprogramming	-

Euromicro Journal, vol. 40, pp. 117-134, 1994


Keywords: Model driven engineering, observers, timed automata, model-checking

Experimentation of Timed Observers for Avionics Models Validation

Ph.Dhaussy 1 , JC.Roger 1 , H.Bonnin 2 , E.Saves 2 , J.Honoré 2 , J.Lohman 2 1: ENSIETA 2 rue François Verny 29806 Brest CEDEX 9 {dhaussy, rogerje } @ensieta.fr 2: CS-SI -Parc de La Plaine -BP5872 -31506 Toulouse cedex 5 {hugues.bonnin, eric.saves, julien.honore, julien.Lohman} @c-s.fr Abstract: Number of avionics systems are designed with formal specification languages, in order to get a clear, unambiguous and complete description of the system. The ATC module, designed with SDL, is a ground/onboard communication system. The SDL description of the system is so rigorous that automatic code generation is used in the system production process. Verifications based on tests are realized on the SDL model, through execution simulation. But SDL mathematical grounds can be exploited in formal verification too, in order to obtain ever earlier the highest level of confidence in the system. The verification of real-time systems by modelchecking has been extensively studied in the last years, leading to important theoritical results. Tools have been applied to verification of real sized systems. The usual approach relies on a model, specifications or properties (requirements) and a model-checking technique to verify the properties on the model. The common work between CS and ENSIETA, reported in this paper, is one of these works. It deals with industrial challenges related to the adoption of formal verification: theoritical remaining problems, tools integration, industrial constraints recognition. In the experiment reported here, we use the observer automata operational formalism for verifying dynamic properties of SDL models. Intuitively, the observers monitor the behaviour of the system looking for violation of properties (for example, safety property). They receive events generated by the system. The observers are executed in parallel with the model in a weak synchronous composition. To ease this composition and therefore support the properties verification of an SDL model, we took the option to translate it in a timed automata based on IF language from Verimag laboratory (observers are also specified in IF). Our first experimentation on avionics case studies was an opportunity to evaluate this technique to verify some behavioural properties. We found that observers are adequate to specify the model behaviour. An appropriate methodology has still to be identified to help user to manipulate them in software design process.

Introduction

Study context

Modern avionics integrate an increasing number of systems, which are more and more complex. In order to meet stringent safety requirements, these systems have to be engineered in a rigorous process supported by methods and tools, better adaptated to these new challenges. Communication is one of the enlarging domain in the aeronautical context: it follows growing circulation in the air space. ATC (for Air Traffic Control) data-link applications are dealing with communications between an Air Traffic Control Center and an aircraft. It allows manual (involving the pilot) and automatic information exchanges such as alerts, position, speed, weather, etc. ; it is used for certain route and departure clearances too. These applications can operate in ACARS or in ATN networks. The study described bellow has been executed on the AFN application, one of the ATC applications. AFN is the "logon" application for all ATC applications, in the ACARS network.

Goals

One of the most productive methodology (in terms of both performance [ie quality, safety] and delays) well designed for communication applications is Model Driven Development (MDD), using asynchronous languages such as SDL (Specification and Description Language). Indeed this approach, using a domain specific language, guarantee to obtain specifications as near as possible of needs. The second benefit is that this language, as its precise semantics defines an execution model, allows to use simulation as a powerful way to early verification. The model is used to generate the final target code too. Today, verification is mainly realized through dynamic tests: execution of the model in the case of simulation, or execution of the final product for other tests (integration, validation). This testing process cannot guarantee the exhaustivity of possible paths coverage. The conclusion of even a huge test campaign cannot be "this property can never arise". This point has to be very carefully considered in more and more complex systems. It is the reason why we consider it is important to explore deeper formal verification on model. This approach allows to formulate properties of the system, on a exhaustive basis, i.e. properties like "this can never arise". The MDD approach allows us to reach this objective: thanks to model transformation into the best appropriate language for formal verification, we can experiment the model verification techniques.

The paper presents, in section 2, the principles of the observer-based verification technique and the implementation with IF language. Section 3 addresses the problem of the manipulation of the requirements and their exploitation for a necessary synthesis of the observer automata. Section 4 presents the environment under development. Conclusions are then given and further works are briefly discussed.

Formal verification by timed observers

Formal verification context

The proof of behavioral and temporal requirements implies model based simulation and the transition system generation on which the analysis of formal properties can be carried out. In much of academic approaches, the recommended method is the use of temporal logic languages, linear or tree structures (LTL, CTL, etc), and the verification of these logic formulas, by model-checking (for example [START_REF] Durrieu | Testabilité des logiciels Embarqués[END_REF]), on the behavior graphs. Many reports were done on the difficulty non specialists engineers have in using these formalisms. This was certainly one of the problems of the penetration of the formal proofs techniques in the industrial engineering processes. To allow their use in the industrial process, it is desirable to provide to the software frameworks user facilities to express logical properties by handling the objects of the model which are comprehensible for him. Often, the designer does not wish to have to learn new specification languages. It is thus interesting to develop interfaces to translate these properties into formulas expressed in temporal logic without the user having to handle them explicitly. Those can be then exploited in the industrial process by mature formal verification tools existing in research centres. Among techniques of expression of formal property, one is based on the observer design.

Observer principle

An observer [START_REF] Aceto | Model checking via reachability testing for timed automata[END_REF][START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF] is an entity that follows the behavior of the system in order to check the failures of them. It is specified in the form of an automaton, which is strongly composed with the system to analyze, in order to generate a reachability graph. It is built so as to encode a logical property and has as a role to observe all the significant events related to the property that we want to check. The observer automaton executes synchronously with the system and monitors run-time state and events of the observed system. It has special nodes known as reject. If one of these nodes is accessible during the composition of the observer with the system to check, then the property is not verified. More precisely, to check a system S, composed of several communicating timed automata, with an observer O, the step is as follows. The observer O is associated S by means of a synchronous composition (S||O). An analysis of accessibility of the reject1 states is carried out on the product of this composition (S||O --> reject). If one of these states is accessible, the property is not verified. If, on the contrary, none is accessible, the property is true. The expression of an observer in the form of automaton seems to be a priori an easier way for the designer. Nevertheless a certain difficulty always remains when the properties to be expressed become complex. The possibilities of transcription errors out of automata comprising many states are quite real. A considered prospect is the automatic generation of observers from specifications of higher level requirements. The goal is to integrate them in the DSL (Domain Specific Language) development framework and thus to allow the handling of the formal concepts via easier constructs use. The important size of the models also requires to consider the possibilities of reduction of the space of the states of the model. One can for example use observers equipped with "cut" operation which make it possible to restrict the behavior of the observed model. A complementary reduction technique of the behaviors of the models is based on the addition of process simulating the environment of the observed model and restricting behaviors. This technique thus makes it possible to initialize the system in configurations, which interest the operator and to identify a desired sequence or a non desired sequence. We currently evaluate this technique and try to identify associated methodology by focusing on systems with important size. We will see thereafter how, with the IF language, we use the operators of restriction and specify the execution context of the analyzed model.

Implementation of the observers

Usually, the use of this verification technique deals with two kinds of observers and an automaton specifying the simulation environment. The first type of observer, named property observer, is used to express a property. The second one, named restriction observer, allows to express constraints on a system. The automaton that specifies the environment of simulation is named context automaton.

The two types of observers are implemented with different observation mechanisms: On one hand, the property observers are non intrusive observers which observe and do not modify the behavior of the system. Their expressiveness is limited to safety and bounded liveness [START_REF] Aceto | The power of reachability testing for timed automata[END_REF]. We show below examples of properties, P1 and P2, for the analyzed avionic protocol. On the other hand, the restriction observers are restrictive observers. They can stop the reachability analysis on some uninteresting paths of exploration. These paths can correspond in not-in conformity or not existent behaviors of the system or environment. Restriction R1 and R2 are two examples of behavior restriction for the protocol. The context automata are intrusive and interact actively with the system. They highly communicate with the system, in the manner to lead it in an interesting configuration. The context automata are implemented using classical communicating automata. They replace the simulation environment. When the input data set of the system is well too broad to be enumerated, such as for example in the case of real numbers or character strings, the graph of the accessible states is infinite thus not exploitable (it is an undecidable problem). An intrusive automaton makes it possible to redefine and limit the input set of the system. The exhaustive exploration of the system thus becomes decidable. The example Context C1 presents a possible environment for the analyzed system. We will see, in section 2.4, that each kind of observer or automaton is written in IF language using annotations and particular operators. We illustrate here their pragmatic use for the avionics protocol example. The first example is a property observers.

Property P1 :

When a plane has checked-in, if the acknowledgement comes after TimeOut units of time, the property will be failed.

Property P2 :

All check-in will receive an acknowledgement (ok or failed).

Next examples concern restriction observers.

Restriction R1 :

A plane won't check-in more than 3 times.

Restriction R2 :

A plane won't change of zone more than 3 times.

The context of an avionic protocol is too big to be enumerated. Considering this, it is important to create a reasonable operational context.

Context C1:

This context considers a plane which can check-in on two stations S1 and S2, and from this two stations it can change from one to the other.

Implementation with IF language

The choice of the implementation language of the models formal verification and the observers was the IF language [START_REF] Bozga | IF-2.0: A validation environment for component-based real-time systems[END_REF] for which many tools were developed. They allow the programs IF and state graph to be generated from higher level and more user level languages (for example SDL, LOTOS, etc.) in order to carry out formal properties checks. The IF processes are communicating by messages buffers timed automata. The communication channels implemented in this language can be parameterized, to specify the type of communication (multicast, unicast, peer), the quality of the media (reliable, lossy), the type of plug (fifo, multiset) and the temporization of the communication (urgent, delay, rate). Advanced data structures allow a fine description of the systems in IF. The simulator of models IF makes it possible to generate an accessibility graph representing the set of all the possible executions of the model. Time in these graphs can be represented in two manners: with discrete time, where the progression of time is implemented by tics of time and each clock has a value. In dense time, the progression of time is implemented by a progression transition and the set of the clocks is characterized by DBMs (Difference Bound Matrices) [START_REF] Alur | A Theory of Timed Automata[END_REF]. VERIMAG developed tools with IF for static analysis of the models such as slice or live, able to carry out a consequent reduction of the models before even the execution of the system. The toolkit CADP [START_REF] Fernandez | CADP: A Protocol Validation and Verification Toolbox[END_REF] developped by INRIA carries out analyses (evaluator, xtl), bisimulations, reductions and abstractions (Aldebaran) on the generated graphs of accessibility. VERIMAG provided libraries, model and simulator, which makes it possible to the users to adapt the design of utilities like code generators or accessibility graphs explorers. Model makes it possible to read a system written in IF and to manage a syntactic tree in memory. Simulator is an essential tool for the realization of explorer of accessibility graphs of models IF. The different kinds of observers described in section 2.2 are established by annotated processes IF observers [START_REF] Ober | Validating timed UML models by simulation and verification[END_REF]. Both kind of observers, property or restriction, defined previously are characterized in IF by the key words: pure for the first one and cut for the second (restrictive). They monitor the system with the match instruction able to detect the occurrences of the signals of the system. It is important to note that the processes observers have priority upon system to validate. Indeed, the IF automata communicate using buffers, however observers need to be strongly synchronized with the system. Their priority level thus allows this synchronous composition.

Moreover, IF allows nodes error and nodes success to be defined. The properties observers are defined with IF pure observers. The marked nodes error make it possible to give a verdict, while the nodes success make it possible to stop the reachability analysis (as a restriction) in a path when arrived in a state considered successful (option "cut on success" of the simulator). The restrictions are expressed in IF with cut observer. These observers can block the reachability analysis in some path using the cut instruction, but they don't contain either error or success nodes. Their role is to reduce the reachability graph, and not to check a property. So, the context automata are described using classic IF process, transforming an open system to a closed one.

Some results

For the avionic protocol, some properties have been verified using this observer technique. As an example, we summarize in table 1 the results for two properties, P1 and P2, given in section 2.2. The protocol has been simulated with the Context 1 and the two restrictions R1 and R2. For Property P1 (resp. Property P2) the protocol system has been composed with the context automaton, the restrictions observers R1 and R2 and the P1 (resp. P2) observer and then simulated. Table 1 The property P1 and the property P2 are both validated in this case.

Translation of requirements into IF observers

One of the motivations of the approach based on the model engineering is to be able to formalize the concepts of requirement and architecture of systems by a set of models. A first difficulty of this step is the taking into account and the handling of the requirements to be validated. A second is the diagnostics exploitation provided by the formal analysis tools, which must be presented at the system designer in specific views and understandable by him, independently of the formal techniques and implemented languages. For the moment, we do not have studied this second aspect. For the requirements handling, the objectives that we fix ourselves are thus to identify the concepts to be introduced into requirements meta-models according to certain points of view of analysis (performance, reliability, etc). Then the translation mechanisms of the requirements models into proof requirements exploited by the formal analysis tools are to be studied. In the current development, the properties and restriction observers or automata context can be generated from higher-level descriptions. For example, we currently transform sequences diagrams into context process or we generate property observers from a more abstract observers formulation. The figure (1) presents a context automaton automatically generated for a case of study of a communication avionics protocol from a sequence diagram. This context present the necessary sequence allowing to configure the state of a communication protocol. The figure (2) presents a property observer generated for the same communication protocol. This is a bounded liveness property expressing, in some case, an error message is sent after a waiting time.

To go further on this way, we seek to identify a language, and thus a meta-model, allowing the requirements description being able to give place to the observers and the context automata synthesis. Many work were invested in this field. For example, in [START_REF] Janssen | Model Checking for Managers[END_REF], a graphic modeling language was proposed and based on requirement patterns. These requirements are translated into linear temporal logic formula and checked with the SPIN model-checker [Hol91]. In [Die96], constraints diagrams, based on the calculation of durations [START_REF] Chaochen | A Calculus of Durations[END_REF] are used to specify properties. [START_REF] Nébut | Une méthode de formalisation progressive des exigences basées sur un modèle simulable[END_REF] presents a refinement method of requirements towards models. The requirement language exploited is RDL (or Requirements Description Language) defined for the avionics systems within the CAROLL project 2 framework.

Functionalities of the environment under development

We exposed until there the guiding principles to build an environment of models validation. We point out that the objective is to have a study framework to experiment the formal techniques to check industrial models. All the ideas evoked previously were the subject for the moment of a beginning of implementation. Nevertheless, the state of the platform allows us today to lead proofs of an embedded model of avionics software. Thus, the environment which we are currently developing allows: 1) to import models UML or SDL and to translate them into models IF, 2) to express behavioral properties coming from the requirements and to translate them into observer automata IF, 3)

Conclusion and further work

In this on-going experimentation, we want to study the verification technique of dynamic properties of SDL models. For that, we use an operational formalism, observer automata, which represent specifications to validate on the model. We seek to currently validate the basic principles of our method on the analysis of an avionics communication protocol (AFN protocol) whose size, although reasonable, is that of an industrial study case. The first results show us that this technique can be used to verify some safety and bounded liveness requirements. The complexity of this protocol is such that it enables us to be confronted with methodological problems: how to describe the context automata and the observers ? How to handle the restrictions to circumvent the explosion of the behaviors number and to ensure the relevance of the analyzed executions? In this work in progress, we treat the aspects related to the abstraction and the reduction of the system behavior in the same formalism as that which allows the expression of the properties. Indeed, the observers and the contexts are automata. Our experiment consolidates us in the idea that the handling of these automata can be exploited in a software engineering process more easily than using formal languages like temporal logical ones. The condition is to be able to control their synthesis from requirements easy handled by the engineer. Many academic works explored various formalisms or languages and contributed to the design of software modeling, simulation and validation tools. Many projects were implemented to apply these techniques for industrial applications and real cases. But we still note today their weak penetration in the system and software engineering processes comparatively with the drastic reliability and safety needs of critical systems. This paradox partly finds its causes in the real difficulty to handle theoretical concepts and formal methods within an industrial framework and the many problems unsolved as for the treatment of complex systems subjected to strong constraints (real time, criticality, deployment). More and more work in industrial contexts are done in this area. The common work between CS and ENSIETA, reported in this article, is one of these works. It deals with industrial challenges related to the adoption of formal verification: theoritical remaining problems, tools integration, industrial constraints recognition. Indeed, one of the main remaining problem in the formal verification area, is the combinatory explosion of states graphs. Studying property observer, restriction observer and context automaton techniques is the way we think the more suitable for industry applications in terms of methodology and capitalization. In the tools area, this experiment allowed us to integrate IF tools, in the perspective of industrial usage (writing helps, guides, scripts, etc). Finally, considering industrial constraints such as DO178 or ARP4754 standards, CS acts in the working groups to advocate this MDD approach with its formal verification aspects. We are convinced that these approaches will help facing the challenges of high reliability and complexity of the present and future critical systems.

2

  Research program of CEA, INRIA, THALES started in 2003.

Figure 1 :Figure 2 :

 12 Figure 1 : Generated context automaton

A reject state is a state of accessibility graph corresponding in a reject node of the observer automaton.