M Hagner
email: hagner@ips.cs.tu-bs.de

M Huhn
email: huhn@ips.cs.tu-bs.de

A Zechner
email: zechner@ips.cs.tu-bs.de

Timing Analysis using the MARTE Profile in the Design of Rail Automation Systems

Keywords: MARTE, Timing Analysis, Rail Automation Systems, CENELEC

published or not. The documents may come

L'archive ouverte

Introduction

Dependable systems are in many cases hard real-time system i.e. if the timing behaviour violates the requirements, the system reaction has to be considered as faulty because of potential severe consequences. Therefore, timing requirements as other runtime properties, which are in non-dependable software design considered as extra-functional like availability, are taken into account from the very beginning of the development process. Within each design phase a catalogue of measures is employed to assure predictable behaviour.

However, nowadays standardised tool-supported model driven development for the application logic on the basis of UML or SysML is on the rise in the railway domain. Moreover, todays rail automation systems are composed out of a set of configurable components to improve reuse. On the other hand, COTS products for hardware components and lower middleware layers find their way into this segment dependable systems. All these require a new treatment of real-time requirements that supports tracing through the model driven design and automated timing analysis for verification. An answer is MARTE (A UML Profile for Modelling and Analysis of Real-Time and Embedded systems) [START_REF]UML Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) RFP[END_REF], a new UML profile extension for embedded and real-time systems. It is proposed by the "Pro-Marte" consortium1 consisting of academics, tool providers, and OMG end-users. The goal of the consortium was to define a concept, in terms of UML extensions, to model real-time and embedded systems. The MARTE Profile is a successor of the Profile for Schedulability, Performance, and Time (SPT Profile) [START_REF]UML profile for schedulability, performance and time[END_REF] and the QoS Profile (Profile for modeling quality of service and fault tolerance characteristics and mechanisms) [START_REF]UML profile for modeling quality of service and fault tolerance characteristics and mechanisms[END_REF]. The profile consists of three main packages (see Figure 1). The MARTE foundations package defines the basic concepts to design and analyze an embedded, real-time system. The MARTE Design Model offers elements for requirements capturing, the specification, the design, and the implementation. Therefore, it provides a concept for high-level modeling and a concept for detailed hard-and software description. The MARTE Analysis Model defines specific model abstractions and annotations that could be used by external tools to analyze the described system. Therefore, the analysis package is divided into three parts, according to the kind of analysis. The first part defines a general concept for quantitative analysis techniques; the second and third parts are focused on schedulability and performance analysis. The analysis package was designed with reference to a number of tools that are specialized to analyze the scheduling behaviour of systems (SymTA/S [START_REF] Henia | System level performance analysis -the symta/s approach[END_REF], TIMES [START_REF] Fersman | A generic approach to schedulability analysis of real-time tasks[END_REF], or MAST [START_REF] Gonz | Mast: Modeling and analysis suite for real time applications[END_REF] ).

Standards for Functional Safety in Railway Applications

The railway is one of the safest means of transport, comparable to civil aviation. However, as with other complex systems, despite all efforts to avoid them, accidents do occur again and again, since railway is transport of big masses, some of them even with catastrophic consequences. Therefore standards are of central importance when developing electronic and programmable systems for safety critical functions. The CENELEC2 standards EN50126, EN50128 and EN50129 give recommendations to railway companies, industry and suppliers for consequently applying quality management (RAMS3 ). Application of those standards has to be carried out systematically during all phases of a product's life cycle.

Quality Management

Due to the fact that failure in safety relevant functions of railway systems may have dramatic consequences, the main focus in RAMS management lies on the safety aspect. CENELEC standards call for an assurrance that the risk of severe hazards is minimized to an acceptable risk [START_REF] Braband | The CENELEC-Standards regarding Functional Safety[END_REF] which is usually expressed as Tolerable Hazard Rate (THR). System failures may origin from two different kinds of reasons:

• random or aging effects on the material

• systematic errors from incorrect design

For the first probabilistic methods can be applied, but the second kind needs another treatment since systematic errors cannot be quantified with mathematical means. In order to prevent systematic errors and random failures, the concept of Safety Integrity Level (SIL) is applied. SIL is a classification related to ranges of THRs. As a SIL comes along with a catalogue of measures to be applied in the different phases of a product's life cycle, SIL addresses in particular systematic errors in the design by recommending methods and practices for the development process.

Development Processes

According to EN50126 [START_REF]CENELEC. EN 50126 -Railway Applications -The Specification and Demonstration of Reliability, Availability, Maintainability, and Safety (RAMS)[END_REF] the system development process comprises several phases: concept, system definition, risk analysis, system requirements, apportionment of system requirements, design, and implementation. Further refinement of the process leads to the loosely coupled development processes for hardware and software. When designing and assembling hardware made of COTS 4 and rather simple electric circuitry most of the RAMS qualities can be addressed directly because of the physical and probabilistic properties of the single parts from resistors to complete electric circuits. Software is immaterial and does not suffer from statistic errors that is why EN50128 [START_REF]EN 50128 -Railway Applications -Software for Railway Control and Protection Systems[END_REF] introduces Software SIL. As a consequence the standard makes recommendations for tracing requirements, using formal or semi-formal methods for design and verification and execution of certain test procedures according to the SSIL that is assigned to the function or subcomponent under development. Furthermore EN50128 proposes phases and artefacts for a software development process (see Figure 2). The development process for software starts with the software requirements specification phase. As inputs serve documents from system requirements specification, system safety requirements, system architecture specification, and software quality assurance plan; outputs are requirements and test requirements. Recommendations for this phase include formal, semi formal, and structured methods like CCS, temporal logic, function block and sequence diagrams, SDL, Yourdan, etc.

Software requirements specification, system safety requirements, system architecture specification, and software quality assurance plan form the basis of the software architecture phase. The software architecture specification has to identify all software components and subsystems, document and analyse interactions between software and hardware, and provide traceability of requirements. The standard proposes fault tree analysis, software error effect analysis, and several programming techniques and best practice architecture fragments.

A design and implementation phase basically ends the constructive part of the software development process. The design has to give detailed information on interfaces of all software components and modules. Every kind of module has to be specified exactly regarding data structures, diagrams of data and control flows, and algorithms. Software module specifications shall be sufficiently detailed for further implementation and coding of a module. Here again recommendations for formal, semi formal, and structured methods can be applied. Object-oriented or module-oriented approaches, coding guidelines, programming languages with certain properties, restriction to a subset of a programming language, utilisation of approved or certified software libraries, and other programming related issues extend the list of recommendations.

Figure 2: Software development process [START_REF] Braband | The CENELEC-Standards regarding Functional Safety[END_REF] Model checking and the like are methods for proving pure functional correctness in the meaning of reactive, computational behaviour. Besides timed Petri nets or temporal logic the CENELEC standards give only marginal recommendations for checking, tracing, and proving correct temporal behaviour. In particular this applies to the architecture and design phases. However, this does not reflect the state of the art in real-time modeling and analysis and in particular for complex dependable systems it is mandatory to assure timing correctness as that timing is a safety relevant matter whether for the functional behaviour or for the prevention of hazards to minimize detection time of failures and to initiate fail safe reactions.

Case Study

