Matteo Bordin
email: bordin@adacore.com

Franco Gasperoni
email: gasperoni@adacore.com

Towards Verifying Model Compilers

Keywords: Code generation, formal methods, model-driven development

In this paper we propose a methodological and technical approach to develop model compilers which provide formal proof of semantic preservation and complement model-level verification activities with formal analysis on the generated source code. Our paper also details which characteristic a programming language shall exhibit to be used as target of a model compiler. Finally, we evaluate the impact of using formal programming languages on the development and qualification of model compilers.

Introduction

Model-driven development is a major innovation vector for the construction of high-integrity embedded systems. The paradigm has been successfully applied to several large projects in the last decade, showing the advantages of shifting from source-centric to model-centric processes. Regardless of success stories, model-based approaches have failed to completely replace source code in the application life cycle. Why?

The first observation is that some model transformation chains have failed to provide clear added-value for the modeling process. These model translators treat the model just as a blueprint of the source code providing no meaningful abstraction gain. For example, several UML2 tools implement a one-to-one mapping between model and source code elements: modeling is thus just "graphical coding". In this case, there is no advantage in choosing a programming language exhibiting particular properties: the generated code is used simply as an intermediate representation between model and object code and no additional verification activities are performed on it.

The second observation concerns the preservation of model-level properties at source-level. This has been done by providing empirical evidence that the code generator has been developed with care and has undergone adequate testing. By contrast, formally proving that properties are preserved from model to source increases confidence in the model translator and in verification activities performed directly on the model.

The third observation is that going from model to object-code is done in two explicit steps: first the source is generated and then it is compiled to object code. In other terms, source code is an explicit artifact of the development process. This requires explicit configuration management of source code, even if it could be desirable to treat it like any other intermediate representation generated during the compilation process.

In this paper we propose a methodological and technical approach to circumvent some of the limitations described above. In particular, we focus on end-to-end property preservation and cohesion of the whole model compilation chain. While we fully acknowledge the importance of promoting modelbased development as a mean for abstraction, we intend to address this specific topic on a separate work.

The approach described in this paper focuses on finding a formal and executable intermediate representation for a model. Such intermediate representation is used [START_REF] Omg | UML2 Metamodel Superstructure[END_REF] to demonstrate that model properties are preserved; [START_REF] Bordin | Beyond ASSERT: Increasing the Effectiveness of Modeldriven Engineering[END_REF] to complement verification activities for the target platform; and [START_REF] Omg | SysML specification[END_REF] to compile the model to object code. Within this paper, we intend to explain why this approach would be of benefit in the development of model compilers in the high-integrity domain, with particular attention for application certification and tool qualification in the context of the DO-178 standard [START_REF] Eurocae | Software Considerations in Airborne Systems and Equipment Certification[END_REF].

Overview of Modelling Languages

In this section we provide a brief overview of some important modeling languages for high-integrity embedded systems and evaluate whether their compilation chains suffer from the limitations described in the introduction.

UML2, SysML and MARTE

UML2 [START_REF] Omg | UML2 Metamodel Superstructure[END_REF] is a general purpose graphical modeling language for object-oriented systems. The language is particularly suited to describe structural properties of systemslike components structure, services and interactions, state machines and deployment. In particular UML2 provides a graphical representation of a program's architecture (i.e. the packages or namespaces, the types or classes, and the program operations). This graphical representation is a blueprint where relationships among types and classes have been made clear. This representation is more humanreadable than its textual counterpart ("a picture is worth a thousand words"). When used in this fashion UML2 is often complemented with textual representation for operation implementation (here a short text is worth a thousand pictures). The one pragmatic drawback when switching between the graphical and textual paradigm is at the environment level: UML2 tools are usually better at handling diagrams than editing text.

To increase the expressiveness of UML2 diagrams, it is possible to use an abstract action language: a high-level and platform-independent textual language to describe algorithmic behavior. The OMG is currently standardizing such a language. UML2 also relies on OCL (Object Constraint Language) to express constraints such as methods pre/post conditions, type invariants, and assertions.

UML2 has a well defined platform-independent semantics. The UML2 standard defines the intended static and dynamic semantics and deliberately gives no indication on how such semantics should be implemented. Presently, the limitation of UML2 is its uncontrolled and complex multiple-view modeling space. A system may be modeled in UML2 from different overlapping viewpoints or, in more common terms, diagrams. Unfortunately, the standard does not provide clear indications on how to guarantee consistency among views. To guarantee view consistency, one limits the views used to nonoverlapping ones. See [START_REF] Bordin | Beyond ASSERT: Increasing the Effectiveness of Modeldriven Engineering[END_REF] for a discussion on the UML2 diagrams needed to model a complete system while avoiding view overlap.

Code generation strategies for UML2 usually treat the model as a blueprint of the code: model elements are mapped to source via a one-to-one mapping. From this perspective, the target programming language is not particularly important since no methodological added value comes from targeting a specific language. Property preservation at source-level is difficult to demonstrate as some of these languages are hard to analyze formally and because most programming languages have no direct way to map OCL constraints, making it difficult to prove that dynamic and static model-level constraints are respected in the translated sources.

SysML [START_REF] Omg | SysML specification[END_REF] is a UML2-derived language used to describe industrial systems with particular emphasis on system-level components interaction and hybrid systems modeling. MARTE [START_REF] Omg | UML profile for MARTE[END_REF] describes the concurrent execution in both platform-independent and platform-specific terms. The platform-specific semantic elements of MARTE can be used for schedulability and other types of concurrent system analysis. This subset of MARTE integrates AADL [START_REF]AADL[END_REF] via the UML profiling mechanism.

Simulink and Stateflow

Simulink and Stateflow [6] are used to model control systems via block diagrams (for data flow) and hierarchical state machines (for state-based behaviour) with an emphasis on mathematical equations. Differently from UML2-based tools, Simulink and Stateflow raise abstraction to the level of control theory and thier model translators employ a more complex code generation strategy translating a set of equations into a list of sequential operations with causal and temporal dependencies. Simulink and Stateflow model translators, however, do not provide evidence of property preservation and elide differences in mathematical semantics between model-space and target hardware.

Introducing Verifying Model Compilers

To improve the state-of-the-art a verifying model compiler would: [START_REF] Omg | UML2 Metamodel Superstructure[END_REF] provide formal evidence that model properties are preserved in the model-tosource translation; (2) perform target-dependent verification activities which cannot be easily done at model level; and (3) wrap the whole translation chain in a single logical tool.

Property Preservation

Modeling languages are particularly well suited for the formalization and verification of structural properties (safety properties of state machines, determinism of concurrent models, ...). A limitation of today's model translation technologies is the lack of formal evidence when it comes to property preservation in the refinement process from model to sources. The core reason for such limitation lies with target programming languages which are executable but not formally analyzable. In practice, the target programming language cannot formalize the properties expressed at model-level: such properties are "lost in translation".

The approach chosen for verifying model compilers is to target formal programming languages which are both executable and analyzable. Such programming languages should be able to represent the properties formalized at model level and permit their proof at source-level.

Some of the properties we are interested in are:

Information and data flow contracts: how components share data and information.

State machine properties such as safety, completeness, and determinism. Design-by-contract in the form of pre/postconditions, invariants, and assertions.

Determinism and analyzability of concurrent execution.