The German railroad network comprises about 50,000 level crossings. According to the laws and regulations of Germany and Switzerland railway lines may be equipped with crossings where trains travel with up to 160 km/h. Due to this european railway standards [START_REF]CENELEC. EN 50126 -Railway Applications -The Specification and Demonstration of Reliability, Availability, Maintainability, and Safety (RAMS)[END_REF] demand high requirements for automatic protection systems concerning reliability, availability, maintainability and safety.

In this case study we will examine the development of an automatic train level crossing system with supervision signal. The purpose of such a system is to prevent street traffic from entering the crossing while trains are approaching it or pass through the crossing. A level crossing system with supervision signal works as an autonomous system; interaction with a railway control centre or interlocking is not necessary.

Basic Execution of Protection

When railway vehicles are approaching a level crossing, road users have to be signalised. On technically safeguarded level crossings this is realised indirectly via the train activating the protection process. The interval of time between announcing the approaching train to its arrival on the crossing must be sufficiently long for road users to either come to a halt before the rails or to enter the area and to safely clear before the train arrives at the level crossing. Not until successful safeguarding the train may pass the level crossing. When the complete train has depleted the level crossing, road users may be given way to cross the rails.

System Boundaries

A protection system for level crossings obviously has boundaries towards its environment: the railway system (train, rails, etc.) and road traffic. Laws and regulations prescribe more detailed restrictions on the concrete interfaces. The level crossing protection system has to warn road traffic by a set of lights comprised of a yellow and a red light with conventional meaning. Additionally the level crossing can also have gates faced toward the street. A railway signal, namely the supervision signal, shall inform the train driver of the state of the level crossing. Besides those prescribed interfaces a protection system also needs an interface component for detecting trains.

Regarding the fact that we will focus on software development -ignoring the true physical boundaries to the environment like climate conditions, electrical interfaces, etc. -our list of interfaces is sufficient.

Variants of Automatic Level Crossing Protection

Protection systems for level crossing are conceived for different operational purposes. Besides the design with supervision signal other systems exist which are remotely controlled by interlockings from railway control centres or manually operated from station personnel. As initially mentioned a protection system with supervision signal works independently from other train operating or control systems which could influence train movement and prevent a train from entering when the crossing is not guarded against road traffic. In this variant the maximum speed of trains is limited to 120 km/h. The supervision signal is faced towards approaching trains and shows whether the protection system works and the area can be entered safely or not. Its placement is in a safe stopping distance from the grade crossing; so the train driver can react and initiate braking. The signal can show two signal aspects LC1, a blinking white light indicating that the facility is safe, or LC0 otherwise. Its activation takes place as soon as the set of lights is showing red.

Parameters and Constraints

Regarding the operation of protection described earlier we get several constraints and parameters which have to be taken into account when developing a protection system:

•

The Development Process

Here we show how to integrate the MARTE profile for specifying real-time properties in a model based development process conforming to CENELEC. Our focus lies on software development but MARTE can be used from early phases of requirement specification on the system level till implementation. We will go through all development phases but after the system architecture phase we concentrate on software development 5and will introduce artefacts of the hardware parts only when required for understanding.

Phase 0 -User Requirements Specification

In the railway domain user requirements are stated by railway companies, which typically have a long history. Alike is the form of user requirements in this domain. Some come from descriptions of operating procedures for railways -mostly written for railway personnel -, sometimes involving descriptions of existing technology. The operation procedures contain explicit time constants for end-to-end paths for functions such as safeguarding the level crossing. Furthermore legal constraints also have to be considered as a source of requirements, next to the tacit knowledge of domain experts. However, in this paper we refer to the more or less formal description of the case study as the user requirements specification in our development process.

Phase 1 -System Requirements Specification and System Architecture

Unlike all other phases this phase is twofold, it contains all system level activities of the development reflecting our concentration on software development. System requirements capture the user requirements and enrich them with goals and requirements of the developing manufacturer like for instance product line development. Furthermore requirements are usually conditioned for further engineering use thus they are getting more technical.

Thereafter follows system architecture. Major system suppliers for railways typically have existing solutions and platforms which fulfil typical requirements of railway standards; especially some generic documents for certification purposes already exist. A system architecture specification collects solution ideas to address functional and extra-functional requirements making use of generic components, COTS, and deciding where new subsystems either hard-or software have to be designed. Using MARTE can help to improve the architectural decision process by making inherited and derived requirements more explicit.

System Requirements Specification

The level crossing system consists of gates, a set of lights, a supervision signal, and activation and deactivation sensors to detect approaching or leaving trains. The arrangement of these elements is depicted in Figure 3.

Set of lights

Supervision signal

Gate

Activation sensor

Deactivation sensor

Figure 3: Schematic view on the level crossing system If a train approaches to pass a level crossing, it first passes the activation sensor (e.g. an axle counter). Hence, the level crossing system recognizes a train coming and starts to prevent the road traffic from crossing the rails. Therefore, it switches the traffic lights yellow. It is well-defined, how long the lights have to stay yellow. If the level crossing is constructed for traffic speeds up to 70 km/h, the set of lights have to stay yellow for three to five seconds. Next the lights are switched to red. The level crossing system has to monitor whether turning the red light on was successful, i.e. the status from the set of lights has to be read. Only afterwards the supervision signal is switched on (showing signal aspect LC1). About 7 seconds later the gates start to close. The time required for closing the gates depends on the length of the gate's bar. If the bars are longer then 6 meters, it can take up to 10 seconds and if they are shorter, 6 seconds.

Right beyond the level crossing is the deactivation sensor. This sensor detects the leaving train; following the gates can be opened, the traffic lights are turned off, and the supervision signal shows LC0 again.

One requirement of the level crossing system is that the actions to protect the level crossing have to be executed fast enough. The supervision signal has to be in LC1 mode 7 seconds before the train passes the signal. These 7 seconds are necessary for the engine driver to recognize the signal and are defined in the engineering standards. If the supervision signal is not in LC1 mode, the engine driver has to stop the train.

The time that remains to switch the supervision signal to LC1 depends on the distance between the activation sensor and the supervision signal. If the distance is longer, the train will take longer to reach the point where the driver has to recognize the supervision signal, thus the system has more time for its interactions. Because of cable costs and costs for the installation and maintainance it is an effort to keep the distance between the sensor and the supervision signal as short as possible. However, the switching order and time intervals inbetween, a minimal distance between the activation sensor and the supervision signal can also be calculated. The distance between the supervision signal and the level crossing is fixed, because it directly depends on the braking distance of the train at maximum speed. In our case study the distance between the activation sensor and the supervision signal is defined to 450 m, which implies that the supervision signal should be in LC1 mode 6.5 seconds after the train passes the sensor (7 seconds before the train passes the supervision signal). Then, the red traffic light is on and 7 seconds later, the closing of the gates should begin. It takes up to 6 seconds afterwards to close the gates. As a result of these constraints, the complete protection of the level crossing has to be finished after 20 seconds (time to switch the supervision signal + red light phase + time to close the gates + processing and communication time). This is one of the main requirements.

System Architecture

In this phase, there is no detailed resource modelling. A fragmentary choice about the hardware architecture is done, mainly influenced by experiences made in previous projects or by applicable COTS. However, there is no final decision about e.g. a specific CPU. Tasks are not described in this phase, because tasks are not yet identified. Hence, no detailed scheduling analysis is possible. A more considerable method at this point of the development is to refine and capture the requirements in the UML model (like execution path deadlines of functionalities etc.) and define the interfaces (which components are connected with each other). Therefore, UML diagrams are extended using the MARTE profile.

Figure 4 shows a component diagram of the level crossing system. The levelCrossingSystem offers two services (represented as methods): one service to prevent the traffic Figure 4: Component diagram of a level crossing system from crossing the rails and switch the supervision signal in LC1 mode (protectLevelCrossing) and one service to open the level crossing again for the traffic and to switch the supervision signal to LC0 mode (unprotectLevelCrossing). These two services represent the main functionality of the system. The train component represents an approaching train that triggers the protection of the level crossing (the service protoctLevelCrossing). Afterwards the level crossing system sets the lights, switches the supervision signal, and closes the gates. The execution flow of these actions is depicted in Figure 5. There is a similar diagram for the unprotectLevelCrossing service of the level crossing system.

The stereotypes used for this diagram are defined in the MARTE specification for a MARTE Design Model: rtUnit -"rtUnit" marks the component as a realt-time unit. rtService -This stereotype implies that this function is a realtime service.

rtf -This stereotype gives the developer the possibility to use the tagged value "absDl" and "occKind".

In Figure 4 the LevelCrossingSystem is represented as a component using the stereotype "rtUnit". The methods of this component (the services) are marked with the stereotypes "rt-Service" and "rtf". With the "absDl" and "occKind" tagged values a deadline and the arrival pattern of the initiating event can be defined for the corresponding functionality. The values are directly derived from the requirement specification. One requirements is that the protection of the level crossing has to be finished after 20 seconds. This is now captured in the com-ponent diagram with the deadline of the protectLevelCrossing service.

A refinement of the requirements is already done in this phase. The user requirements specification defines that the protect-LevelCrossing service has a deadline of 20 seconds. Another requirement is that the supervision signal has to be in LC1 mode after 6.5 seconds. The following equation shows, how the requirements are distributed: 6.5 s = t yellow + tcommunication + tprocessing Derived from maximum car length, stopping distance of road vehicles, and their minimum depletion speed of the crossing, follows that the lights have to be yellow for 5 seconds (t yellow = 5 s). Hence, it is easy to calculate that there are 1.5 second left for the communication between the elements of the level crossing (tcommunication) and for the processing of the commands (tprocessing). This is possible for this case study, because of the low complexity of the interactions of the level crossing system (i.e. there are no backward loops or data dependencies thus simple addition of numbers or intervals suffices).

The execution flow of the actions can be defined in sequence diagrams or activity charts. Figure 5 represents the actions of the safeguarding process. In this diagram, it is possible to give a more detailed description about runtime of actions or requirements. Therefore, the Value Specification Language (VSL) can be used. In Figure 5, two variables are defined. The first t0 is the mark, where the service levelCrossingSystem is triggered. Later the set of lights should switch to red. Afterwards the supervision signal should be set to LC0 (the light blinks soon enough for the engine driver that the train does not need to be stopped). This has to happen 6.5 seconds after the approaching train triggered the level crossing system. From 12 to 14 seconds after the train triggered the level crossing system, the system starts to close the gates. The last requirement for this service is that the gates have to close within 6 seconds. Again, all values are directly derived from the requirements specification.

Phase 2 -Software Requirements Specification

At this stage of development as a result of the system architecture phase apportionment of functions and assignment to COTS, pure hardware and software has already been accomplished on a level of coarse subsystems. Requirements regarding functions assigned to software have to be collected and refined. In an iterative execution of the process the boundaries of the software system will get clearer over time due to results and choices from the concurrent hardware architecture process. Thus, high-level functions assigned to software realisation have to be split to meet the new boundaries.

In our case study, functional integration and control of all hardware and COTS systems shall be performed in software. The software has to read and interpret values from axle counters and simple I/O-hardware. On the other hand it controls and sends data in given telegram message formats to those elements. Some parameters e.g. bar length type and a lot more have to be configurable. Although software or software architecture itself cannot fulfil timing requirements on its own it is inevitable to inherit and track such requirements for later phases. Nevertheless, architectural decisions on the software level may influence satisfiability of requirements positively, e.g. in separating timing critical from other functions [START_REF] Bass | Software Architecture in Practice[END_REF], or negatively. In addition choosing architectural styles or best practice methods and solutions for the software infrastructure, can ease predictive validation of timing requirements.

Phase 3 -Software Architecture and Design

As in this phase the software structure is developed, the architecture and the behaviour of the system is described in more detail. Hence, it is possible to give more precise predictions about the timing requirements of the system. These predictions can be made using scheduling analysis tools (e.g. SymTA/S [START_REF] Henia | System level performance analysis -the symta/s approach[END_REF] or MAST [START_REF] Gonz | Mast: Modeling and analysis suite for real time applications[END_REF]). The metamodels of (UML or SysML based) CASE tools and timing analysis tools differ and thus, an analysis on the basis of UML models is only possible after a transformation from the UML metamodel into the metamodel of the chosen scheduling analysis tool. Moreover, the UML model has to be completed with respect to timing analysis: It is necessary to add priorities, scheduling algorithms, task execution times etc. To keep this information added for timing exploration separated from requirements and design decisions, one possibility is to create a scheduling analysis view [START_REF] Hagner | Tool support for a scheduling analysis view[END_REF]. This view should contain all necessary information for a scheduling analysis.

The scheduling analysis view uses the following stereotypes:

SaExecHost -This stereotype describes a CPU or other device which executes functional steps.

SaCommHost -This stereotype marks a component as a communication channel.

Scheduler -If necessary, it is possible to use this stereotpye to define an explicite scheduler. Otherwise, this can be done with a tagged value of the "SaExecHost" or "Sa-CommHost " stereotype.

SchedulableResource -A SchedulableResource is defined as a kind of concurrency resource with logical concurrency.

SaExecStep -A "SaExecStep" is a kind of step that represents a usage of a resource, like a CPU.

SaCommStep -A "SaCommStep" is a kind of step that represents a usage of a communication media.

SaEnd2EndFlow -End-to-end flows describe a unit of processing work in the analyzed system, which contend for use of the processing resources.

GaWorkloadEvent -Defines a stream of events that make up a workload which drives the system. allocated -This stereotype maps a "SchedulableResource" on a "SaExecHost" or "SaCommHost ".

SharedResource -Resources like memory or I/O devices are described with the "SharedResource" stereotype.

Most of the introduced stereotypes are defined in the MARTE specification of a scheduling analysis model (MARTE Analysis Model). Our collection of stereotypes is based on the metamodel of scheduling analysis tools like SymTA/S.

Figure 6 shows a class diagram of the scheduling analysis view that describes the structure of the level crossing system. The functionalities/the tasks are represented by methods of the "SchedulableResource" marked classes. The "SchedulableResources" are mapped on resources (like processors or busses). This is done using the "allocate" stereotype. The tasks are described using the "SaExecStep" stereotype. All components communicate with each other over a bus. The methods that represent the communication are extended with the "SaComm-Step" stereotype.