In section 4 we will analyze several target languages (SPARK/Ada, ACSL/C, JML/Java, Spec#/C#) and evaluate them in terms of property preservation, soundness of proving technology, efficiency, and interfacing abilities with other languages. This last point is significant as some components of the final application may be handcrafted possibly because of reuse or outsourcing.

Complementing Verification Activities

Verifying model compilers complement model-level verification with formal proofs at source-level. In fact, several crucial characteristics of a complete system can be proved only at source-level. For example, consider platform-specific properties such as absence of overflow, array-out-of-bound, or stack overflow errors: proving such properties requires knowledge of the implementation semantics and may not be provable at model-leveleven in the presence of fully expressive abstract action languages. This need for source-level analysis to verify target-specific properties requires targeting a programming language for which sound proof techniques exist.

Errors detected at source-level should be either fed back into the model (e.g. an overflow may imply that a computation in the model diverges) or are due to errors in the model compiler implementation. Absence of run-time errors in the generated sources reinforces confidence in the model compiler. In both cases the modeler need not understand the intermediate language representation used for formal verification. In section 4 we evaluate possible target programming languages from this perspective.

A Single Logical Tool

From a technical perspective, current model translation techniques separate source code generation from traditional source-to-object compilation. This strategy forces the modeler to regard source code as an explicit product of the development process and thus subject to configuration management, verification and traceability. To remove these source-centric activities, model-to-object translation should be wrapped in a single logical tool. A verifying model compiler would hide intermediate source code generation and proofs from the modeler in the same way a conventional compiler hides semantic analysis and intermediate code generation from programmers. Furthermore, by wrapping the whole model compilation chain in a single logical tool, it is easier to cross-compile a model, execute it, and debug it on the target hardware (or simulator). This approach is orthogonal to model execution/debug via interpretation on an abstract (UML) virtual machine.

As a final note, a verifying model compiler should generate appropriate hooks where foreign code may be interfaced to incorporate existing or subcontracted components.

Evaluation of Possible Target Languages

As stated in the previous section, the intermediate representation generated by a model compiler shall:

1. Be unambiguous.

Guarantee that the model semantics is

preserved in the transformation to ensure that verification activities performed at the model level apply also to the final executable program.

3. Permit additional target-dependent static verification activities to be performed, such as: checking for absence of run-time errors, verifying conformance to design contracts (pre/post conditions, invariants, etc.), analyzing stack size requirements, and computing worstcase execution time.

Point 1 says that the static and run-time semantics of the target language shall be well defined. Point 2 says that the chosen target programming language must be rich enough to represent most (if not all) semantic constructs of the input model, possibly including formally expressed properties. Point 3 says that verification tools for the chosen programming language must exist to complement the verification activities performed at the model level.

Contrary to the common practice, the developer of the model compiler, and not the end users, should choose the target programming language of a model compiler. This choice has a great impact on the development of a sound model compiler and on the possibility of qualifying it with respect to appropriate industrial standards (ex. DO-178). We return to this specific point in section 5.

Considering the input modeling language of interest (the UML-centric family and Simulink/Statflow) and due to the requirements above, our candidate target programming languages are:

1. SPARK: SPARK [8] is a subset of Ada augmented with annotations to describe contracts for information/data flow and behavior (pre/post conditions, invariants). Contracts can be formally proved through automated tools.

2. C and the ANSI C Specification Language (ACSL): ACSL is an annotation conceptually similar to SPARK annotations. Contracts can be formally proved via automated tools, for example in Frama-C [START_REF][END_REF].

3. Java and the Java Modeling Language (JML). JML [START_REF] Jml | [END_REF] is an annotation language to specify the behavior of Java programs. It is used to improve both static and dynamic checks for Java programs. Contracts can be formally proved using the ESC/Java2 theorem prover [START_REF] Jml | [END_REF].

Spec# [11]

, an extension to the C# programming language to describe and formally prove behavioral contracts of C# programs.

The choice of the target programming language is strongly connected to the availability of a conventional compiler presenting the appropriate characteristics. In particular, the compiler shall:

Target the chosen hardware target.

Produce efficient object code.

Require minimal run-time libraries. The time or space overhead induced by the run-time support may cause a discrepancy between the results of analysis performed at the modeling or programming language level and empirical evidence. For example, consider a compiler targeting a virtual machine that includes a thread to perform garbage collection: this thread is present neither in the model nor in the intermediate source-level representation, complicating the timing analysis.

Guarantee some form of traceability between source code and object code: this requirement derives from international standards for highintegrity embedded systems development such as DO-178B for commercial avionics.

We cannot thus evaluate programming languages and their compilers separately, but we shall instead treat them a whole.

The fitness of a programming language as target of a model compiler is evaluated based on three criteria: (i) the programming language coverage of the semantic needs for modeling language described above, (ii) the kinds of static verification supported at source code level and (iii) the availability of compilers for the domain of interest. SPARK supports the description and proof of data/information flow and behavioral contracts. Concurrency is supported with first-class language features and annotations to prove absence of deadlocks, race conditions and priority ceiling violations. It has a focus on proving absence of runtime errors such as numeric overflow or out-of-bound array indexes. It has a limited support for objectoriented semantics: polymorphism is outside the language semantics. The SPARK theorem prover is sound. SPARK is compiled to object code using standard Ada compilers: conventional compilers with the properties described above are available and all Ada compilers generate equivalent object code starting from the same SPARK program. Since SPARK is based on Ada, its interfacing with other languages is pretty straightforward.

C and ACSL present characteristics similar to SPARK, with the main difference being the lack of support for concurrency. The typing system for C is much less expressive than the SPARK one: the C and ACSL representation of a given semantics can be much more verbose than the corresponding SPARK one. For example, SPARK can directly express type properties such as the minimal and maximal value for an integer; while ACSL requires annotations (logic formulae) for each single variable or formal parameter. This difference is caused by the different roots of the two languages: SPARK derives from Ada, which has an expressive typing system; ACSL is based on C which is extremely poor (and platform-dependent) when describing types. Sound theorem provers for ACSL exist, such as Frama-C [START_REF][END_REF]. C and ACSL are compiled to object code using C compilers: conventional compilers with the properties described above exist. Interfacing C with other languages is straightforward.

Java and JML support formal specification and proof of properties on object-oriented programs using polymorphism. ESC/Java2 is, by its own design, an unsound theorem prover. The language does not provide advanced support for numeric types and their analysis. The language can rely on the concurrency features described by the Real-Time Java and Safety Critical Java initiatives, which are conceptually similar to those present in SPARK; however, no specific JML annotations exist for such concurrency features. A Java implementation may include a virtual machine to execute, increasing the semantic distance between the input for analysis and the actual executable. Spec# supports formal specification and proof of properties for object-oriented programs using polymorphism. The language does not provide advanced support to describe and analyze numeric types, and it lacks concurrency features appropriate for the domain of interest. At the moment of writing, Spec# requires a compiler targeting a .NET implementation, making it unsuitable for highintegrity embedded systems. The result of our analysis does not identify a clear winner, even if SPARK and C/ACSL are probably the most suitable solutions for the domain of interest.

Language Evaluation

SPARK

The main limit of these languages is the lack of support for object-oriented features.

Examples of a SPARK Verifying Model Compiler Usage

In this section we provide some simple examples on how the verifying model compiler philosophy can be of benefit in the development of high-integrity software. The first two examples target Stateflow and Simulink models, while the third and fourth focus on Executable UML models.

The first example is taken from the February 2010 issue of "Communication of the ACM" [START_REF] Miller | Software Model Checking Takes Off[END_REF]. In [START_REF] Miller | Software Model Checking Takes Off[END_REF] the authors use a separate formal specification language to model the behavior of a microwave oven and prove a set of properties on it via model checking. A typical property is: "if the oven is running, then the door is closed". The control algorithm of the microwave oven is modeled in Stateflow. The proof technology used in [START_REF] Miller | Software Model Checking Takes Off[END_REF] is NuSMV [13]. To demonstrate that the property was not satisfied by the input model and to produce a counter example, the NuSMV theorem prover produced and evaluated 9.8x10 6 states.

The second example is taken from a Simulink model to implement the control algorithm for a window manager to be used in heads-up and heads-down displays for next-generation commercial aircraft [START_REF] Whalen | ADGS-2100 Adaptive Display & Guidance System Window Manager Analysis[END_REF]. Among the properties proved on the Simulink model, the most interesting are related to the logic of selecting the most appropriate unit to display the information to the user. The properties were again proved at model level by using model checking techniques.

Our main goal was to evaluate if we could translate the model and properties of interest in SPARK so as to use a unique representation to feed to the proof engine and the traditional compiler. Following our verifying model compiler vision, we wanted to (i) decrease the semantic distance between the executable and its formal specification used to prove properties and (ii) increase the confidence that the source code representation implements the model semantics by proving that the properties proved at model level still hold at source level. It must be noted that the SPARK proving technology is based on abstract interpretation and deductive verification rather than model checking.

We translated both the Stateflow model of [START_REF] Miller | Software Model Checking Takes Off[END_REF] and the Simulink model of [START_REF] Whalen | ADGS-2100 Adaptive Display & Guidance System Window Manager Analysis[END_REF] in SPARK and added the properties of interest as post conditions of the subprogram implementing, respectively, the state machine logic and the control algorithm. For the Stateflow model, we were also able to fully model the state machine logic as a concatenation of logic expressions (again, as part of the post condition of the subprogram implementing the state machine logic). We used a prototype of the Simulink and Stateflow Ada back-end based on the Gene-Auto technology [START_REF]Gene-Auto[END_REF] and manually added SPARK annotations a posteriori on the generated code. The process of manually adding annotations was straightforward and we expect their automatic generation to be likewise. The SPARK code was translated into, respectively, 50 and 38 verification conditions. It is included in an extended version of this paper on the AdaCore web site [START_REF] Bordin | Verifying Model Compilers[END_REF]. We used a development version of the SPARK technology which can be coupled with the SMT solvers through the Victor translator [START_REF] Jackson | Using SMT Solvers to Verify High-Integrity Programs" 2 nd international Workshop on Automated Formal Methods[END_REF].

The SPARK technology was able to prove the same properties and detect the same violations detected by the technology used in the original papers. SPARK was also able to provide precise conditions under which the violated properties do not hold. Such conditions are equivalent to the counter example produced by the NuSMV model checker. In addition, we were also able to prove that the properties of interest hold when the input model is slightly changed, again as suggested in the original papers. SPARK was of course able to prove also the absence of run-time errors, a task at which model checkers are usually not particularly effective.

The last two examples we list focus on the proof of absence of run-time errors in the code generated from an Executable UML model. Such experiments were successfully carried out by AdaCore clients using model compilers targeting SPARK on commercial applications in the defense [START_REF] Wedin | Applying Model-driven Architecture and SPARK Ada -A SPARK Ada Model Compiler for xtUML[END_REF] and energy domains [START_REF] Curtis | SPARK annotations Within Executable UML" Reliable Software Technologies -Ada Europe[END_REF] using different Executable UML modeling environments (respectively Mentor Graphics BridgePoint and Kennedy Carter iUML). In the cited projects, the generation of SPARK from Executable UML models permitted a zero-cost formal verification of absence of run-time errors in the functionalities encoded using an abstract action language which manipulates Executable UML elements. In particular, no specific constraints were imposed on the modeling standard to accommodate the generation of SPARK code and all required annotations were automatically generated. We acknowledge that this approach defeats the use of SPARK as a design-by-contract tool: the contracts are inferred automatically from the implementation in Executable UML. However, the purpose for the use of SPARK in this context was the proof of absence of run-time errors, rather than partial correctness: from this point of view, the SPARK model compilers were extremely successful in complementing model-level verification activities with source level formal verification without requiring any modification to the users' modeling practice.

Developing Verifying Model Compilers

In the previous section we provided evidence that the verifying model compiler vision is feasible and has already been applied in industrial projects. We now focus on the evaluation of the impact of using formal programming languages as target for the model compilation chain in terms of: Development of the model compiler itself.

Qualification of the model compiler in a DO-178 context.

Certification in a DO-178 context of an application including generated code.

Our feedback derives from our involvement with the Gene-Auto consortium (ITEA 05018, [START_REF] Toom | Gene-Auto: an Automatic Code Generator for a safe subset of Simulink/Stateflow and Scicos[END_REF]) for the development of a SPARK back-end for a sound subset of Simulink and StateFlow.

Impact on Model Compiler Development

While being constrained by SPARK semantic and syntactic limitations increased the initial definition of the code generation strategy, the use of a formal programming language as target for a model compiler caused surprising benefits during the development of the latter. The generated code produced by the prototype SPARK back-end for Gene-Auto had to be compilable and pass a small formal verification test. This requirement led to the discovery of several inconsistencies within the whole model compilation chain, including the part shared with the back-end for the C programming language. The errors we found included uninitialized or useless variables, dead code and unnecessary statements (for example, an if statement statically evaluable to False or True). Such discoveries permitted to greatly improve the Gene-Auto model compiler, with benefits for both the SPARK and C back-ends. In this particular case the same errors could have been caught by less formal verification tools (for example CodePeer [27] and Coverity Static Analysis [START_REF]Coverity Static Analysis[END_REF]) which do not require the use of stringent semantics as for SPARK. However, the use of a formal language is still of benefit because it leaves the door open for more advanced formal analysis, in particular related to the absence of run-time errors and partial correctness (see the following sections). 5.2 Impact on DO-178 Tool Qualification DO-178 does not discuss directly if/how the qualification of a model compiler could alleviate the verification activities on the generated code. An accepted approach in industrial practice (see for example [32]) is however to formalize low-level requirements in a model and rely on a model compiler qualified as development tool to:

1. Perform some verification activities (for example testing and structural coverage) on the model, typically via simulation: verification at a higher abstraction level is expected to be less costly.

2. Skip some verification activities on the source code (for example compliance with low-level requirements) because the generated code is expected to be faithful to its model-level specification.

In order to rely on model simulation instead of testing of executable code for verification activities, it is also usually necessary to produce evidence that the generated code is compiled to object code preserving the same functional properties. The whole qualification process of a development tool is extremely costly: for Gene-Auto the estimated qualification cost is around eight person years. The high initial investment in qualifying a model compiler as a development tool has been so far a barrier to the commercial availability of qualified model compilers.

In this paper, we propose an alternative path which could be considered to alleviate the qualification costs of a model compiler. Our approach does not consider for the moment how to provide evidence of property preservation from the generated source code to the (cross-)compiled object code. It is however worth noting that it is usually simpler to provide such evidence for formal programming languages because they employ a much simpler semantics and thus do not exercise particularly advanced or obscure features of a language/compiler.

The strategy we propose here to alleviate the cost of qualifying a model compiler is conceptually similar to the "Unit Proof" methodology promoted by Airbus [START_REF] Souyris | Formal Verification of Avionics Software Products[END_REF], which permits to eliminate most verification activities on source code if (i) all low-level requirements are expressed as formal properties, (ii) the formal verification framework is qualified accordingly to DO-178 as a verification tool. In a DO-178 context, qualifying a verification tool (like a theorem prover) is much less costly than qualifying a development tool (like a model compiler). The same applies also to Tool Qualification Levels in DO-178C.

The strategy we propose requires to:

1. Express low-level requirements at model-level, potentially using formal specification of properties. Formal specification of properties is not always necessary: for example, the logic of a state machine by itself formalizes low-level requirements without requiring the explicit production of formal properties. This point requires a modeling language able to model formal properties: this is the case of both Simulink/Stateflow and Executable UML (via OCL).

2. Verify that all model-level properties are correctly translated to the formal programming language targeted by the model compiler. Additional properties may be produced in the source code, for example to represent the logic of a state machine as a post-condition (see also the source code available in the extended version of this paper [START_REF] Bordin | Verifying Model Compilers[END_REF]).

3.

Prove that all model level properties hold at source level. As show in section 4.1, we were able to formally express and prove model-level properties on SPARK programs.

4. Qualify the formal verification technology used at point 3 as a verification tool.

If the conditions above are all met, we can formally demonstrate that the generated source code complies with the low-level requirements formalized at model level, without qualifying the model compiler as a development tool. We thus believe that the verifying model compiler vision could permit to benefit of the advantages typical of a qualified model compiler (reduction of verification activities on source code) without actually requiring the qualification of the model compiler itself.

Impact on DO-178 Application Certification

The use of formal programming languages as a mean to decrease the cost of unit testing is increasing in the high-integrity domain: consider, in addition to SPARK, the use of tools like Caveat [20] and Astrée [START_REF]Astrée[END_REF]. By targeting a formal programming language, we guarantee that the generated source code can be safely integrated with other (legacy) high-integrity components written in the same formal language. For example, the generation of SPARK assures that the same level of safety can be maintained across different software components and that global, application-level analysis can be performed. If we targeted classical programming languages, we would have limited the formal verification to a component-by-component basis and required manual analysis for the integration of manually written SPARK and generated Ada code. The model compiler vision fully guarantees that the proven advantages of using formal programming languages in a DO-178 certification context can be applied even when the application code is partially generated from modeling languages.

Related work

The use of intermediate (pivot) languages for formal verification has been already proposed and implemented in TOPCASED with Fiacre [START_REF] Berthomieu | Fiacre: an Intermediate Language for Model Verification In the TOPCASED Environment[END_REF]. However, Fiacre is a verification-oriented pivot language: its use consists in being generated from modeling languages like AADL to verify some specific properties. Another interesting approach closer to the verifying model compiler vision is the one proposed by ClawZ [START_REF] Arthan | ClawZ: Control Laws in Z[END_REF]. It provides formal evidence of semantic preservation of the refinement process from Simulink models to SPARK source code. This evidence is provided by translating both the Simulink model and SPARK program into Z schemas and formally proving their equivalence. To achieve this result, it was necessary to define a formal Z representation for a subset of Simulink; a Z representation for SPARK is, on the other side, already available [START_REF] O'neill | The Formal Semantics of SPARK83[END_REF]. The main advantage of ClawZ is its verification tool nature, meaning that its DO-178 qualification would cost less than qualifying a code generator (which is a development tool). In addition it does not need to have any internal knowledge of the code generator, as it just copes with the initial input (the model) and the final output (the SPARK code). The approach proposed by ClawZ is conceptually similar to the one we propose, in the sense they both require formal programming languages to be the target of code generation: it is not a coincidence that SPARK is the target language of ClawZ. At this stage, the main advantage of the model compiler vision is the avoidance of using additional explicit formal representations (like Z) to prove property preservation. Recent advancements [START_REF] O'halloran | Guess and Verify -Back to the Future[END_REF] on this technology suggest that the Z representations can be hidden.

Formal evidence of property preservation can also be obtained by construction if the model compiler itself is formally developed/verified. This is the approach applied for the CompCert [START_REF] Leroy | Formal Verification of a realistic compiler[END_REF] compiler and for the block sequencer in Gene-Auto. Both technologies were developed using Coq [31]. The main limitation of this approach is that the complexity and cost of the formal development may drastically limit the scope of the technology. CompCert for example has only PowerPC and ARM back-ends, has limited optimization features and contains several functionalities (for example I/O and parsing) which are not formally specified/verified. The Gene-Auto block sequencer is specified with 4500 SLOC of Coq (including 130 theorems) [START_REF] Izerrouken | Machine-Checked Sequencer for Crititcal Embedded Code Generator[END_REF] and represents just a single step in the model compilation chain.

The last alternative solution is to consider just verification of absence of run-time errors on the generated code using tools like Polyspace or CodePeer. This approach clearly does not provide any evidence of property preservation. The same of course applies when trying to infer the faithfulness of the generated code to the model by simply comparing test results obtained via model simulation and execution of the generated code.

Conclusion

In this paper we have discussed the vision for verifying model compilers. Verifying model compilers promise improvements over the state-of-the-art in code generation by targeting a formal programming language which (i) can automatically provide evidence that property proved at model level still hold at source level and (ii) can complement modellevel verification activities with source-level formal verification of platform-specific properties. We supported our point-of-view with limited experiments for Simulink and Stateflow models and with industrial-scale applications for Executable UML models. All experiments used SPARK as a target language.

In this paper we also evaluated different programming languages with respect to the requirement of being used as targets of a verifying model compiler. The SPARK and Frama-C frameworks emerged as the most effective choices.

Finally, we discussed the impact of targeting formal programming languages from several points of view, in particular (i) development process of a model compiler, (ii) DO-178 tool qualification and (iii) DO-178 application certification. The deployment of verifying model compilers brings benefit for all aspects above.

From a conceptual standpoint, the most valuable outcome of our discussion is the positioning of traditional programming languages within a modelcentric development process. In contexts outside the high-integrity domain, source code may well be considered as a derived artifact with no interesting properties. On the contrary, if property preservation and platform-specific verification are significant concerns, the formal programming language plays a pivotal role within a model-based compilation chain, even though such intermediate representation may not be directly visible to the modeler. This requires finding a semantic mapping for the modeling language which lends itself to formal verification via automated theorem proving. Considering this aspect, it is important to note that the dominant needs when developing a (verifying) model compiler shall be those expressed by the developers of the model compiler rather than those of the final users. Given the cost of qualification/certification and that mature technologies exist to easily integrate modules written in different programming languages, there is no reason to target a less-than-ideal formal programming language.

Formal programming languages and proof technologies may of course need to be enhanced to extend the set of properties they can prove and to ensure that properties can be preserved from model to sources. If this technical development is accomplished, verifying model compilers will ease the adoption of the model-driven paradigm, increase the confidence in modeled application, and improve the overall development process.

Acknowledgements

This work was carried out within the context of the LAMBDA project, part of the System@tic cluster. The views presented in this paper are those of the authors' only and do not necessarily engage those of the other members of the LAMBDA consortium. The authors gratefully thank the Gene-Auto consortium.


M Steindl

J Mottok

H Meier
email: hans.meier@e-technik.fh-regensburg.de

F Schiller
email: schiller@itm.tum.de

M Fruechtl
email: fruechtl@itm.tum.de

Safeguarded Processing of Sensor Data

Keywords: Safely Embedded Software, FPGA, Diverse Instructions, Safety Code Weaving

The spectrum of software tasks no longer includes only rare function controlling tasks for sensor actuator chains in reactive embedded systems. However, more and more responsible challenges like safety-critical scenarios are tackled. Therefore sensor data have to be safeguarded by several mechanism. An obvious and widely used approach is the use of two redundant hardware controllers, but this comes along with an additional cost, space and energy factor. Another way to fulfill certain safety properties is to implement a second diverse software channel in a single microcontroller architecture according the Safely Embedded Software (SES) approach. However, a lack of performance occurs by implementing this diverse channel for complex computations e.g. floating-point operations. This paper gives an approach for transferring the SES into a coprocessor and to migrate SES to a flexible and powerful FPGA architecture.

Introduction

The increasing functionality in automotive systems is mostly realized by software. Those software is often part of a sensor-actor chain, e.g. the break-by-wire technology, and meets safety-relevant requirements in many cases. As a consequence of this several measures to ensure the right processing of sensor data have to be taken. A widely used method to achieve both fail safe and fail operational architectures is based on hardware redundancy. However, this comes along with an additional cost, space and energy factor. With the Safely Embedded Software (SES) approach diverse redundancy could be created by software [START_REF] Mottok | Safely Embedded Software for State Machines in Automotive Applications[END_REF]. This approach allows to detect both permanent and temporary errors and due to this a suitable reaction (e.g. retry, recover, fail safe state or fail operational) could be initiated. Also SES is independent of specific hardware and specific operating systems which makes it more portable.

On the other side arithmetic coding mechanisms are accompanied by larger data values and more complex operations in the transformation domain, so the diverse software channel is the main time-consuming factor in the system. This paper introduces a solution to this matter by transferring the SES part to dedicated hardware and continuous with a complete migration of the SES architecture to a FPGA, where microcontroller and SES-coprocessor are realized within a single FPGA. The FPGA architecture also offers benefits in sensor data conditioning. Modern sensors often need special algorithms for signal conditioning which need a lot of processing power if they must be realized in software. In a FPGA architecture such tasks could be easily realized in hardware and so the performance of the system could be improved.

The following section gives an overview of the SES approach, the performance is analyzed in section 3. Section 4 describes the FPGA archtecture.

Safely Embedded Software (SES)

This Section gives an overview of the Safely Embedded Software (SES) approach. Safety Code Weaving is the procedure of adding a second software channel to an existing software channel. In this way, SES adds a second channel of the transformed domain to the software channel of the original domain. In dedicated nodes of the control flow graph, comparator functionality is added. Though, the second channel comprises diverse data, diverse instructions, comparator and monitoring functionality. The comparator or voter, respectively, on the same ECU has to be safeguarded with voter diversity [START_REF] Ehrenberger | Software-Verifikation[END_REF] or other additional diverse checks. Due to the safety code weaving, it is possible to check the validity of data in a given granularity. Based on this results, a dedicated fault reaction is initiated to achieve a fail safe state. Some examples for possible fault reactions are backward recovery, forward recovery, reset, consecutive calculation, consecutive transmission (timing redundancy), retry, substitute value, degradation of service (limp home)

x c = A * x f + B x + D where x c , x f ∈ Z, A ∈ N + , B x , D ∈ N 0 , B x + D < A.
The prime number A [START_REF] Forin | Vital Coded Microprocessor Principles and Application for Various Transit Systems[END_REF][START_REF] Ozello | The Coded Microprocessor Certification[END_REF] determines important safety characteristics like Hamming Distance and residual error probability P = 1/A of the code. Number A has to be prime because in case of a sequence of i faulty operations with constant offset f , the final offset will be i * f . This offset is a multiple of a prime number A if and only if i or f is divisible by A. If A is not a prime number then several factors of i and f may cause multiples of A. The same holds for the multiplication of two faulty operands. Additionally, so called deterministic criteria like the above mentioned Hamming Distance and the Arithmetic Distance verify the choice of a prime number.

Other functional characteristics like necessary bit field size etc. the handling of overflow are also caused by the value of A. The simple transformation x c = A * x f is illustrated in Fig. 3. The static signature B x ensures the correct memory addresses of variables by using the memory address of the variable or any other variable specific number. The dynamic signature D ensures that the variable is used in the correct task cycle. The determination of the dynamic signature depends on the used scheduling scheme. It can be calculated by a clocked counter or it is offered directly by the task scheduler.

The instructions are coded in that way, that at the end of each cycle (i. e. before the output starts) either a comparator verifies the diverse channel results z c = A * z f + B z + D?, or the coded channel is checked directly by the verification condition (z c -B z -D) mod A = 0? (cf. Definition 1).

Coding of Operations

A complete set of arithmetic and logical operators in the transformed domain can be derived. The transformation in Definition 1 is used. Definition 2 (Coded Operators) A coded operator OP c is an operator in the transformed domain that corresponds to an operator OP in the original domain. Its application to uncoded values provides coded values as results that are equal to those received by transforming the result from the original domain after the application OP for the original values. The formalism is defined, such that the following statement is correct for all x f , y f from the original domain and all x c , y c from the transformed domain, where x c = σ(x f ) and y c = σ(y f ) is valid:

x f c s x c y f c s y c z f c s z c z f = x f OP y f c s z c = x c OP c y c (1)
Accordingly, the unary operators are noted as:

z f = OP y f c s z c = OP c y c (2)
In the following, the derivation steps for the integer addition and integer subtraction operation are explained exemplarily.

Coding of integer Addition

The addition is the simplest operation of the four basic arithmetic operations. Defining a coded operator (see Definition 2), the coded operation ⊕ is formalized as follows:

z f = x f + y f c s z c = x c ⊕ y c (3)
Starting with the addition in the original domain and applying the formula for the inverse transformation, the following equation can be obtained for z c using 1:

z f = x f + y f z c -B z -D A = x c -B x -D A + y c -B y -D A z c -B z -D = x c -B x -D + y c -B y -D z c = x c -B x -D + y c -B y + B z z c = x c + y c + (B z -B x -B y ) const.
-D (4)

The equations ( 3) and ( 4) state two different representations of z c . A comparison leads immediately to the definition of the coded addition ⊕: Definition 3 (Coded Addition ⊕)

z c = x c ⊕ y c = x c + y c + (B z -B x -B y ) -D 2.

Coding of integer Subtraction

In analogy to the addition in Section 2.2.1, the coded operation can be formalized as follows:

z f = x f -y f c s z c = x c y c (5)
Applying the formula for the inverse transformation, the following equation can be obtained for z c :

z f = x f -y f z c -B z -D A = x c -B x -D A - y c -B y -D A z c -B z -D = x c -B x -D -y c + B y + D z c = x c -y c + (B z + B y -B x ) const.
+D [START_REF] Mahr | Hardware-Software-Codesign Vieweg[END_REF] According to this equation, the coded subtraction can be defined as follows: Definition 4 (Coded Subtraction )

z c = x c y c = x c -y c + (B z -B x + B y ) + D
On basis of this procedure, other arithmetic operations like multiplication and division can be formalized.

Coded Floating-Point Operations

Additionally to the coded integer operations coded floating-point operations could be formulated. Finite floating-point numbers are internally represented by a dataset containing sign, exponent and the fraction. A single (32 Bit) floating-point number is encoded by a 1-bit sign s, an 8-bit exponent e and a 23-bit fraction f, as shown in Table 1.

For a proper transformation of floating-point numbers into the transformed domain the dataset is transformed separately. So each part of the dataset (sign,

Performance Analysis

In this Section, the performance of the coded addition is discussed. In addition to the coded integer addition, the coded floating-point addition is introduced. This floating-point addition in the transformed domain is based on coded integer addition with separating mantissa, exponent and sign. For a better comparison between the performance of floating-point additions in the original and the transformed domain, the calculations in the original domain are completely emulated in software and no internal compiler library is used. The calculations in the transformed domain are completely handled in software following the SES approach.

All measurements are done on an Infineon XC167CI-32F40F BB-A(XC167) microcontroller. This 16-bit controller is broadly used in the automotive industry. For clock frequency, 20 MHz were selected and the Keil Vision3 v3.53 C-Compiler without optimizations is used.

As shown in Figure 4(a), the coded integer addition on the XC167 microcontroller is only about 3.5 times slower than the addition in the original domain. However, the corresponding floating-point addition (Figure 4(b)) is about 10 times slower. As mentioned above, the floating-point addition in the original domain is emulated in software, so that the difference to a calculation with a hardware floating-point unit (FPU) would be much higher. The mentioned integer addition as well as the floating-point addition are the easiest operations in the transformed domain. It is expected that for other arithmetic operations like multiplication or division the difference in performance between original and transformed domain is rising, especially for coded floating-point operations.

Due to this, SES could lead to a growing demand for performance if e.g floating-point operations should be safeguarded.

SES-Coprocessor

A possible option to raise the performance is to source out the SES part of the microcontroller by applying a SES-coprocessor.

External coprocessor approach

The SES-coprocessor connected to the microcontroller (Figure 5) contains a coded arithmetic logic unit (ALU c ) for integer and (if needed) floating-point arithmetic. The communication path between microcontroller and SES-coprocessor has to be safeguarded. This ALU c could be completely realized in hardware, so a complex programmable logic device (CPLD) or a field programmable gate array (FPGA) would be a proper platform for the SES-coprocessor. If a large number of units is expected, an application specific integrated circuit (ASIC) is a possible alternative. The interconnection between microcontroller and coprocessor could be realized by port-or memory mapping, also serial connections (CAN, I 2 C, etc.) are possible.

Hardware implementation of coded addition

This Section describes the realization of the coded integer addition in hardware.

Based on the definition of the coded integer addition (Section 2.2.1)

z c = x c + y c + (B z -B x -B y ) const.
-D

a simple hardware model could be created. The coded ALU c for integer-addition is shown in Figure 6 and consists of 2 adders and 3 subtracters in a serial alignment.

Overflow handling is not explicitly mentioned in this paper. Due to the concurrent logic approach of this model, the execution time of a coded addition only depends on the propagation delay of the gates, as there is no dependency on the clock frequency (of course, the propagation delay affects the clock frequency on the whole design). If we assume that Figure 6: Structure of a coded ALU for coded integeraddition the propagation delay of an adder/subtracter would be about 6ns, the calculation of a coded addition could be finished in about 30ns.

In a next step, this design could be optimized. A main advantage of a hardware implementation in comparison to software is the possibility to parallelize operations. The equation 7 could be rearranged as follows:

z c = (x c + y c + B z ) -(B x + B y + D) (8)
Based on the equation 8 we could modify the hardware model in the following way.

Figure 7 shows an optimized hardware model for a coded integer addition. In contrast to Figure 6, this ALU consists of 4 adders and 1 subtracter, two additions are done parallel in stage 1 and 2. Due to this, the calculation time of the coded addition is reduced to 18ns in this way.

With this SES-coprocessor approach, the performance of the system could be increased, but on the other hand additional hardware is needed.

Migration to a FPGA architecture

FPGAs allow a flexible, low-cost solution for control functions, bridging an interface between components or simply as glue logic for a variety of customized systems. Multiple functions could be integrated into a single-chip solution to reduce board space and costs [START_REF]Actel Corporation: Reliability Considerations for Automotive FPGAs[END_REF]. Many FPGA vendors provide powerful microcontroller soft cores (Table 2. So it would be obvious to integrate the microcontroller and the SES-coprocessor onto a single FPGA.

Single core processor with SES

State of the art FPGAs contain either hardwired microcontrollers (e.g. Xilinx Virtex 4) or a microcontroller soft core could be implemented. Figure 8 shows a FPGA including a microcontroller soft core and a SES-coprocessor. The SES-coprocessor is reconfigurable and contains the operations defined in the SES approach needed by the application. An increasing number of microcontroller soft cores is available, so there is a suitable device for many applica- This approach offers a couple of advantages:

• modular microcontroller concept -several microcontroller could be used on the same FPGA, so the microcontroller could be upgraded quickly due to modified requirements without changing any hardware components.

• modular SES-coprocessor concept -the SEScoprocessor could be easily adapted to the desired application, for instance only coded integer arithmetic could be installed or, if needed, coded floating-point arithmetic could also be implemented.

• concept verification with fault injection strategies (stimulated bit flips) in the soft core divider.

• automatic regression tests are also possible as needed for a safety assessment of the SES FPGA.

Multi core processor with SES

For higher SIL demands, this approach could be easily expanded by adding a traditional redundant hardware channel.

The approach described in figure 9 uses the existing know-how in redundant hardware design. The two microcontrollers have not necessarily be equal in this concept, two different soft cores can be implemented to reduce common cause failures. In this way, diverse hardware channels are achieved. This is a main advantage against a classical dual core processor, the two cores are mostly identical here. Although the

Further options to increase the performance

Some sensors need a special and complex signal conditioning which may consume a lot of processing power if it must be realized in software. Modern FP-GAs can hold more than one single microcontroller soft core and a SES-coprocessor, so dedicated digital hardware for signal conditioning could be easily implemented too. Also coprocessors for other special applications could be added. Some examples for such tasks:

• signal conditioning (digital filters),

• fast signal processing (DCT, DFT,...),

• fast arithmetic calculations (e.g. multiplications with high bit width),

• decoders or

• multiplexers Also external digital hardware components could be reduced by including them into a FPGA. So this approach increases performance, fulfills safety requirements with the SES approach and reduces the amount of hardware components.

Intelligent Sensors

A weak point concerning safety sensor data processing is the interconnection between sensor and host. Nowadays many sensors have a digital interface, in many case they can be directly connected to a bus system like LIN, I 2 C or CAN. Such a sensor comprises typically a microcontroller which is responsible for signal conditioning and connectivity. Considering the limited output range of a sensor a tailored SES unit could be implemented on this microcontroller too (Figure 11). This SES unit safeguards the transmission from sensor to host. For higher SIL demands the protocol could be extended by a message counter and a time counter.

Hardware -Software Codesign

Choosing a FPGA architecture including microcontroller and SES cores also affects the design methodology of the system. The possibility for hardware -software codesign allows the cooperative and concurrent development of hardware and software (cospecification, co-development, and co-verification) in order to achieve shared functionality and performance goals for a combined system [START_REF] Gupta | Hardware-Software Cosynthesis for Digital Systems IEEE Design & Test of Computers[END_REF], [START_REF] Mahr | Hardware-Software-Codesign Vieweg[END_REF]. In this way, the decision if a task should be realized in software or in hardware could be changed rapidly. Special sensor signal conditioning tasks could be either realized in software or in hardware (or any combination of that) without changing any hardware component. In a classic microcontroller design such a decision leads to an expensive and complicated design modification. Also the parallelization of hard and software design reduces costs of development and the time to market.

Conclusion and Outlook

The FPGA approach presented in this paper offers considerable advantages. On the one hand the performance of SES guided systems could be improved by sourcing the SES part out into a dedicated hardware. For this only a low density FPGA is necessary and possibly existing system could be retained. The fast growing performance of FPGAs allows on the other hand a complete integration of microcontroller and SES-coprocessor into a single component. Also specialized coprocessors for signal conditioning of sensor data or other individual tasks could be integrated. This leads to increased performance and a flexible approach for safety embedded systems. If the design methodology is adapted too, also economic advantages are possible.

Figure 3 :

 3 Figure 3: Simple coding x c = A * x f from the original into the transformation domain.

Figure 5 :

 5 Figure 5: Microcontroller with a SES-Coprocessor.The interconnection between microcontroller and coprocessor could be realized by port-or memory mapping, also serial connections (CAN, I 2 C, etc.) are possible.

  floating-point additions per second

Figure 4 :

 4 Figure 4: Performance of integer and floating-point additions in the original and coded domain on Infineon XC167CI-32F40F BB-A microcontroller

Figure 7 :

 7 Figure 7: Structure of a optimized coded ALU for integer-addition

Figure 8 :

 8 Figure 8: FPGA including microcontroller soft core and SES-coprocessor

Figure 9 :

 9 Figure 9: FPGA including dual microcontroller soft core and SES-coprocessor in a redundant hardware approach

Figure 10 :

 10 Figure 10: FPGA including microcontroller soft core, SES-coprocessor and several coprocessors for individual tasks

Figure 11 :

 11 Figure 11: Intelligent Sensors with SES

  Error detection techniques like ECC only check the validity of data in the RAM/ROM area. With SES it is possible to check the validity of data inside the whole memory area, including cache and CPU registers (Figure2).

			processing in hardware / software domain
			memory		1st channel (original domain)
			variables	OP 1
			constants			OP 2	OP n
		sensor	transform (edit time)	comparator	units	comp. unit 1 transform (runtime) comp. unit 2 optional optional	comp. unit n mandatory	actuator
			coded
			variables	coded
			coded	OP 1	coded
			constants			OP 2	coded
							OP n
			memory		2nd channel (transformed domain)
			Figure 1: Safe Sensor Data Processing
	or shutdown.
		Memory
		REGISTER
		CACHE
			Safeguarded
			by SES
	Safeguarded
	by ECC,	RAM/ROM
	etc...
	Figure 2: Safeguarded Areas
	2.1 Coding of Data
	Safely Embedded Software is based on the (AN+B)-
	code of the Coded Monoprocessor [1] transformation
	of original integer data x f into diverse coded data x c .
	Definition 1 (Coded Data) Coded data is data
	fulfilling the relation:

Table 1 :

 1 Representation of 32-bit IEEE 754 single floating-point number exponent, fraction) is treated as integer and transformed under the rules shown in section 2.1.Coded floating-point operations are also based on the coded integer operations (section 2.2.1, 2.2.2), so the parts of the floating-point dataset are processed separately with the coded integer operations.

	1	8	23
	S	Exponent	Fraction
	31		0

Table 2 :

 2 Table 2 illustrates a few examples (list is not exhaustive). Of course, a proprietary solution is also possible. common microcontroller soft cores

	Type Name	Vendor
	8-Bit	PicoBlaze	Xilinx
	16-Bit Nios II	Altera
	32-Bit Leon	Gaisler Research
	32-Bit MicroBlaze Xilinx


M Dievart

P Charbonnaud

X Desforges

An embedded distributed tool for transportation systems health assessment

Keywords: Distributed diagnosis, prognosis, health status, embedded systems, transportation systems

This article presents an embedded distributed tool for health assessment of complex systems. The presented architecture is based on a solving method for embedded technical diagnostics and prognostics. This tool provides services enabling the evaluation of the health status of complex systems. Diagnostic services provide information for the maintenance decision support system that leads to reduce the periods of unavailability and determine if their future mission can be carried out. The diagnostic and prognostic functions are detailed and the exchanged data are specified. An example shows the feasibility of the proposed architecture and demonstrates the correctness of the developed algorithms.

Introduction

Transportation systems are the objects of new regulations in terms of environment, goods and people safety, and the needs of new services have consequences on the complexity of embedded systems. To face this increasing complexity, multiple functionalities of the resources are embedded and deployed into networks of functions achieved by Line Replaceable Units (LRU). Faulty LRUs are replaced when the vehicle is at its base and repaired in the maintenance workshops, while the repaired system carries on with its mission. The increasing number of functionalities of the embedded systems contributes to raise the possession and acquisition costs leading the resources customers to optimize their availability rate.

Bringing into operation the Condition-Based Maintenance (CBM) recommendations usually improve the equipment availability [1,2]. Indeed, the CBM depends on the effectiveness of the system state provided by monitoring and diagnostic functions. They are carried out in particular from on line data that an embedded centralized diagnostic function generally process. However, in the case of system of systems also called complex system, the identification of the faulty components is difficult using centralized architectures. After the mission, the maintenance operators must collect information by interactions with the embedded diagnostic system, in order to isolate possible faulty LRUs, and to apply troubleshooting procedures. The drawbacks of such architectures are related to the numerous pieces of information to process, which might be wrong. The automated diagnostic processes combine these errors and lead to useless removals of LRUs. Those removals are costly and increase the risk of damaging the system.

The technical diagnosis of transportation systems provides to the maintenance operators a list of LRUs that should be replaced. When the diagnosis is done online, the maintenance operators prepare the intervention sooner, reducing the duration and the costs of maintenance actions. The main task of a diagnostic function is to deliver an advice on a set of faulty components and to determine the severity of the fault. A difficulty in diagnosing such complex systems is due to their numerous kinds of functions integrating different technologies (electronics, data processing, mechanics, hydraulics…). Thus, the implemented diagnostic techniques must be adapted to the knowledge available about the system. During its use, various faults may impact the resource. Those faults degrade its operating modes. Three types of faults are considered: Cataleptic, Permanent and Fugitive.

Different implementations of the monitoring and diagnostic functions associated to the LRUs exist. The LRU hosts its monitoring and diagnostic functions, the diagnostic function can also be hosted in another platform or, the monitoring and diagnostic functions can totally be distributed in different platforms.

In the case of aircrafts, the Centralized Maintenance System (CMS) provide a list of likely faulty LRUs for the maintenance operator. This list is established according to information provided by the built-in test equipments that collect monitoring information from the LRUs and generate tests if they are needed. CMS correlates data to provide a "pre-diagnosis" of the LRUs. The flight warning system provides to the cockpit crew information on aircraft failed functions [3,4].

Complex systems can be considered as sets of systems that depend more or less on each other. A system implements one or several functions. For safety purposes, functions can be redundant as well as the LRUs implementing them. That explains why several models are necessary to classify the different operating modes of the LRUs and their health status.

In this paper, a decentralized/distributed health assessment is proposed for reducing the number of useless removals of LRUs and for providing information about the availability of the system. For applications to systems of systems, monitoring and diagnostic functions can be implemented closer to the LRUs thanks to the multi-agent approach. In the case of a distributed approach, a collaborative mechanism between diagnostic agents have to enable the convergence of the local diagnoses towards a set of accused LRUs which should ideally correspond to the true faulty ones. Furthermore, prognostic agents are in charge of evaluating the Remaining Useful Lifetime (RUL) of systems and functions of the complex system from the RUL of LRUs provided by a monitoring layer. The Health Status is computed from the results provided by the diagnostic and prognostic agents.

System of systems modeling

Generally, the system is analyzed from different models in order to obtain a satisfying representation for diagnosis purpose. This analysis enables to collect the available knowledge on the complex systems. Many of them are helpful to design their diagnostic functions. In the literature [5][6][7][8], these models can be functional, structural, behavioral and teleological. They enable to model the behavior of components, of functions and of their interactions according to normal or degraded modes. In other studies, models are added to evaluate the diagnosis confidence [9].

A Complex System (CS) can be defined by a finite set of m system ∑ i . CS = {∑ 1 , ∑ 2 ,.., ∑ m }. A system ∑ i can be defined as a set of n function F i,j . ∑ i = {F i,1 , F i,2 ,..,F i,n }. A function F i,j can be defined as a set of k LRUs implementing this function. F i,j = {LRU i,j,1 , …,LRU i,j,k }. If a LRU contribute to the implementation of more than one function, this one should be duplicated as many times as it contributes to the implementation of function. If an LRU contributes to the implementation of 3 functions, it must exist three LRUs of that kind when defining the system. The fact that these LRUs are equivalent must be declared in the knowledge base. After defining the hierarchical decomposition of the system, a system modeling has to be formalized for ensuring system diagnostic. In this paper, the necessary System Knowledge to diagnose the complex system are collected in the set SK made of four types of knowledge: functional, structural, behavioral and topological.

The Functional Description (FD) is the set of functions ensured by every system. FD represents links between LRUs, functions and system. The Structural Description (SD) is dedicated to the identification of the set of LRUs and of physical connections between them. SD introduce predicate CONNECT(X,Y) that means that X is connected to Y. S : CONNECT(LRU i,j,q , LRU p,r,s ) with q and s respectively one of the LRUs implementing F i,j and F p,r . The behavioral models are used in order to identify the relevant indicators that are used to generate symptoms for the various faults that may affect the LRUs. They help to classify the faults of the LRUs from their symptoms. For diagnostic purpose, the knowledge BM provides the relationships between the symptoms, the LRUs and their faults. The Topological Dependencies (TD) determines the proximities of components that may be the origin of indirect failures or faults of a LRU due to the proximity of another failed one. TD introduce predicate TOPO(X,Y) that means that X is close to Y and that some faults of X may affect the functioning of Y. TD: TOPO(LRU i,j,q , LRU p,r,s ) with q and s respectively one of the LRUs implementing F i,j and F p,r .

Finally, BM TD FD SD = SK

Embedded health assessment

The OSA-CBM project [10] defines a Health Assessment (HA) layer whose primary function determines the health status of a monitored system, subsystem, equipment or component in terms of fault, failure, availability. The health assessment module should take into account diagnoses, trends in the health history, operational status and loading, and the maintenance history. The HA layer provides the Health Status (HS) of a monitored entity.

Prognostics and Health Management (PHM) is defined in [11] as the phase involved with predicting future behavior, including RUL, in terms of current operating state and the scheduling of required maintenance actions. According to [12], diagnosis and prognosis are processes of assessment of a system's health. Diagnosis is an assessment about the current and past health of a system based on observed symptoms, and prognosis is an assessment of the future health. The different results given by diagnostic and prognostic functions must be considered as a decision support to operate appropriately on the system. In the proposed approach, the HA is introduced as a combination of the results of the diagnostic and prognostic functions.

Ideally, the diagnosis identifies a set ∆ 2 of failed function and locates their causes, i.e. a set ∆ 1 of faulty LRUs from a set of symptoms S and a set of tests T. This leads to the next relationship where Diag is the diagnostic function:

(∆ 1 , ∆ 2 ) = Diag(SK, S, T)

The function Diag can be implemented thanks to two sub-functions: Diag1 and Diag2. The function Diag1 allows, starting from a set of symptoms and a set of tests, to identify the set of faulty LRUs of the system

∆ 1 = Diag1(SK, S, T),
where ∆ 1 = {AB(LRU i,j,k ),…,AB(LRU p,r,s )} and the function Diag2 enables to locate the set of failed function from tests and the set of failed LRUs:

∆ 2 = Diag2(SK, ∆ 1 , T)
where ∆ 2 = {AB(F i,j ),…,AB(F p,r )}. AB(.) denotes either a faulty LRU or a failed function.

The prognostic function, that completes the diagnostic function, has been the subject of many studies since the end of the 90s. Prognostic allows determining the RUL of a component or a system [13]. In [14], the prognostic is defines as the capability to provide early detection of the precursor and/or incipient fault condition (very "small" fault) of a component, and to have the technology and means to manage and predict the progression of this fault condition to component failure. A global point of view of the studies realized on prognostic is proposed in [15]. The RUL can either be determined by indicators extrapolation or from failure probability of the component of the system like the Mean Time To Failure (MTTF) or the Mean Time Between Failures (MTBF). The RUL is an assessment of the remaining operational time until the system becomes unable to complete its mission successfully according to the conditions of operation. This means that the prognostic function requires a historic of the current and future mission with their constraints. This knowledge allows determining thresholds beyond which the LRU cannot carry out the mission in nominal mode. In short term, the data about the current mission are used online and in long-term, the data about the future mission are used when the system is in the maintenance area. Of course, this threshold is not useful when determining the likelihood of failure. The RUL of an LRU is ensured by the monitoring layer. Let us note RUL(LRU i,j,k ) the RUL of the LRU i,j,k , TBAB(LRU i,j,k ) the Time Before Abnormal Behavior of the LRU i,j,k . and TBAB(F i,j ) the TBAB of the function F i,j , As it exists dependencies between LRUs and RUL are the data generated by the monitoring, TBAB is introduced and can be defined by : TBAB(LRU i,j,k ) = Min(RUL(LRU i,j,k ), TBAB(LRU i,j,k ), TBAB struc (LRUs)) where TBAB struc (LRUs) is the set of TBAB of upstream structurally dependent LRU of the LRU i,j,k .

Therefore, for a given function F i,j without redundant LRUs, RUL(F i,j ) = Min (TBAB(LRU i,j,1 ), …, TBAB(LRU i,j,k )). Let us considered now the case of a function F i,j implemented by A redundant LRUs. And this function is not considered as failed if at least B of A LRUs are not failed. In this case, TBAB(F i,j ) is equal to the B th maximum RUL among the A TBAB of each LRUs implementing F i,j . For example, if a function F i,j is ensured by LRU i,j,1 , LRU i,j,2 and LRU i,j,3 , and the function is not considered as failed if at least 2 of this 3 LRUs are not failed. Given RUL(LRU i,j,1 ) = 5UT, RUL(LRU i,j,2 ) = 10UT and RUL(LRU i,j,3 ) = 15UT, TBAB (F i,j ) = 10 UT.

Ideally, the prognosis identifies the set ∏ 2 of the RUL of each function implementing the system of systems and the set ∏ 1 of RUL of each LRU from a set of extrapolated data ED and a set of threshold Th. This leads to the next relationship where Prog is the prognostic function:

(∏ 1 , ∏ 2 ) = Prog(SK, ED, Th) The function Prog can be implemented thanks to two sub-functions. The function Prog1 allows, starting from a set of extrapolated data and a set of threshold, to identify the set of TBAB of the LRUs of a function ∏ 1 = Prog1(SK, RUL, TBAB), where ∏ 1 = {TBAB (LRU i,j,k ),…, TBAB (LRU p,r,s )} and the function Prog2 enables to locate the set of failed function from tests and the set of failed LRUs: ∏ 2 = Prog2(SK, ∏ 1 ) where ∏ 2 = {TBAB (F i,j ),…, TBAB (F p,r )}. TBAB (.) denotes either the TBAB of a LRU or the TBAB of a function.

In this paper, the health management of the system is ensured by a diagnostic function and a prognostic function. Data produced by these functions, list of RULs, faulty components and failed functions, are differently interpreted according to the current end user of the system. This implies the use of different kinds of histories and knowledge, including safety limits of the system defined by the operator. Considering HS(X) the Health Status of X, the health status of an LRU can be defined by:

)) AB(LRU ) (TBAB(LRU )) ¬AB(LRU ) (TBAB(LRU = ) HS(LRU k j, i, k j, i, k j, i, k j, i, k j, i, Considering j i, F Δ 1
the list of failed LRUs implementing the function F i,j and j i, F Π 1 the list of the RUL of LRUs implementing F i,j the health status of F i,j can be defined as:

) Π (Δ = ) HS(F j i, F j i, F j i, 1 1
. The health status of the complex system is also defined as:

) Π (Δ = HS(SC) 2 2
and can be described as a use case diagram available in figure 1. Technologies often provide satisfying solutions to face complexity. The diagnostic function was implemented in a distributed structure according to the multi-agent system concept. The agents of the structure cooperate and exchange data whatever the language used to model the information they contain is. This implementation requires data and models that have been collected and organized. In the case of complex systems, some works [16][17][18] show the feasibility to implement an embedded distributed diagnostic function with or without cooperation between its elements.

In figure 2 Several types of data are considered: a "symptom" is generated by the monitoring layer, a "faulty LRU message" is generated by the function "To propagate symptom" of a DA. A "known symptom" is has at least one cause identified by an analysis done at the system design stage and stored in KB. An "unknown symptom" has no cause identified in KB.

The activities of the diagnostic function are carried out by cooperation between the DAs. The reception of a symptom by a DA starts the process. The corresponding DA begins by inserting the received symptom in the chronologic list according to the date the monitoring layer. Then, the DA checks the type of symptom received. If the symptom is known, the database returns the cause of failure of the LRU and the DA declares it as known, otherwise, the cause of failure of the LRU is declared as unknown. It also manages the list of symptoms, chronologically. ∆ 1 and ∆ 2 are updated according to the type of the symptom and the answers of the database dealing with a status of the symptom (known or unknown) in the case of a failure symptom. Then, the DA searches structural dependencies with the failed LRU thanks to KB. If there is at least one dependent LRU, "propagation symptoms" are sent to the DAs that diagnose those LRUs which may not operate correctly and are declared "out of order". During this stage, the DA updates ∆ 1 and ∆ 2 according to the chronological list of symptoms. The status and the timestamp of the LRU are updated and data are recorded and displayed. Supervision of the DAs is ensured during "the fault propagation" function. If a DA did not confirm that it receives the message during the propagation task, the diagnostic process declares the agent as failed.

The evolution of the status of a LRU is shown in figure 3. An LRU is declared as "OK" at the beginning of the process. If an "unknown symptom" is received, the status switches to "unknown failure" (see (1) in the figure). If a symptom is received and this symptom (or set of symptom) is known, the status of the LRU is defined as "known failure" (see (2) in the figure). The reception of a Faulty LRU message only allows switching the status of the LRU from "OK" to "Out of Order" (see (3) in the figure). Four different values describe the state of a LRU:

"OK" when the LRU is not faulty, "UF" when the LRU is faulty but the cause is unknown (Unknown Failure), "KF" when the cause of its failure is known (Known Failure), "OO" when the LRU does not work in nominal mode or is failed because of the failure of another LRU (Out of Order). In our case, the status of an LRU evolved differently. The status of the LRU is estimated by the DA that received data whose causality is not respected (according to apparition timestamp). As it is possible to challenge the order of reception of the data (symptoms and Faulty_LRU_Messages), the evolution of the status of a LRU is different as shown in figure 4. The red arrows denote that the causality was not respected. Arrows number 4 (in the case of an unknown failure) and 5 (in the case of a known failure) in figure 4 mean that a faulty LRU message has been diagnosed before a symptom. Arrows numbers 3 and 6 in figure 4 mean that a symptom has been diagnosed before a faulty LRU message. The arrow number 7 denotes that a symptom or a set of symptoms was firstly declared has unknown but, because of the symptom(s) received afterward, it becomes a known failed situation. When a LRU is subjected to a known or an unknown failure, the known failure is privileged in the results. Whatever the kind of failure is known or unknown, the LRU must be removed.

Therefore, there are two different ways to process the diagnosis depending on data received by the DA (symptom or Faulty_LRU_Message). Whatever the data (symptom or Faulty_LRU_message) the diagnostic function has to deal with, the results are recorded in the blackboard of the DA. Every time the DA receives a symptom or a Faulty_LRU_message, the old diagnostic result is duplicated and one copy is updated according to the data received. The blackboard of a DA contains the evolution of the status of the LRUs and of its implemented function and the data (symptom or Faulty_LRU_message). From this historic, it is possible to track the evolution of the status of each LRUs and each function of the system according to received data. The algorithm of the function ToDiagnose(Symptom) describes the behavior of the diagnostic function when a DA receives a symptom sent by the Monitoring layer.

Algorithm ToDiagnose(Symptom)

Return the results in the blackboard of the DA 1. Begin 2. Verify the symptom chronology 3. Define L the list of data ever diagnosed that appeared after symptom received 4. Query the database for knowing if the failure is identified 5. Change the status of the LRU incriminated by the symptom according to database answer and LRU current status (OK to UF, OK to KF OR UF to KF) 6. While L is not empty 7.

ToDiagnose(L.data)

Algorithm ToDiagnose(Faulty_LRU_Message)

Return the results in the blackboard of the 1. Begin 2. Verify the Faulty_LRU_Message chronology 3. Define L the list of data ever diagnosed that appeared after Faulty LRU Message received 4. Change the status of the LRU incriminated by the Faulty LRU Message (OK to OO) 5. While L is not empty 6.

ToDiagnose(L.data)

7. EndWhile 8. Query the database for structural dependencies 9. While it exists dependencies 10.

Send(Faulty_LRU_Message) to DA

EndWhile 12. End

The activities chain involved when a symptom is generated is showed in figure 5 . The Send function sends Faulty_LRU_Message to the DA in charge of diagnosing the LRU incriminated by the Faulty_LRU_Message and launch the algorithm "ToDiagnose(Faulty_LRU_Message)" of this DA. Aiming at prognosing the LRUs and the functions, the monitoring layer sends RUL of each LRU periodically to corresponding Prognostic Agents (PAs). Each PA is prognosing one function of the system and uses KB. Figure 6 shows the activity diagram of a PA. The reception of a RUL or a TBAB_message by a PA starts its process. A TBAB_message is a message send by a PA to a PA. A TBAB_message is composed of the number of the upstream LRU monitored by the PA that sends the TBAB_message, the calculated TBAB of this LRU and the number of the LRU the upstream LRU is structurally connected to. Finally, the TBAB_message is send to the PA that computes the downstream LRU. The involved PA updates the Time Before Abnormal Behavior (TBAB) of this LRU in the list it manages for each LRU implementing the function it prognoses. When a PA receives for the first time a TBAB_message from another PA that prognoses an upstream LRU, it records the TBAB_message. This record is updated every time it receives another TBAB_message from the same PA that prognoses the same upstream LRU. The PA defines the TBAB of the corresponding function. Then, it sends the TBAB (encapsulated in TBAB_Message) of this LRU to the PAs prognosing functions carried out by LRUs depending on the LRU for which the TBAB has been received. These PAs may then update the TBAB of their prognosed functions. As the RUL is defined to be the data that define remaining useful lifetime of a LRU processed by the monitoring layer, TBAB is defined to denote the same concept but take into account the structural dependencies of the LRU. It is to note that TBAB may be equal to RUL if the RUL sends by the monitoring is minor than the TBAB of upstream LRUs among the structural dependencies. Therefore, there are two different ways to process the prognosis depending on data received by the PA (RUL or TBAB_message). Whatever the data (RUL or TBAB_message) the prognostic function has to calculate, the results are recorded in the blackboard of the PA. Every time the PA receives a RUL or a TBAB_message, the old prognostic result is duplicated and one copy is updated according to the data received. The blackboard of a PA contains the evolution of the TBAB of the LRUs and its function implemented and the data (RUL or TBAB_message). For each TBAB of the LRUs, the data (RUL or TBAB_message) from which the TBAB has been computed are recorded. From this historic, it is possible to track the evolution of the TBAB of each LRUs and each function of the system according to received messages. Query the database for structural dependencies 6.

While it exists dependencies 7. The sequence of activities involved when a RUL is generated is similar to the one involved when a symptom is generated (see figure 5). For the prognosis, RULs are generated by the monitoring layer to PAs and TBAB_Message are exchanged between PAs.

Send(TBAB_Message)

Both functions (To diagnose and to prognose) are activated when the HA system is started, but the diagnostic and prognostic functions are only processed when they receive a message, otherwise, they stand by. Diagnostic and prognostic sessions are finished when all the DAs and PAs are in sleeping mode.

Example of implementation

An example of implementation of the distributed HA function onto a system made of 2 functions both ensured by 3 LRUs is given in figure 7. This structure leads to the HA function to be implemented by 2 DAs and 2 PAs. DAs and PAs receive data generated by the monitoring layer respectively symptoms (full arrows between monitoring and health assessment layers) and RULs (dotted arrows between monitoring and health assessment layers). DAs communicate between them and KB (bold dotted arrows inside the health assessment layer). PAs do it between them and KB (bold arrows inside the health assessment layer) too. In fact, the communication between Agent of the same nature (DA or PA) is processed according to the structural dependencies between LRUs and the description of Each time a DA receives a symptom, it copies Δ1 and Δ2 in its own blackboard and updates them with the result computed from the new symptom. This carries out the tracking of the evolution of the diagnostic process and this enables the diagnostic process to be non-monotone. If the DA receives a "propagation symptom", this one is used to refine the diagnosis. To explain this activity, let us considered the example with 1,1,1 LRU , 1,1,2 LRU and1,1,3 LRU that are structurally dependant. SD (the only considered knowledge for this example) contains knowledge about the system:

CONNECT( 1,1,1 LRU , 1,1,2 LRU ), CONNECT( 1,1,2 LRU , 1,1,3 LRU ).
Each LRU has its proper monitoring periods for its symptoms. For example, if we consider one symptom per LRU, we suppose that the symptom emitted from the monitoring of LRU are declared as "out of order". The evolution of the status of these 3 LRUs according to the order of reception of symptoms is described in the chronogram in figure 8. The state of the LRU changes and the timestamps of its changes are updated. At the end of the HA process, a list of faulty LRUs with their causes, their dated changes of status and a list of failed functions are available. The causes of faulty LRUs are described in terms of sentences from FMEA studies or of faulty LRUs for "OO" LRUs. The causes of failed functions are described in terms of faulty LRUs.

Considering the example as described in figure 7 with this failure: LRU 2,1,1 failed and the cause of the failure of LRU 2,1,1 is known to be a power failure. After symptom generation, the diagnosis result is given by:

Conclusion

The distributed diagnostic and prognostic functions, presented in this paper, implement a distributed health assessment for systems of systems. The health assessment is here based on a monitoring layer that provides symptoms and estimations of the remaining useful lives of the components of the system.

The proposed diagnosis is a non-monotonic process that permits to take into accounts the events

Figure

  Figure 1: Use case diagram of a maintenance system

  , the architecture presented is based on a distributed implementation. Local diagnostic agents cooperate to diagnose the system. A middleware makes it possible to implement the services provided by the agents. The architecture consists of several LRUs gathered into several functions denoted LRU layer. Each LRU is observed by a monitoring function. The monitoring layer represents the monitoring functions designed by the suppliers. The monitoring functions send their symptoms to Diagnostic Agents (DAs). Using the cause-symptom relations, each DA determines the set of faulty LRUs among the LRUs that implement a function. One or more databases (KB) contain the set SK that supports the activities of the DAs. A Human/Machine Interface (HMI) displays the failed functions of the system for the production operators and the LRUs to replace or to fix for the maintenance operators. If the collaboration is correct the global diagnosis of the system in terms of faulty LRUs is the union of local diagnoses.

Figure 2 :

 2 Figure 2: Distributed approach of Health Assessment

Figure 3 :

 3 Figure 3: Status of a LRU

Figure 4 :

 4 Figure 4: Estimated LRU status by DA

  Query the database for structural dependencies 10. While it exists dependencies 11. ) describes the behavior of the diagnostic function when receiving a Faulty_LRU_Message sent by another DA.

Figure 5 :

 5 Figure 5: Activity Diagram of the distributed diagnosis system

Figure 6 :

 6 Figure 6: Activity Diagram of PA The algorithm of the function ToPrognose(RUL) describes the behavior of the prognostic function when a PA receives a RUL sent by the Monitoring layer.

Figure 7 .

 7 Figure 7. An example of implementation of a distributed health assessment function

  as "out of order". DAs receive the symptoms when it is detected by the monitoring layer. Firstly, the DA receives 1,1

∆ 1 =

 1 LRU 2,1,1 (status: KF, cause: power failure, timestamp: 2009/07/05 15h26min56s) & LRU 1,1,2 (status: OO, cause LRU 2,1,1 failure, timestamp: 2009/07/05 15h26min57s) ∆ 2 = Function 11 (status: OO, cause: function 12 failure, timestamp: 2009/07/05 15h26min58s) & Function 21 (status: KF, cause: LRU 2,1,1 failure, timestamp: 2009/07/05 15h26min57s)In each set ∆ 1 and ∆ 2 the LRUs or functions that do not work in a nominal mode are listed with their current states, the causes of their failures and the timestamps of their changes of state.

Figure 8 :

 8 Figure 8: Chronogram of the evolution of the status of LRUs

2Π

  = RUL (F 1,1 ) = 10 TU, RUL (F 2,1 ) = 20 TU.

detected by the monitoring layer and time stamped before their asynchronous transmissions.

All the pieces of diagnostic and prognostic data and their timestamps are recorded to enable performance evaluation at the end of the health assessment session. Performance indicators (speed of convergence, data flow, and computational load...) may therefore be evaluated from the timestamps of the different data that are exchanged between the agents or stored. Further works will deal with performance evaluation of the proposed structure compared to centralized structures.

Acknowledgement

The project was supported by Airbus France.

References [1]

Jardine, A., Lin, D. and Banjevic, D.