Figure 6 depicts the entire level crossing system. Beside other things, it consists of a component ControlUnit. This component is refined in the class diagram presented in Figure 7 which lists all tasks of the ControlUnit. Part of this list are tasks to check the behaviour of the unit (systemIntegrity-Check, cycleTimeMonitoring), tasks to control the set of lights (sendSetYellow, checkRedStatus . . . ), tasks to initiate the closing and opening of the gates (closeGates, openGates), etc.

Details about tasks and scheduling parameters are examined during this phase. These details can now be added to the model using tagged values (see Figure 8). Thus, it is possible to define deadlines, execution times, priorities, etc.. For a scheduling analysis, it is necessary that all time/scheduling concerning information are added to the model. The execution times can be estimated from experts or measured from previous projects. The response times are calculated using the analysis tools, and afterwards transferred back into the model (where the variable r1 is defined in Figure 8). The dependencies of tasks and the execution order can be illustrated using activity or sequence diagrams. The diagrams are used to show the workload behaviours. This is done using the "GaWorkloadEvent" and the "SaEnd2EndFlow" stereotypes. The corresponding tagged values offer enough opportunities to describe the situations (e.g. the arrival pattern of the approaching train or the deadline of an execution path).

One important requirement for the level crossing system is that the supervision signal is in LC1 mode soon enough for the engine driver to recognize it, so the train does not need to be stopped. The order of the actions, that are executed when a train approaches, has been described in the system requirements specification (section 4.2). This workload situation is described using sequence or activity diagrams.

It is possible and one of the main purposes of the scheduling analysis view, to transform a model into the format of a scheduling analysis tool. The analysis results show whether deadlines are met, execution paths are executed fast enough, etc. The results of the analysis can be transferred back into the UML model. In Figure 9 a part of the level crossing system is depicted in SymTA/S. The tasks are mapped on resources and connected using event streams. On the SymTA/S model an analysis can be executed automatically.

The hardware is developed in parallel and so the scheduling analysis view may change iteratively. New hardware decisions may have great impact on the timing behaviour of the system, because of their influence on execution times, blocking times etc. For the hardware development, the MARTE profile can also be used. Elements for detailed hardware modeling are part of the MARTE design model. Nevertheless, the focus of this document lies on the software modelling. The analysis results of the scheduling analysis view may also have influence on the hardware development. If a result of the analysis is that a utilization of a resource is too high or a deadline is missed, it may be a solution to employ faster hardware. In this phase, the design, implementation, and calibration is done. It is still recommended to use scheduling analysis during the implementation and calibration phase. As the structure of the system developed in phase 3 is fixed, the model (especially the scheduling analysis view) can still be used for further analyses. The task execution times now can either be calculated or measured times. Therefore tools like aiT [START_REF] Ferdinand | Reliable and precise wcet determination for a real-life processor[END_REF] or RTA Trace 6 . As now code exists the realised hardware/software system can be validated for the first time. However, using formally founded worst case execution time calculations like done by aiT and scheduling analysis is of additional value, because then the anaylsis result is a verification and not only a simulation based and thus incomplete statement.

Lessons Learned

MARTE offers manifold possibilities for modeling embedded systems. Because of the broad scope of the profile, it is nontrivial to select an appropriate set of elements for a specific modeling purpose that also meets to the needs of a dependable system design process as a whole like seamless tracing or completeness for automated analysis. This is true even more, because in the manufacturing of complex software systems many developers only have a partial view on the design. In discussions with practioneers it turned out that a restricted 6 http://www.etas.com/de/products/rta trace.php set of MARTE profile elements and guidelines for their use in a certain development phase is preliminary for a successful transfer into practise. Modeling rules and guidelines releave the developer from the complexity of UML and the MARTE profile and therefore increase productivity because the developer can concentrate on the modeling but integrate the timing easily. As a step in that direction we defined a scheduling analysis view [START_REF] Hagner | Tool support for a scheduling analysis view[END_REF] with guidelines to assure the extension of a design with timing and resource information leads to a model that is complete w.r.t. a scheduling analysis. Moreover, the timing related information, that is exclusively required for analysis purposes, is added in a separated view to the model to avoid the overloading of the design model in particular with temporary information that is only of use to explore and evaulate a number of design alternatives.

A major benefit of modeling guidelines is that transformations to analysis tools can be easier automated. This is due to the fact that the automatic transformations can be kept simpler if the structure of the MARTE extended UML model is restricted. This is especially helpful for the scheduling analysis views, used in phase 3 (see section 4.4).

On the OMG MARTE homepage 7 the Papyrus for UML tool 8 is proposed. The Papyrus for UML project offers an add-on for their modeling tool that includes all MARTE elements. With this tool and the add-on, it is possible to create models conforming to MARTE. Papyrus for UML is still under development. Thus, there are some features, which do not work properly (e.g. using activity charts) until now.

Conclusion

We have presented how to use the MARTE profile within system and software development process conforming to domain specific standards for safety critical systems. In the early phases, it helps to capture and visualise the timing requirements with UML conforming notations. In the later phases, MARTE annotations can be used for scheduling analysis before any implementation takes place. As a case study we have shown how to enrich a model of a level crossing protection system for scheduling analysis. The extended model can be used as an input for automatic scheduling analysis tools. The CENELEC standards give only marginal recommendations for checking, tracing and proving correct temporal behaviour. As we have shown, the integration of timing requirements into a model based, tool supported design methodology is useful and necessary. The future versions of the standards should be extended by recommendations for acquisition and refinement of timing requirements during the development of safety critical and programmable systems.

Figure 1 :

 1 Figure 1: MARTE architecture model

  Maximum allowed speed of trains • Diameter of level crossing • Maximum expected length of road vehicles • Minimum expected depletion time of road vehicles • Stopping distance of road vehicles including time to react • Train deceleration at emergency brake • Reaction time of the train driver Most of those parameters and constraints result in requirements as we will see later.

Figure 5 :

 5 Figure 5: Sequence chart representing the protection of the level crossing

Figure 6 :

 6 Figure 6: Sequence chart representing the protection of the level crossing

Figure 7 :

 7 Figure 7: A more detailed representation of the ControlUnit component

Figure 8 :

 8 Figure 8: Tagged Values

Figure 9 :

 9 Figure 9: A workload situation in SymTA/S

http://www.promarte.org

European Committee for Electrotechnical Standardization

Reliability, Availability, Maintainability, and Safety

Components Off The Shelf

HW development will ideally take place in parallel.

http://www.omgmarte.org

http://www.papyrusuml.org

Acknowledgements

We are grateful to Stefan Gerken from Siemens Transprotation Systems for fruitful discussions on a subprofile applicable in practise as well as the Symtavision GmbH for the grant of free software licenses.


Norbert Neuendorf

René Knorr

Comparison of functional integration methods from aviation and automotive industries

Keywords: Functional architecture, communication structures, artificial co-driver, joint solutions

Abstract and Introduction

Both automotive industry and aviation have to put in a variety of efforts to integrate new functions into their systems that will resolve problems still unresolved. In both areas unresolved problems can especially be found where cross-linked systems are the prerequisite for solution. Current technical and functional architectures are suited for this application only in a limited way. Therefore this article will give an outlook to the future of both military and civil architectures, as they are the basis for functional integration.

Automotive industry

Example

On the 15th of November in 2007 a traffic pile-up occurred on the autobahn from Munich to the northward direction. After an initial crash an involved coach was at right-angles to the motor way. All lanes were obstructed; solely the breakdown lane was unobstructed. Other vehicles were approaching at high speed (Figure 1). The driver on the middle lane was trapped between cars at his sides and the bus obstructing the lanes in front of him. An independent and accident-free solution of the situation was not possible under these circumstances. Even worse: His panic reaction involved many other cars in the pile-up. He was the point of origin for a chain reaction. A joint solution, maybe available in the future, would have directed as many vehicles as possible over the breakdown lane, and rightly in a coordinated way. For the rest of the vehicles the solution would have been selected that would have promised the least overall damage (Figure 2). The outlined advanced driver assistance system is not possible on the basis of current functional and technical architectures. Below the necessary change from today's architecture to future architecture is described.

2.2 Today's architecture Today's architecture is characterised by unities of function, control unit and sensors/actuators (Figure 3). Installing more assistant functions is accordingly identical to integrating more unities of function, control unit and sensors/actuators. A coordination of the assistant functions is realised only rudimentarily because coordination is not supported by this kind of architecture und can only be realised at great efforts. One important disadvantage of the lack of coordination is the fact that the communication of every as-sistant function with the driver is more or less separated from the other assistant functions. Every assistant functions uses its own communication channels. The communication happens without consideration of the current system state or even the state of the driver.

2.3 Architecture and functional integration in the future There will be a substantial change in vehicle's architecture in the next years. The independence between function on the one side and control unit and sensor configuration on the other side is the essential difference between today's architecture and the architecture in the future (Figure 4). It is not valid any longer that a function is executable if its control unit and its sensors are present. In fact a function is always executable when enough system resources and the necessary environmental information are available at execution time. System resources and environmental information are abstracted from the function.

For system resources abstraction is done by open system architectures like AUTOSAR [START_REF] Dr | AUTOSAR Validation Experiences[END_REF] or concepts that go beyond AUTOSAR like service orientated communication. The number of electronic control units will decrease. The single control unit will provide enough system resources for more than one function. If a control unit or respectively the control unit network provides sufficient capacities functions can be added without the need for integration of further control units.

For environmental information abstraction is done by concepts of data fusion. These concepts are under way [START_REF] Prof | Verteiltes Umgebungsmodell für Fahrzeugsoftware (VerUM)[END_REF]. Data fusion abstracts the raw data of the sensors from the functions. But it is even more important that all environmental information is available system wide for all functions. If new functions do not need additional environmental information no additional sensors have to be integrated into the system.

The possibility of creating more information robustness and/or information quality by appropriate algorithms is another advantage of sensor fusion. The system becomes better in respect of system reliability and system performance. One disadvantage of sensor fusion: the higher demand for system resources. And it is not an easy task to overcome difficulties with system-wide information propagation (update rates and latency). In summary functions can possibly be upgraded without upgrade of hardware in terms of electronic control units or sensors. Thereby the costs calculation is changed. Functions themselves obtain a value that is independent of the hardware costs. In addition to economies-of-scale effects new savings potential is created by the significantly improved ratio functions to hardware components. Architecture in the future -new possibilities

The abstraction of functions from hardware, the thereby resulting simplified functional integration and the system-wide provision of comprehensive information provide new possibilities. They are the prerequisite for the solution of pestering problems that arise from the integration of more and more assistance functions into the car. The automobile makes up for a trend that has been initiated in aviation many years earlier. Instead of four crew members some decades ago an airplane can be flown by two pilots and automatic systems. The accident rate in civil aviation is as low as never before. But new problems have arisen by the operation of automatic systems: Underload of pilots in standard situations and loss of skills, thereby resulting overload in non-standard situations without automatic systems by the previous loss of skills. Furthermore loss of situation awareness and loss of system comprehension by information overload. Aviation has already made the experience that an increasing automation level can make systems less safe instead more safe. Problems like "pilot-out-ofthe-loop", "mode confusion" or even "loss of situation awareness" are well known in aviation. Car drivers will possibly meet the same problems. Today's situation is affected by increasing demands to the driver. The driver faces an increasing system complexity by a multiplicity of driver assistance functions. Reams of assistance functions whose single or combined functionality can not be understood by the driver route much information over various information channels to the driver. Mostly this is done uncoordinated and takes care for neither the driving situation nor the system or driver state. Additionally there is an increasing situation complexity by more and more vehicles on the road. The driver can become overstrained. And overstrain on the road always means danger of accidents. Solution to the problem is the reduction of the information overload by coordinating the information flow to the driver in dependence on situation and driver state. Information is processed actively and combined to more significant information. Results are presented at optimal point of time. Objective is the specific support of the driver in terms of an "artificial co-driver" [START_REF] Neuendorf | Pilot-in-the-Loop -Auf dem Weg zum ,artificial co-pilot' im Automobil[END_REF]. It is not intended to create an additional driver assistance function and to increase the system complexity. It is intended to transfer a concept from aviation to automotive industry to overcome the problems mentioned above.

The communication manager of the future is the central and exclusive interface between driver assistance functions in the car and the driver. Using a single, central interface allows the creation of optimal communication: concepts for operation and information can be realised without exceptions or deviation.

The "artificial co-driver" has full access to all information: It knows the system state, the driver state and out of data fusion the environmental state. All its actions are based on the knowledge of the situation and the ability to interpret the situation. A workload management as part of the communication manager determines the level of workload of the driver and the environmental condition. For example driving over a highway at good weather conditions is easier than driving in the mountains with rain or snow in the night. Depending on workload level and situation the workload management optimises the information flow to the driver. In critical situations only important, especially safety relevant information is presented to the driver. Less important information is postponed, unimportant information is omitted. The communication manager is based on the concept of "intelligent automation" with approaches like human-based automation, cooperative automation and cognitive automation. These approaches have been implemented successfully [4] in first aviation projects. The automations have abilities that correspond to the human abilities of information processing and problem solving. Thus the driver can understand the decisions of the system. A communication and workload manager based on cognitive automation as a driver assistant system on top of the car ensures optimal "situation awareness" by situation and driver dependent information processing and presentation. The ability to find solutions in contradictory situations is an important advantage of the cognitive automation. Ideally a communication manager is doing a human being would do if it had enough time to think about the situation, the objectives and the different possible solutions.

Extending the communication manager beyond information presentation to autonomous action is the solution for the example of traffic pile-up mentioned above. The objectives are known (minimal damage), the situation data comes out of the data fusion and the system knows the abilities of the car and thus the options for action. But one element is missing for a satisfying solution.

The vehicles have to aggregate their selfish objectives to an overall objective. And they have to harmonise their options for action. The result is a driver assistance system that goes beyond a single car.

For this purpose cars have to be equipped with appropriate communication means. Architecture in the future -Car2X-communication Likely communication networks of vehicles will be so called mobile ad-hoc networks. These networks are dynamic in several respects:

The number of vehicles in a communication cluster is varying, the set of vehicles is varying and the positions of the vehicles are varying. An efficient routing of messages is necessary in such dynamic, mobile ad-hoc networks. Simple broadcast algorithms would produce to high communication costs (costs in terms of bandwidth, latency and hardware requirements). Therefore messages have to be routed through the network. Like the network the routing itself has to be dynamic and optimised continuously. Appropriate mechanisms are under investigation and development at the moment [START_REF] Volbert | A Simulation Environment for Ad Hoc Networks Using Sector Subdivision[END_REF] (Figure 5). Additionally further technological aspect have to be taken into account. A suitable transmission standard has to be used, e.g. IEEE 802.11p for the automotive sector. Furthermore the data exchange has to be secure: encryption, authorisation, authentication and redundancy are important topics. Aviation is strong with these topics. But in aviation changes are imminent too.

Aviation

Progress in aviation

The success of military operations is more and more depending on the joint action of all combatants. Here communication plays a decisive role too. On this basis military operations and the example of avoiding a traffic pile-up are comparable. Accordingly there must be similar solution elements. This chapter is focused on possible future communication structures in military aviation.

There are programs that deal with improvement of the communication infrastructure for military operations. Such a program is ETAP. ETAP (European Technology Acquisition Program) is designed to develop the technology required to build a future combat air system (FCAS). Within ETAP, there are several Technology Demonstration Programs (TDPs), which will each demonstrate a product from a certain discipline. "Communication/Data Link" is one of those programs. By the way, not only military aviation is pursuing of improvement. According to Eurocontrol [START_REF]Eurocontrol: Civil-Military CNS/ATM Interoperability Roadmap[END_REF] the capacity of the existing Air Traffic Control (ATC) / Air Traffic Management (ATM) communications infrastructure is already tending towards saturation. It is expected that the existing systems in Europe will be overloaded within the next 15 years. Current ATC and ATM systems and operational procedures are seen as the bottlenecks in air transportation in the near future. These systems and services are closely linked to the functional components of Communication, Navigation and Surveillance (CNS).

For both military and civil aviation it is true that communications plays the primary role for data and information exchange among the air traffic participants. It is a prerequisite for an efficient and safe mission performance Civil aviation is also mentioned because there is only a single airspace for both military and civil aircrafts. Military communication structures have to be interconnected with the civil ones and vice versa (Figure 6). The networks are coupled technical and functional. That's an expansion of the architecture.

infrastructures in military aviation

There are no real backbones but satellites and command and control stations can be included as a relay or as a terrestrial network. Architecture principles, network management and security principles The specific tasks define the basic architecture principles. They are as follows:

• The communication nodes are not identical. They can not provide the full bandwidth of com-munication systems. Therefore communication resources have to be partitioned, taking into account the specific tasks of a communication node. • It is impossible to manage a network completely ad-hoc. But the more mobile the network nodes are, the more ad-hoc a network should be. • The network management is a central part of a network. But for security and performance reasons it should be a distributed system. These principles are valid for both the automotive and the avionic world. The civil avionic world knows many technologies for a network management according to the aforesaid principles. But the technologies have to be adapted to the military needs and completed with purely military technologies. An operational network management has to ensure elementary network qualities:

• Security: Ensuring that the network is protected from unauthorized users. • Performance: Eliminating bottlenecks in the network. • Reliability: Making sure the network is available to users and responding to hardware and software malfunctions. A network management is a complex system. The functions it performs include controlling, planning, allocating, deploying, coordinating, and monitoring the resources of a network, network planning, frequency allocation, predetermined traffic routing to support load balancing, cryptographic key distribution. authorization, configuration management, fault management, security management, performance management, bandwidth management, and accounting management. Of course security management and cryptographic key distribution is essential for military applications. But future autonomous cars will need the same security level in order to prevent obstruction or misuse of functions based on ad-hoc networks. Security Principles NATO currently only uses symmetric key ciphering for military communication. Symmetric keys have to be provided in a logistic process. For NATO the keys are managed centrally. They are distributed by couriers and supplied to the aircrafts be special devices. On the one hand the key chain is very long, many persons have to handle the keys and automation of the key distribution can hardly be established. On the other hand in operation the keys are valid for only one day. Central -and secure -provision of symmetric keys is therefore a very high effort. For future communica-tion structures with much more network participants than today these procedures will not be applicable. Future communication infrastructure in military aviation will base on asymmetric keys to avoid the disadvantages of symmetric keys. Fortunately civil data communication has a lot of experiences with asymmetric encryption keys military aviation can benefit from.

Conclusion

Functional development and integration are highly depending on the capabilities of the underlying architecture. We now face a change in architectures in both the military and the automotive worlds. The differences between them will become smaller and strong similarities -especially for communication structures -arise. Future communication structures for cars as well as for (military) aircrafts will use ad-hoc networking based on clusters. Therefore it is likely they will both use similar communication architectures and security principles. The new communication structures are the top of new functional and technical architectures. On the one hand they become more and more determinative for the functional architecture. They are the prerequisites for new functions that leave behind the tight borders of a single car or aircraft.

Figure 1 :Figure 2 :

 12 Figure 1: Situation that led to a traffic pile-up

Figure 3 :

 3 Figure 3: Today's architecture with unities of function, control unit and sensors As a first approximation every driver assistance function is realised with a specific sensor configuration (and possibly actuator configuration) and a dedicated electronic control unit well adapted for the needs of the function. A function is executable well if all these components are present and they are working free from defects. Part of the freedom from defects is: All physical environmental conditions have to be within the ranges of the sensors. E.g. an assistance function based on a camera fails in dense fog. The costs directly result from the combination of the aforementioned components. Thereby the sensors are often the most expensive components and so price-setting. Lower priced variants for lower market segments are created by installing lower priced sensors with inferior sensor range and/or value quality. As a result of the inferior sensor range or value quality the functionality itself is limited. Further savings potential is only possible by economies-of-scale effects.Installing more assistant functions is accordingly identical to integrating more unities of function, control unit and sensors/actuators. A coordination of the assistant functions is realised only rudimentarily because coordination is not supported by this kind of architecture und can only be realised at great efforts. One important disadvantage of the lack of coordination is the fact that the communication of every as-

Figure 4 :

 4 Figure 4: Architecture in the future with data fusion, environmental abstraction and communication manager

Figure 5 :

 5 Figure 5: Simulation of a dynamic, mobile ad-hoc network at the University of Paderborn, Germany

Figure 7 :

 7 Figure 7: Ad-hoc network clusters as basis for future communication infrastructures in military aviation


C Hote

M Lalo

P Munier

D Pilaud

Industrial applicability of advanced model/code-based V&V techniques for verifying program properties in embedded applications

Keywords: model checking, abstract interpretation, test, verification and validation 1

Industrial applicability of advanced model/code-based V&V techniques for verifying program properties in embedded applications

C Hote, M Lalo, P Munier, D Pilaud

Introduction

The last three decades have been very beneficial to the embedded software engineering standpoint and many software tools today help engineers to build larger and more complex software applications. Out of many examples, design tools introduce graphical formalisms (block diagram, state chart) from which early simulations, rapid-prototyping, and early specification error detection can be achieved without writing a single line of source code. In the same vein, auto-code generation was first introduced in the late 80' for supporting the design of embedded avionic systems, nuclear systems, and railways controllers. Later on in the mid 90s, those techniques spread out towards automotive sectors and are now used in many industrial sectors including consumer electronics, and medical devices. In the same time, the verification and validation techniques did not improve at the same pace and as a result, companies developing embedded software struggle in the testing phases of the software development process or have to deal with annoying software quality issues including product recalls, delay in deliveries or mission losses. Based on recent advances in static verification of program properties, a new hope is unveiled. The first section of the paper defines and positions several proving and testing activities available in the embedded software domain. The second section gives examples of properties which can be proven at the model and/or at the code level. Finally, this paper presents future directions mixing these different approaches.

2

Definition and problematic

From error detection to property proving

There are many definitions to validation and verification activities although most of them lead to two fundamental objectives; 1 -Maximizing the number of errors found during the software development process 2 -Minimizing the number or errors released in final software applications.

For many decades, testing techniques have been focusing on the first objective based on the assumption that item #1 infers a good confidence level in item #2 provided enough time has been spent in testing, and provided item #2 is, in general, not a solvable problem.

As a result, many testing techniques improved for easing the detection of more bugs and very few focused on measuring the amount of remaining bugs in software applications. The first domain refers to bug detection techniques while the latter refers to property proving, generally, an NP-hard problem.

Out of many, once could mention some interesting properties embedded systems should comply with:

• Functional property or compliance with specifications: the software must compute some known outputs with some known inputs, within a defined sequence. In other words the software implementation should behave in compliance with its specifications. • Timing property or compliance with operational requirements: the software must provide with the right answers within a known time frame and using a finite amount of memory. • Absence of run-time errors in programs: the software must react deterministically, without any unpredictable behaviors, and be reliable to any execution and to any possible input values.

The following paragraphs discuss several techniques that may be used for achieving those objectives and depending when they apply. In theory, if one is able to run an exhaustive testing campaign and check for each test that the oracle is true, this would constitute a proof that the property is true. For real-time embedded application however, this is out of reach for almost any system. Testing is great to find errors, and to gain confidence that the property is true. Though, it's never a proof.

Static analysis

When the focus is on bringing counter examples, the goal is to only warn the user if a counter example can be found. This makes these static techniques shift from "being sound and complete" to partial, in order not to swamp the user with false positives. The drawback is that these techniques miss errors (false negative) and can not prove the absence of errors in case nothing is reported. But these techniques work pretty well on the early detection of errors.

The only way to bring a proof is to use mathematical approaches of software, hence require static techniques.

The next section will detail one view of different techniques.

Model and Code-based verification

Although the scope of this document is not to describe which formal techniques exist and what their application domain is, we can restrict this paper to two main techniques:

• Model-checking and their derivative (symbolic model checking, NP prover approach is suitable for solving problems at the level of model. • Abstract interpretation is working on a semantically strong language, most of the time a low level development language. This technique is suitable for understanding the data flow of a program. "Automatic test case generation" can also be a mean to look for counter examples. . This is a technique can be derivate from the first two, and will not be detailed in this paper These techniques are mature enough for being available in commercial tools such as Mathworks tools or Esterel technologies tools. This will be detailed in the upcoming section with examples on which types or properties they can handle. For model checking, we'll provide examples using Simulink® Design Verifier. For abstract interpretation, we'll provide examples using PolySpace™ Model Link SL.

3

Examples of properties and how they can be proven

Prove model coverage

The first demo shows the ability to prove 100% coverage on a finite state machine model. The oracle for this model is: 100% coverage can be reached. The demo is "sldvdemo_fuelsys_logic" using Matlab 07b. The demo has been stopped before reaching 100% of the objectives Figure 1.

After automatic test generation, this report show which coverage has been reached for each state, and each transition. The oracle was defined for 100% state-transition coverage, not for a decision, condition or MC/DC coverage 3.2 Temporal logic oracle This second demo shows the ability to prove a functional property (based on temporal logic) of a model. The oracle is the only way to have 6 outputs equal to 1 in a row is that the input is equal to 2. The demo is "sldvdemo_debounce_testobjblks" using Matlab 07b

The objective was to prove that if an output is equal to 1, than the previous output was greater than 1, as shown in the figure below Oracle showing a functional property based on temporal logic.

While-loop based algorithms

For abstract interpretation, C language is an appropriate language to show what it can prove at that level as it is close enough to a run-time to be dealing with timing issues, run-time errors and dead code.

This example shows how abstract semantic allows converging on a dataflow whose previous values are re-used for the next output. Using the rtwdemo_fuelsys_fixpt of MATLAB release 07b, abstract interpretation can show a portion of dead code which indicates that the state Fuelsys/Overspeed can not be reached. Knowing that this model is a closed-loop model, this means that the system is stable and can not run in over-speed. If the functional property is that the engine should never run in over-speed, this property can be proved using abstract interpretation. If this portion of dead code is not intended, this can be a highlight of a functional error.

This is an example of a functional property which can be proved at the code level. This is possible if the oracle is expressed in a binary way. For instance, the following oracle can be proven true or false by abstract interpretation: "the value of a given variable should always be within a range or never within this range (here dead code)".

Run-time errors

Another example of errors which is half a functional property, half a run-time property, can be a run-time property whose cause will most probably be non-compliance to a functional property. We will not discuss here whether the cause of the error is a typo of the table whose index should start with 1 (and therefore get rid of the array[index -1] in the generated code), of if the index should not be between 0 and 4, resulting in a violation of a functional property for instance. If the table represents arbitrary calibrations, this type or errors might be detected at a very late stage of the overall development process, if not after the generated code goes into production.

Proving code Correctness

Another property which can be proven with abstract semantic is the robustness and reliability optimizations done in the code. For instance, the question about overflows can be answered comparing ranges of the destination type with the actual computed ranges.

Thanks to its sound approach, abstract semantic also allow to prove the code correctness on the same topic • Software development process: in this context, the final goal is to reduce the testing efforts required to have confidence in the final code and keep (if not increase) the level of confidence of the final delivered code • For Quality assessment, the goal is to perform final audit of source code and measure the final code correctness to reduce the risk of leaving errors in the source code. • With Code certification, the goal is to prove to certification authorities that everything has been done to reduce the risk of leaving errors in the field. • When proving can not reach a 100%, the techniques can be used to generate defensive behavior within the final embedded code, similar to what exception handling does in some languages, but focused on very few non-proven properties.

Development

Adopt a development process which is component based only

Some development processes are component based and define their Verification and Validation activities at the component level only, without having some robustness test at the system level. This is only possible under certain conditions.

• First, the development process must define all the component dependencies and their impacts toward the entire application. If one component is modified and its outputs vary within another range than previously, the process must clearly identify which other components should be re-verified. • On top of this impact analysis, the process must define for each component all its interfaces: with inputs and outputs and toward unknown parameters at the development stage such as calibrations. For each parameter, some data ranges must be specified: they can be either restricted to functional values only or/and may also contain worst case ranges.

For this kind of process, the idea is to reduce the amount of work in integration testing, as the total size of the code represents several hundred thousand lines of code, with more thousands points of calibrations, which might change the behavior of the whole application, even after delivery. For the purpose of code correctness and software reliability, testing is out of reach to prove anything.

So abstract interpretation can solve that by successfully verify -for each component -that the outputs match the specification, providing no run-time error happens and therefore preserve data integrity. This process can be automated by using data-ranges coming from specification documents, such as databases associating ranges for each software component, including calibrations.

Reduce iteration in Software development cycle

When the software development process is not particularly component oriented, errors can be equally spread over the whole development cycle. A run-time error for instance, such as an overflow, may be local to a function which performs computation on its local data, or may happen globally because of the effects of another software component. This requires abstract interpretation to work both at the component level and at the application level. The type of review, however, will be different for each step. In both cases, doing code verification functional test allows to find defect at early stages of each project, and therefore reduce testing activities in the field, or on test benches.

Other techniques may highlight where errors lie, but cannot guarantee that other operations are safe. That usually forces the user to proceed with redundant tests. Abstract Interpretation flags all operations that will never experience run-time errors-no matter the operating conditions. This contributes to reducing testing efforts and thus reduces the number of iterations in a development cycle.

Quality Assurance

Quality assessment for OEM

Within the relationships of suppliers and integrators, source code has always been an area of doubt. Traditional quality metrics, derived from ISO 9126 are in place for almost two decades, but can only rate the quality of the process more than the reliability of the final product. They work on the assumption that doing things right will produce the right software. Abstract interpretation, on the other hand, does not measure the quality of the development process, but only focuses on proving the code correctness of the final product. This is crucial for OEM which owns the responsibility of the final software reliability. Assessing a source code at his final stage of production be done by sampling files, classes, packages from the entire application or by verifying the whole source code. It provides a direct measure of the source code, and indicates areas where errors can happen, no matter how these lines were produced. This is ideal in situations where the results count more than the process to produce them.

Collaboration between OEM and supplier: Process improvement

On the margin of quality assessment, having a supplier using this technology in his tool chain is a great value for an OEM. Knowing how and when PolySpace products for C/C++ were used during coding gives great confidence in code reliability. It provides a guarantee that software robustness and reliability are ensured in the most efficient way possible. This is particularly appealing for suppliers companies, which see in abstract interpretation a mean to measure and improve source code reliability and not only a final code assessment tool.

Certification

Certification is about providing evidence that the development process has been done according to what has been defined. In that context, proving that a code verification tool can not miss one error is essential for certification authorities. Abstract interpretation is one of them by its exhaustive and sound approach. Every data approximation is done in a conservative way, in order to ensure that no value was missed. This way, it's possible to show certification authorities reports from the software validation efforts • Showing all flagged sections of the code which cannot return a software fault • Demonstrating for the operations that can return a software fault that they have been reviewed. For the first task, the certification authority can audit the tool vendor creating the code verification tool. Evidences should be provided that the underlying technology and his development process allow creating a code verification tool which can not miss errors. The second task can be achieved by providing evidence of code review operated on the non-proven points.

Generating defensive code based on non-proven properties

When it is impossible to demonstrate all the properties by these techniques: For example, code verification cannot prove 100% of run time errors if the C program is not driven by coding rules. It is therefore necessary to learn how to use the test and formal approaches together.

One idea would be to generate code or to create a model accordingly to the non proven properties. This would of course impact the associated development cycle. From a classic Design-Generate code-verify, some new steps could be introduced

• Design at the model level • Generate code

• Formal verification at both model and code level.

• (new) From the non-proven properties, produce both a model and the associated code • (new) Test of the of these properties, and decision to incorporate (or not) defensive code in the embedded system

Let's consider two examples:

• A model can be enhanced with non-proven properties. This can include the error-case behavior of the property. The model will thus be designed to behave properly in case the error happens. This will require a change in the development process: once the design is complete, the user will need to check which properties can be proven. On the remaining, he will have to choose whether the implementation in the design of this defensive behavior is appropriate or not. Code generation will follow, and produce the right defensive code.

• The code can be enhanced with non-proven properties. For run-time errors, it is possible to include defensive code for non-proven checks. The principle is similar to exception handling, but focused on specific run-time checks in the code: the benefit is to have limited overhead in the execution time and the size of the code. This enables the user to embed the code in the final real-time system.

Conclusion

In order to generate model and code for these non-proven properties, it's required to maximize the number of proven properties.

In the first part of this paper, we have seen which area checking can be successfully applied to: proving temporal and Boolean properties, proving model coverage, and finding counter example to functional properties.

In the second part of this document, we have seen which areas abstract interpretation can be successfully used: proving the absence of runtime errors, solving while-loop algorithms, and dealing with data related errors.

Combining these techniques together would help covering all areas and all type or errors which can be introduced in a development cycle. With proof ratios over 90% for both techniques can be reached separately, it can be anticipated that combined techniques will over a much higher proof ratio.

In a third part, we have discussed the possibility to combine these techniques with testing, thus enabling to embed C code containing focused defensive programming on non-proven properties. This can be an alternative to having 100% proof ratios. The next question is now how fast industrial will modify their development process to adopt these techniques.

  Figure 2.Oracle showing a functional property based on temporal logic.3.3 While-loop based algorithmsFor abstract interpretation, C language is an appropriate language to show what it can prove at that level as it is close enough to a run-time to be dealing with timing issues, run-time errors and dead code.

Figure 3 .

 3 Figure 3. The figure above shows how data ranges can be propagated throughout a code called within a while loop and invoking 2 steps memorization of variables.

Figure 4 .

 4 Figure 4. This is the same figure at the generated code levelIt must be noticed here that working at the generated code level enable tools to link back to the model, which consists in terms of process in a functionality overlap. These findings can be done both at the model and the code level, providing the model has a strong syntax and semantic.3.4 Dead codeHere is an example on the same demo than Simulink® Design Verifier. We'll see that the types of errors it finds are different, as they are more related to the dataflow than the temporal logic.Instead of having the default full range entries which are not functionally realistic, the code verification was performed on bounded entries. Because of the fixed point implementation of the model, the real C bounded entries are different. They map the implementation ranges in the generated C code. Throttle 0 120 Enginespeed 0 1000 EGO 0 1536 MAP 0 256

Figure 5 .

 5 Figure 5.

Figure 6 .

 6 Figure 6.This figure proves that no overflow will ever happen at this line By looking closer at this line, abstract interpretation can give you more details about why this oracle is always true

Figure 8 .

 8 Figure 8. This figure shows dead code (in grey) of saturation because data ranges are small enough to fit into a 16 bit signed type without saturation.

  2.2 Dynamic testingDynamic testing consists in setting test objectives, in generating test cases, and then in verifying the results obtained from the execution of the tested software component match the test objectives.

	Besides very few examples (table truth, code coverage), dynamic testing cannot be exhaustive and cannot bring a
	definitive proof a test objective has been achieved. In that regard, dynamic testing is a bug detection technique
	more than a proving technique.
	If you want to prove that a property is true, you need to rely on mathematical techniques. If you want to prove that
	a property is false, you can bring a counter example. Nevertheless, if no counter example can be brought, it does
	not constitute any proof.

The saturation above is indicated as grey because the data ranges saved into the variable are much smaller than the destination type. A typical application can be code generation optimization.