E Ledinot

D Pariente
email: dillon.pariente@dassault-aviation.fr

Formal Verification of Hand-Coded Software Some Industrial Experiments and Lessons Learnt

Keywords: Software verification, Hoare Logic, Theorem Proving, Caveat, Caduceus, Why, Coq, Simplify

This paper gives an account of an ongoing attempt to prove the safety properties, of a hand-coded safety critical embedded software of industrial size. The method used is based on annotating the C source files with assertions that encode the safety-related functional properties to be satisfied by the software, and then generating proof obligations to be discharged by some theorem provers. We discuss what has been achieved and what difficulties were encountered, from which we derive requirements regarding the evolution of the verification tools involved in that experiment.

Introduction

Since 1990, Dassault Aviation has carried out numerous formal methods studies and assessments. The first ones were focused on synchronous languages (first Esterel [START_REF] Berry | Esterel: a formal method applied to avionic software development[END_REF], then Lustre), for control and data flow formal specification, coding and model checking through collaborations with research teams. Over the last few years, much effort was devoted to the integration of UML modelling and signal flow programming (Matlab, Scade, Esterel), in order to introduce these new methods and tools in the Flight Control System (FCS) software development process.

Following the Model Driven Engineering approach (MDE), parts of an embedded software were reengineered with Matlab/Simulink, Rational Rose and Esterel Studio [START_REF] Le Biannic | Spécification Objet UML de logiciels temps-réel[END_REF]. By the end of 2003, the first control module formally specified in a graphical way, automatically generated (~15 Kloc), and proven was embedded in a military aircraft operational software.

In the meantime, some experiments on formal verification of hand-written code were initiated, because in numerous situations pieces of software of high criticality level cannot be generated from formal specification models. This is especially the case for programs encoding algorithms with complex control or data structures (nested loops, extensive use of pointers, etc.), or for system level programming (drivers, schedulers, coding/uncoding of data formats etc.). This is also the case when software engineers don't want to be constrained by restricted specification languages. This is the basis of our motivation to assess the theorem proving approach to formally verify annotated hand-coded imperative programs, from which are generated proof obligations to be later discharged by automatic deduction tools, or by interactive theorem provers when the available decision procedures fail.

In the following, we will briefly introduce the underlying technical background and the two tools we have been assessing for the last two years: Caveat [6], [START_REF] Baudin | CAVEAT: A Tool for Software Validation[END_REF] and Caduceus [5]. Then we proceed by stressing some of the lessons we learnt and by presenting some general requirements to improve these formal verification tools. We aim to use them operationally in the mid-term, trying to follow the way that has been paved by B-method & tool [START_REF] Behm | Météor : A successful application of B in a Large Project[END_REF].

Background

To be able to present our past and current experiments in proving the correctness imperative programs, we propose at first a brief and non formal presentation of the underlying method and foundational background. For rigorous explanations, please seek the abundant references and tutorials related to the subject, for instance [START_REF] Hoare | Unifying Theories of Programming[END_REF].

2.1 Reminder of basics : Floyd-Hoare's logic Correctness proof of imperative program is essentially based on Floyd-Hoare's logic [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. The main purpose of this logic is to provide a set of rules defining how to formally reason about the properties of imperative programs.

Hoare's logic is based on a triple which describes how the execution of a statement changes the state of data variables. A Hoare triple is defined as : {p} S {q} where p and q are respectively the precondition and the postcondition (expressed as first order logic formulas), and S is a programming statement. The whole expression means that if p holds before the execution of S, then q will hold after the execution of S, if S terminates (partial correctness).

The assignment rule is the following one :

Rassign:

-----------------{p[y/x]} x:=y {p} which states that if p holds after the assignment (x:=y), then p, where all occurrences of x have been substituted by y, holds before that assignment. For example, {x>-1} x:=x+1 {x>0} is a valid triple.

In the same way, Hoare defined the following well known rules:

Rsequence: {p} S {q} {q} T {r} ---------------------{p} S ; T {r}

Rcondition: {p /\ C} T {q}{p /\ ¬C} E {q} ------------------------------ {p} if C then T else E {q} Rloop: {p}=>{inv} {inv /\ C} S {inv} {inv /\ ¬C} => {q} --------------------------------- {p} while (C) do S {q}
where inv is an invariant of the loop, which holds before, after, and for each execution of the loop body. As a matter of fact, this rule describes a recurrence principle. Since these rules are partial correctness rules, loop termination for instance has to be established. This is done by identifying a loop variant (var) which must be positive when entering the loop, and decrease towards 0 at each loop turn.

Verification conditions, proof obligations and weakest preconditions

A weakest precondition (WP) is computed by backward propagation of a given property through statements, according to Hoare's logic rules. Hence, a WP function takes two arguments: a statement S and a property q, and returns the most general condition c over the execution state just before executing S, such that q is valid after S execution. This is usually written:

c := WP( S, q )
A verification condition is defined w.r.t. a given property q to be proved valid after execution of a statement S, and a precondition p which holds before S, as follows: q holds after S if p holds before S. Formally, we can write the verification condition as:

p => WP( S, q )

Sometimes, verification conditions may be too difficult to prove in only one formula like the previous one. Typically, for loops, the verification condition has to be split into several proof obligations; if we want to prove valid the following triple:

{p} while (C) do S {q} whose verification condition is:

p => WP( while (C) do S, q )

we will have to prove valid three proof obligations related to invariance (the necessary invariant inv is generally provided by the user), and two proof obligations related to termination (w.r.t. the variant var).

Hoare's logic extensions: dealing with function calls

Hoare's logic needs to be extended so that WP can still be computed through function calls. The solution can not be to inline called functions as it could make WP computations rapidly explode in size. The way current program provers work is more reasonable: function calls are replaced with the properties (pre and postconditions) of the called functions.

In the following example, in the body of function f, the call to function g will be "replaced" by {pre g } and {post g } which are respectively the precondition and postcondition of function g (after substitution of function parameters and predicate parameters):

{pre g } void g(…) { … } {post g } {pre f } int f(…) { Sf1; g(…); Sf2;} {post f }
Before propagation of pre/postconditions of called functions

{pre g } void g(…) { … } {post g } {pre f } int f(…) { Sf1; {pre g } /* g(…); */ {post g } Sf2;} {post f }

After propagation of pre/postconditions of called functions

The new verification condition to be proven valid is:

{pre f } => WP(Sf1,{pre g })
which specifies that the preconditions of function g must be satisfied by any statement executed before. The verification condition :

{pre f } => WP(Sf1,{post g }=> WP(Sf2,{post f }))
which expresses backward propagation of postcondition post f through the code of function f, and "embedding" the postconditions of function g.

Remark about WP computation:

It is worth mentioning that, in many tools, WP is not computed as described, i.

RHS: code with function assignments and call LHS: generated verification condition

The two functions f and g are respectively annotated by postconditions. The verification condition is displayed on the right hand side: it is computed on the basis of a forward propagation and quantification instead of classical WP computations.

Assessment of verification tools

In this paragraph, we will focus on two different C program verification tools: Caveat, developed at CEA [6] and Caduceus developed at LRI [5]. Caveat and Caduceus are based on Hoare's logic and are both dedicated to proving correctness properties specified through annotations of C statements. They propose different, and to some extent complementary, features, methodologies of use, advantages and limitations.

Both tools were assessed on the same embedded software, a 70+ Kloc module in charge of fault detection, isolation and recovery (FDIR) for a group of sensors. It mainly consists in voting algorithms and a failure management logic. About 70 consolidated parameters are delivered by this sensor management module, and five safety properties have to be proved per parameter.

Experiments with Caveat

Caveat [6], [START_REF] Baudin | CAVEAT: A Tool for Software Validation[END_REF] is a static analysis tool designed to help verify safety properties on critical software. It operates on ANSI C programs. It was developed by CEA, the French Nuclear Agency, and is used as an operational tool by Airbus-France (to replace some unit tests by formal verification), as well as EdF, the French electricity company.

It is based on WP computation and first order rewriting techniques (proof engines). The main features of Caveat are navigation facilities, property synthesis, and automated or interactive deduction.

Program verification methodology, in brief

First step: Caveat performs an automatic analysis of the whole project, which leads to the generation of: -properties related to preventing runtime errors such as null pointer assignment, division by zero, out of bound array access, etc, -the input variable list, -the output variable list (including side-effects), -the functional expressions for every function output. Depending on selected strategies (discussed below), these functional expressions can be used as postconditions during WP computations.

Second step: the user can annotate the code with: -other preconditions, -postconditions, especially when Caveat was not able to generate functional expression for outputs needed to prove a given property (failing to generate a functional expression is generally due to the presence of a loop), -loop invariants and termination conditions (variants), -intermediate assertions (optional), aiming to simplify the task of WP computation.

Third step: a given property (a proof obligation, a postcondition, or an assertion) is selected by the user who then triggers the Caveat simplifier and prover to prove that property. Caveat returns either true, or false (in case of false, a counter-example is displayed), or provides the user with a residual formula (remainder) whenever the rewriting engine was not able to prove the property.

In case of a residual formula, the user is provided with an interactive rewriter. The rewriting task (e.g.: transforming the given formula into conjunctive normal form, disjunctive normal form, splitting it by case, folding/unfolding definitions, etc.) aims at transforming and simplifying manually the residual as much as possible, in order to obtain a true or false value or a remaining formula that can not be simplified anymore. Often, this remaining formula is a missing precondition that the user should add as a new annotation.

Note that the remaining formula must be accurately analyzed by an expert user familiar with logic and with a deep knowledge of the C code, as it is generally not clearly readable (residuals are the results of WP computation and automatic rewritings that render original properties quite unrecognizable!).

User strategies

It is important to note that the following strategies can improve effectiveness and productivity of program verification with Caveat:

-postconditions annotated by the user can be preferred to functional expressions generated automatically, -user assertions can be left over during WP computations, -when taking into account postconditions or assertions, it is possible to ask Caveat to quantify any variable belonging to the predicates. Universally quantified variables do not need to be dealt with by WP computation. This results in saving computation time, and in simplifying the proof obligations and proof residuals. Any use of these strategies needs a deep analysis and experience, as its efficiency strongly depends simultaneously on the structure and size of the properties, verification conditions and source code.

Experimenting on small examples is of course relevant, but does not provide all the needed insights when facing an actual industrial size software.

Some lessons learnt :

Compared with other program verification tools, and after experimenting with Caveat on real applications, the major advantage of the tool turns out to be the generation of functional expressions for all function outputs (these functional expressions are used as automatically generated postconditions). During our assessment, we definitely appreciated this functionality.

Some drawbacks imposed limitations difficult to overcome. For example, we had too often to cope with the automatic prover weaknesses: this one was not powerful enough to handle large size pieces of code and large verification conditions.

Even for some proof obligations that looked trivial, a proof was not always computable: the automatic rewriting engine of Caveat (without any heuristic or means to disable this automatic step) systematically enlarged the verification condition size so that subsequent manual interactions were unfeasible in an economically reasonable amount of time. Some limitations were also encountered on non ANSI C syntactic features, and most importantly on aliases (pointers pointing to the same memory location). Unfortunately the embedded C code we chose to experiment with Caveat made extensive use of aliases that Caveat couldn't handle.

These problems and a few others are going to be fixed. As an example, Caveat is known to be able to deal with aliases in its latest releases, and work is done to automate relevant invariant generation using abstract interpretation.

Results

We succeeded in proving four safety properties over a 3Kloc alias-free sample of the 70+ Kloc software mentioned previously. After a significant training period that made a software engineer become a Caveat experienced user, it took him nearly six manmonths to achieve this encouraging but limited result.

A first objective of the evaluation was to prove five safety properties for one parameter on the full code, and then to prove the 350 properties (5 properties for each of the 70 parameters). But the software to be proven correct, which was developed in parallel with our experiment, turned out to make an extensive use of pointers and aliases. Unfortunately, two years ago Caveat was not able to handle true aliases efficiently. To try to overcome this limitation, we moved to Caduceus whose first assessable version was released in September 2004.

Experiments with Caduceus

Caduceus [5] is a promising new C program verification tool which is still under development at LRI -Université Paris Sud. It is a proof obligation generator also based on Hoare's logic, though with some foundational background rooted in the typetheoretic approach of proof assistance [START_REF] Filliâtre | Preuves de programmes impératifs en théorie des types[END_REF], [8]. This background may have some importance in the long run when verification of verification tools will become a major issue, especially for the use of this kind of tools on software development processes subject to certification.

Program verification methodology, in brief

At first, an important point to outline is Caduceus' ability, thanks to an inner memory management model, to deal efficiently with aliases. This allowed us to apply Caduceus to our benchmark 70+ Kloc C embedded code, containing potential and actual aliases.

The first step of the program verification methodology consists in annotating the C code. For the moment, and it is to our opinion the main drawback of Caduceus, no functional expression is automatically generated from program expressions for output or global variables. This results in a big difference with Caveat annotations: Caduceus annotations are more voluminous and cumbersome to write because arithmetic and logical computations have to be manually paraphrased at the predicate level. On large pieces of software the size of annotations blows up, jeopardizing scalability.

Annotations are specified as comments inside the code (especially for loop invariants), or in the function declaration files (as headers ".h" files). These annotations are expressed into Java Modelling Language (JML) and some extensions. JML is a behavioural interface specification. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. JML is not limited to Java code, of course, and LRI has adapted it to the needs of property specification on ANSI C programs.

As usual, the possible annotations are preconditions, postconditions, invariants and variants, assertions, and assignments (i.e., for each function or loop, the list of updated/assigned variables must be provided by the user).

Of course, when working on a large source code, some of the annotations mentioned above are very time-consuming to write manually. In many cases, trivial postconditions or preconditions, simple invariants and variants, and all assigned variables could be generated automatically.

In the particular case of safety critical embedded software for which only a subset of possible C statements are authorized, a lot of non functional annotations could be generated as early as the parsing phase of the code.

LRI is currently working on these issues, and some important results are expected in the next months. To deal with the 70+ Kloc code we developed an inhouse prototype of annotation generator. This generator, mainly developed in CAML, produced automatically (in 10 minutes on a 1GHz PC) all the expected simple invariants, variants, loop and function assignments, and most of the preconditions related to non-null pointers. The same task done manually by an experimented user was evaluated to a 3-month workload. It took 3 weeks to develop the first version of this prototype generator which does not address all possible C statements, but only those currently used in our benchmarking embedded code.

Second step: what we call Caduceus is indeed a tool suite (Fig. 1). It is a pipeline of processors: the Caduceus compiler feeding the Why compiler [START_REF] Filliâtre | Preuves de programmes impératifs en théorie des types[END_REF], [16], which in turn generates proof obligations in different formats to be handled by different theorem provers: interactive proof assistants such as Coq [8] and PVS or decision procedures such as Simplify [START_REF] Detlefs | Simplify theorem prover[END_REF] and haRVey [11]. From the end-user point of view, the Why compilation is completely transparent, and it is mentioned here because Why is used as an intermediate language. The Why language is able to express high level order functions and to manipulate abstract types, thus providing a powerful means for WP computation. Why is designed so that type theory based consistency checks of the generated proof obligations with respect to annotations could be performed.

An important point to notice is that the annotation style depends on the targeted theorem prover: the way hypotheses and axioms are expressed must be defined according to some inner features of the targeted provers.

For example, with Simplify, the following two sets of axioms, that both define by recurrence the sum of the elements of an array, are treated quite differently by Simplify's deduction strategies:

axiomA1: \forall int tab[], int i, int j; i>j => sum(tab,i,j)==0 axiomA2: \forall int tab[], int i, int j; (i<=j)=>sum(tab,i,j)==tab[i]+sum(tab,i+1,j) axiomB1: \forall int tab[], int i; sum(tab,i,i) == 0 axiomB2: \forall int tab[], int i, int j; sum(tab,i,j) == tab[j] + sum(tab,i,j-1)

Axioms A1 and A2 behave well with Simplify's proof engine, while B1 and B2 make Simplify loop for ever.

Of course, a Simplify specialist would certainly find a rationale to explain that behaviour (and Prolog programmers will be familiar with logically equivalent definitions that are drastically different from the computational point of view!).

But from a software engineer standpoint, this kind of sensitivity is somehow unfortunate: the annotated C source files should be unique, whatever number of deduction tools are used in the subsequent stages of the verification process. The annotations should depend only on the software correctness properties to express and on human readability. One would like to have them not depending on tricky and obscure tool-feature issues.

Some lessons learnt

At this time, the experiment with Caduceus amounts nearly to one man.year effort and is still in progress.

The lessons learnt by mid-2005 drove deep modifications to Caduceus, especially on the C memory model that axiomatizes pointers' management. These modifications will be evaluated in 2006,.and we hope that by then many current limitations will be overcome.

We successfully made the proofs at unit level, and at the lower levels of the software integration hierarchy. More precisely, the call-graph of the software is a 11-level call tree. The main module is at, level 1 (the highest), and unit proofs are made at level 11 (the lowest). We managed to carry out proofs of the five properties for one parameter from level 11 to level 6. At levels higher than 6, the number, size and structure of the generated verification conditions were such that neither Simplify nor haRVey managed to prove them.

Let us give briefly some insight on why the higher the proof in the program hierarchy, the more complex were the generated verification conditions. It was mainly due to Caduceus' model and default assumptions on memory separation of global variables.

Memory separation had to be demonstrated for every couple of identically typed fields of global structure variables (used to store sensor measures). Basically these verification conditions consisted in proving that two pointers' base addresses and offsets were unequal. With more than 100 identically typed global structure fields at level 5, 4950 huge non tractable verification conditions were generated…

From level 11 to level 6, an average 60% of the verification conditions were discharged by means of automatic decision procedures. Some of the remaining unproved formulas were proved interactively with Coq. Some specialized and effective tactics were defined in Coq with the macro language to assess the possibility of speeding up these interactive proofs.

In the end, the feasibility of proving the five safety properties at the software boundaries (level 1) is not yet demonstrated. But the reason why we didn't manage to do so are well understood. LRI has undertaken major modifications of the memory model that should lead to smaller and fewer verification conditions at the expense of more sophisticated static analyses in Caduceus. It is expected that Simplify will have a lower failure rate on valid verification conditions generated by this forthcoming version of Caduceus, and that making proofs from levels 5 to 1 will become tractable.

We came up with a few other insights in the course of the experiment:

• So-called "ghost" variables turned out to be needed in Caduceus' annotation language: JML formulas are closed formulas whose only free variables are program variables.

For cyclic control programs that do not store in state variables some past values (that may be useless from the programming point of view but that are mandatory to formally specify some functional temporal properties), one needs to add modifiable "virtual program variables" at the annotation level to store these states and refer to them.

• Having the ability to use several automatic deduction tools to prove the verification conditions is a definite advantage: crossdemonstration of the same property by two different provers (which are magic "black boxes" from the software engineer point of view) increases the level of confidence one may have in these verification elementary steps. This kind of multiple demonstration approach is likely to be valuable in the future when arguing the case for using this tool suite in certification contexts (DO-178C more specifically).

To sum-up, we mainly faced scalability problems, but we expect to overcome them shortly with the next Caduceus release.

We have also uncovered some phenomena that greatly impede our verification productivity. The most important one is the great sensitivity of the success rate of automatic deduction tools to any change upward in the verification process. Any change in the annotation style (remember the sum(tab) example above), or in Caduceus/Why implementation, or in the automatic deduction tools, may cause some unforeseen regressions in the progress of the verification task: some proved verification conditions were no longer automatically provable while the code and annotations had remained unchanged.

Since proving a program is by far more time consuming than compiling or testing a program, some "robustness" is mandatory to have these techniques economically viable on large projects.

Towards IPEs : Integrated Proof Environments

Many issues already tackled in software development processes should be addressed as well in an industrial proof assistance environment dedicated to program verification.

It could be useful to consider that proof results (from decision procedures) or proof terms (from theorem proving assistants) should be seen as "binary files", or object files. In that way, files of annotated C instructions as well as proof scripts of interactive provers can be considered as source files. As for the provers (be they automatic or interactive), they woud play a role similar to that of compilers. Following this analogy, the need for versioning, configuration management, automatic reassembly of "binary objects" etc. should appear obvious in program proof development processes.

To elaborate a bit on that, we clearly felt the need for an integrated development environment (IDE) and related project management tools.

Some interesting developments along these lines have been made with Eclipse at INRIA Sophia: JACK (Java Applet Correctness Kit) [14] already provides some very useful functions such as traceability from proof obligations to annotations, proof validity management, computation of project progress statistics, impact analysis and incremental automatic reconstruction of "binary objects" triggered at high level (at the annotation level for instance).

Of course what turned out to be necessary in Java applets formal verification projects is also necessary for any other similar project on any other programming language. A Caveat and/or Caduceus Eclipse plug-in similar to JACK's will be developed once the scalability problems are solved.

It is likely that an industrially mature C correctness proof environment will also have to integrate other verification tools such as static analyzers, and perhaps even model checkers.

As mentioned before, on industrial size projects the \assigns annotations can't be manually provided by users. A static analyzer front-end has to generate them automatically. Some kinds of loop variants and invariants can also be automatically generated, thus sparing software engineers costly man.months of boring work. Software engineers should only be in charge of functional annotations and be released from manually setting annotations that could result from program control and data-flow analysis.

We wonder whether static analysis based preprocessors may not have to be introduced beyond mere assistance to setting non functional annotations.

Since we are facing a complexity issue at the higher levels of software integration, we wonder as well whether a code slicer would be helpful. To reduce the size of the verification conditions, one would generate them only on slices of the code, one slice per annotation.

Of course, such an approach has major drawbacks, especially if one envisions to use these techniques in D0178-compliant processes. We definitely hope that the new Caduceus memory model will solve the v.c size explosion problem. If not, we would need to resort to a program slicer.

We also had a look at other techniques to cope with software complexity, such as pre-processing the code by predicate abstraction techniques [START_REF] Ball | Automatic predicate abstraction of C programs[END_REF][7] and then using model checkers on the abstracted model.

We will investigate such techniques in case of failure of the theorem proving approach, or later as an additional mean of enhancing productivity in formal verification of hand-coded software, especially for temporal properties.

Conclusion

We have discussed an on-going attempt to prove about 350 safety properties on a 70+Kloc manually written C program, featuring many aliases and pointer issues.

We started with Caveat by 2003 and then moved to Caduceus by mid-2004, because its memory model could handle true aliases that Caveat could not at that time. It was the first release of Caduceus, which was still in its infancy.

Although we used two theorem provers, with great support by their development teams, and devoted a 1,5 m.y effort to the project at Dassault, we still did not manage to achieve our goal, 35 years after Hoare's seminal paper [START_REF] Hoare | An axiomatic basis for computer programming[END_REF],

We are still facing scalability issues. However we hope to solve them in the next few months thanks to major modifications in Caduceus' C memory model. We have obtained so far limited but encouraging results, therefore we remain confident in the feasibility of our project.

Once the five properties are proved at the main level for one parameter, we will face a productivity issue.

In some sense, the overall verification project consists in 70 similar verification sub-projects: the same five safety properties have to be proved on 70 different but similar parts of the program (one per voted sensor parameter). We would like not to spend 70 times the effort spent on the five first properties for the first parameter.

Failure rates and strategies of automated deduction tools, Coq tactics and tacticals like any other kind of automation tool, will have to be tuned carefully to take advantage of the structure and similarities of the code parts, and thus spare a significant amount of

Glossary

Figure 1 :

 1 Figure 1: The Caduceus/Why processing flow

verification effort. True feasibility will be established once the 350 properties over the 70 parameters are proved within a 1 to 3 m.y effort.

By then, the industrial maturity of the tools, their integration in some of our current processes and D0178 related issues will be at stake.

Acknowledgement

The authors are grateful to P. Baudin, J. Raguideau, D. Schoen, J.C Filliâtre and C. Marché for their reactivity and technical support for the last two years.


Alain Le Guennec

Bernard Dion

Bridging UML and Safety-Critical Software Development Environments

Keywords: Model-driven-design, formal-methods, UML, SCADE, safety-critical

This paper presents an approach combining the respective strengths of UML and SCADE to develop safety-critical systems. By using UML to specify the system's high-level requirements and architecture, and then SCADE to formally specify the software behavior, we provide a seamless flow from the initial requirement analysis phase down to the final integration on the target platform. This flow is based on the connection of UML tools with the SCADE environment, leveraging industry standards such as UML2, XMI, and DO-178B to provide a solution that is exactly tailored to the specific needs of safety critical projects.

Introduction

Overview of UML

The Unified Modeling Language (UML) is a widely adopted standard used to describe systems and software. It is a graphical notation that defines several kinds of diagrams, each providing a particular view on the system being specified:

• Use-case diagrams help capture high-level requirements.

• Sequence diagrams, by associating scenarios to requirements, help understand the interactions of the system with its environment, as well as inner interactions.

• Structure diagrams permit a hierarchical decomposition of the system in a hierarchy of connected "blocks" or sub-systems.

• Class diagrams define interfaces, classes and block types, in an object-oriented way.

• Package diagrams help organize the artifacts and spot the inter-dependencies.

• Statecharts and activity diagrams define behavior of active classes. However, when it comes to specifying behavior of safety-critical systems in UML, several problems arise:

• The actions and computations that are commonly associated with statecharts or operation bodies are often directly written in the target programming language, like C or C++, and hence fall outside of the scope of UML. The Action Semantics for UML, which is supposed to fill this need, is unfortunately not widely supported by current UML tools.

• Even without external code "in-lined" in UML, there still is no widely agreed-upon semantics for behavioral artifacts (although there are several proposals for a UML semantics), making them difficult to analyze formally without stringent restrictions.

• The execution framework implied by UML is based on asynchronous, queue-based, communications. Such a framework is not always appropriate for the targeted application domain. Moreover, it may imply dynamic allocation of memory for queues, unless they can be proven bounded.

• Behavioral specifications in UML allow for non-determinism and potentially unbounded computations, which again is an issue for safety-critical applications. In UML, an instance of an active class (let us call it a "block" in the following) represents a logical flow of control that reacts to its environment by pulling input messages out of its message queue one at a time, doing some computation (following the "run-tocompletion" principle) and sending one or several output message(s) to other instances as a response. 1.2 Overview of SCADE On the other hand, SCADE (the Safety Critical Application Development Environment) is both a notation and a toolset that was specifically developed to describe and implement safety critical systems for application domains such as aeronautics or automobile. The SCADE notation includes both block diagrams and safe state machines, as shown on the Figure 1 In SCADE, a Node (which we can also call a "block") performs logically atomic computations, providing deterministic output values corresponding to a given set of input values, according to the previous memorized state. The computation is often triggered by a periodic clock (although it need not be), after inputs are sampled from the environment and hold.

The SCADE toolset supports a model-driven paradigm in which the SCADE model is the software specification: tool is used to measure the coverage of the SCADE model with respect to a given requirements-based test suite. • The SCADE Suite Design Verifier (DV) supports corner bug detection and formal verification of safety requirements. In this paper, we will not further comment on the model coverage and the formal verification activities. The interested reader may refer to [START_REF] Bouali | Using Formal Verification in Real-Time Embedded Software Development[END_REF][START_REF] Dion | Efficient Development of Embedded Automotive Software with IEC 61508 Objectives using SCADE Drive[END_REF].

The C code generator is certified with respect to DO-178B level A (avionics) and IEC 61508 up to SIL 4 (other industrial domains, such as automotive or railways), thus providing a guarantee that the generated code is correct with respect to the model. 1.2 About combining UML and SCADE Notwithstanding the importance of precise and formal behavioral specifications as offered by SCADE, the high-level view offered by UML structure diagrams is often what is used in the early phases of a design when System Engineers are sketching the architecture of the application, assembling "blocks" that are connected together and that communicate through well-defined interfaces. The use of UML is appropriate at that level. There clearly is added value in combining UML and SCADE together, as each of them has strengths that the other can benefit of:

• UML is best used to describe the overall architecture of the application • SCADE is best used to formally describe the behavior of safety-critical software parts (note that less critical, or communication intensive sub-systems can remain in UML)

Therefore, a UML "block" and a SCADE "block" have some syntactical similarities, in that they both react to a set of inputs and provide a set of outputs in response. The sets of possible inputs and outputs form the overall "interface" of the block (note that we use interface in a quite broad way here, not to be confused with the actual interface syntactic construct of UML: Indeed the "interface" of a UML "block" can be composed of several provided or required UML interfaces). Another syntactic similarity is that UML "blocks" and SCADE "blocks" can be further decomposed into inter-connected sub-blocks. These syntactic similarities form the basis of the bridge between UML and SCADE. The biggest difference between UML and SCADE lies in how inputs and outputs relate to time. This "time factor" leads us to consider several situations:

• Purely safety-critical applications, where all software behavior is eventually specified with SCADE. • Hybrid applications, where some safetycritical sub-systems in SCADE communicate asynchronously with other sub-systems through a communication framework as commonly provided by UML environments.

Purely safety-critical applications in UML2 and SCADE

The primary goal of our bridge between UML and SCADE is to allow the designer to seamlessly refine a block defined in UML with behavior specified within SCADE, without ever having to manually duplicate (and maintain!) interface information at the boundary between the two languages. In UML on the other hand, the possible inputs and outputs of a block type are deduced from the features (attributes, signal-reception or operations) that the block provides or that the block requires, respectively. Features are usually exposed only through specific ports of the block, which represent interaction points between the block and its surrounding environment. The system is made of a controller block (called "cruise_control", of type "CruiseControl"), that we intend to specify in SCADE, and several sensors (on the left) and actuators (on the right). More precisely, left and right blocks represent software drivers managing the sensors/actuators and exposing the corresponding services to the controller block through well-defined ports. Features are usually grouped into interfaces. Therefore, a port has a set of provided interfaces and a set of required interfaces. A symmetric (or mirror) port located on the other side of an assembly connector provides the required interfaces of its peer port, and vice-versa. Provided and required interfaces together form a protocol for communication between two blocks through a pair of conjugated ports. For instance, the "On" port of block "cruise_control: CruiseControl" provides the "IButtonCB" interface. Its peer port is the "pressed" port of the "On: Button" block which requires the same "IButtonCB" interface.

Mapping rules

From UML blocks to SCADE blocks: For each class (block type) in UML that we want to refine in SCADE, there shall be a corresponding SCADE node with the same name and a related interface: Inputs and outputs of the SCADE block are derived from the UML block according to the following rules, organized according to the various kinds of features to be considered: UML signal reception: One possible feature of a UML interface is the reception of a specific signal. Communication with signals is the simplest case: When a signal reception for signal S belongs to an interface "I" provided by a port "p" of a block type "B", it means that instances of "B" can receive occurrences of "S" via "p". Considering the above discussion on the representation of "sporadic" signals in SCADE, if "B" is also the corresponding SCADE node, then it means that "B" possesses an input named "p_S_input" and typed by a structure with the following fields:

• The first field is a boolean flag that indicates the presence status of "S" for a given execution of "B".

• The following fields correspond to the parameter conveyed by signal "S", and therefore have corresponding types. If there are no parameters, the type is "bool" directly. Symmetrically, if interface "I" were a required interface of port "p", then SCADE node "B" would possess an output named "p_S_output" and typed as above. Note that there can be a reception for a same signal "S" in both provided or required interfaces of one or several ports of "B", hence the use of prefixes when naming I/Os in SCADE. For instance, the "On" port has a provided interface "IButtonCB" featuring one reception for signal "pressed", which maps to a SCADE input named "On_pressed", of type "bool":

CruiseControl On_pressed_input : bool UML operation call: An operation call is usually realized by two signals: A call signal, and a call return signal. When an operation "op" belongs to an interface provided by a port "p" of a block-type "B", the corresponding SCADE node "B" will have:

• An input "p_op_call" corresponding to the call signal, whose type is a structure with a first field being the boolean presence status and the following fields representing the in and in-out parameters of the operation.

• An output "p_op_result" corresponding to the return signal, whose type is also a structure with a first field being the boolean presence status, the remaining fields being the in-out, out and return parameters of the operation.

Symmetrically, if interface "I" were a required interface of port "p", then SCADE node "B" would possess an output with a default name of "p_op_call" for the call-signal and an input "p_op_result" for the return-signal, with types as specified previously. UML attribute: Starting with UML2, attributes are also allowed within interfaces (even though most UML1.x tools allowed for attributes in interfaces already). When an attribute/property "a" of type "T" belongs to an interface "I" provided by a port "p" of a block type "B", it means that instances of "B" "maintain information corresponding to the type and multiplicity of the property and facilitate retrieval and modification of that information". Therefore, an attribute potentially corresponds to two derived operations, the classical accessor and mutator operations. Read-only attributes only have an accessor. Some UML tools or UML profiles also allow for write-only attributes, with only a mutator. The I/Os of the corresponding SCADE nodes are derived as for operations calls to accessors and mutators, with the following subtle differences:

• Since the value of the attribute is provided "all the time", there is no need for an input call-signal (which is considered as implicit) nor for a boolean presence status in the return-signal for the accessor operation in SCADE. The SCADE node "B" will simply have an output "p_a_output" of type "T" (if "a" is not write-only).

• Since the mutator does never return any value, and is supposed to execute "instantly", there is not need for an output return-signal for the mutator. The SCADE node "B" will only have an input "p_a_input" of type "[bool, T]" (if "a" is not read-only). For instance, the "speed" port of CruiseControl has a required interface "ISpeed" featuring a read-only "speed" integer attribute (provided by the speed sensor), whose accessor maps to a SCADE input "speed_speed" of type "int". The "throttle" port has a required interface "IThrottle" featuring a "throttle" write-only integer attribute, whose mutator maps to a SCADE output "throttle_throttle" of type "[bool, int]": Handling of multiplicities: If a UML port has a multiplicity greater than one, it is replicated by expansion when mapped to SCADE (the multiplicity must of course be statically computable). Attributes with a multiplicity greater than one map to arrays. Note: The mapping strategy must remain flexible. Indeed, there are numerous profiles for UML that might impact what shall be considered an input or an output from a SCADE point of view. For example, some profiles such as UML/RT [START_REF] Selic | Using UML for Modeling Complex Real-Time Systems[END_REF] or SysML [START_REF]The SysML partners[END_REF] introduced the notion of directionality for attributes to simplify port and protocol specification. Ignoring such "semantic variation points" introduced by profile annotations would result in a SCADE model that would not reflect the intent of the UML model.

Taking block hierarchy into account

Although hierarchy can be expressed in SCADE directly, using SCADE block diagrams, there are at least two reasons why it can be useful to consider a mapping between structure diagrams of UML2 and SCADE block diagrams:

• UML offers good graphical structuring capabilities when doing pure structural decomposition (connectors and ports can convey several messages in a very compact graphical notation).

• When designing at system-level it is not always possible to foresee which subsystems will eventually be specified using SCADE and which won't. It would be a pity not reusing the existing inter-connection when doing the SCADE design in later stages of the development. Since this section focuses on purely safety-critical applications where the behavior of all blocks is specified with SCADE, we can discard the UML communication framework and map the block assemblies specified by UML structure diagrams directly into corresponding SCADE block diagrams. Note that it would be possible to generate textual SCADE equations representing block assemblies, instead of block diagrams (which are equations with presentation / layout information attached). However, graphical block diagrams have one major advantage: They are much easier to review. This is especially important in the context of certification (such as DO-178B), since the SCADE diagrams will be the reference for certification, not the UML diagrams. Indeed, neither the UML tools nor the UML/SCADE bridge are certified as DO-178B development tools).

The following mapping rules state how to transform this UML structure diagram into a corresponding SCADE block diagram directly: Parts: A UML part represents a nested sub-block. A part can also have a multiplicity ("1" by default). Parts of a block in UML are turned into calls to the SCADE nodes corresponding to the parts' respective block-types. If a part has a (static) multiplicity greater than one, it is expanded into as many node-calls. Connectors: Assembly connectors are used to link sub-blocks together through ports having symmetrical interfaces. Delegation connectors are used to link sub-blocks to their parent block, through ports having compatible interface. In SCADE, connectors are mapped into equations linking outputs of the source to inputs of the target, and vice-versa (a UML port can indeed be bi-directional). The mapping allows for connecting a port p1 of a block b1 to a port p2 of a block b2 if b1*p1 = b2*p2 when considering the multiplicities of parts and ports (the equations are replicated accordingly.)

Example: Let us assume that the CruiseControl block has been further refined within UML into subblocks, before it was decided to specify its inner working with SCADE. Figure 13 illustrates Note that SCADE blocks are not necessarily leaf blocks from a structure point of view. Some SCADE blocks can be further decomposed, using other SCADE blocks that may not exist in the UML model.

Behavioral modeling using data-flow block diagram:

The "ThrottleCmd" block appearing in Figure 13 and The "CruiseStateMgt" block is responsible for managing functional modes of the Cruise Control. SSMs offer several benefit over UML statecharts, such as handling of simultaneous events, of absent events, and fixed transition priorities, providing a good expressive power while keeping the behavior precise and deterministic at the same time:

Figure 1 :

 1 Figure 1: SCADE Block-diagrams and Safe State Machines

Figure 2 :

 2 Figure 2: Workflow of the SCADE toolset Verification activities are supported by a combination of three different tools: • The SCADE Suite Simulator supports interactive or batch simulation of a SCADE model, for both data flows and safe state machines. • The SCADE Suite Model Test Coverage (MTC) tool is used to measure the coverage of the SCADE model with respect to a given requirements-based test suite. • The SCADE Suite Design Verifier (DV) supportscorner bug detection and formal verification of safety requirements. In this paper, we will not further comment on the model coverage and the formal verification activities. The interested reader may refer to[START_REF] Bouali | Using Formal Verification in Real-Time Embedded Software Development[END_REF][START_REF] Dion | Efficient Development of Embedded Automotive Software with IEC 61508 Objectives using SCADE Drive[END_REF].

2 . 1

 21 Syntactic bridge at block interface In this section, we define a syntactic mapping between a block interface in UML and a block interface in SCADE. Thanks to this mapping, interfaces of blocks defined in UML can be directly reused within SCADE when specifying the behavior of said blocks. SCADE is based on the synchronous data-flow paradigm. Inputs and outputs of a SCADE block are typed data-flows. The type of a data-flow can be simple (bool, int, real) or structured (a structure or tuple made of a set of typed fields). In the special case when the first field of a structured input data-flow is of type bool (or when the input data-flow's type itself is bool), this boolean value can be used as a "signal presence status" in triggers of transitions in SCADE Safe State Machines. Symmetrically, when the first field of a structured output data-flow is of type bool (or when the output data-flow's type itself is bool), this boolean value represents the "signal presence status" of the output signal, set to true if and only if the signal is emitted during the execution of a SCADE node. Input or output flows associated with such a boolean presence status can be used to represent sporadic or transient signals which are considered only for some specific executions of the SCADE node.

Figure 3 :

 3 Figure 3: Overview of the CruiseControl system

Figure 4 :

 4 Figure 4: Interfaces involved in the CruiseControl

Figure 5 :

 5 Figure 5: A UML block viewed from SCADE

Figure 6 :

 6 Figure 6: I/Os for signal reception in UML

Figure 7 :

 7 Figure 7: I/Os for signal reception in SCADE

Figure 8 :

 8 Figure 8: I/Os for operation call in UML

Figure 9 :

 9 Figure 9: I/Os for operation call in SCADE

Figure 10 :Figure 11 :

 1011 Figure 10: I/Os for an attribute accessor in UML

Figure 12 :

 12 Figure 12: I/Os for attributes in SCADE

Figure 14

 14 Figure 13: Internal structure of the CruiseControl block Figure 14 is a SCADE block diagram corresponding to the UML structure diagram of Figure 13:

Figure 14 :

 14 Figure 14: Cruise Control SCADE block diagram 2.4 Completing the behavioral model within SCADE After a first level of structure has been mapped into SCADE, it is now possible to further refine the various SCADE blocks already defined, using either data-flow block diagrams, or Safe State Machines.Note that SCADE blocks are not necessarily leaf blocks from a structure point of view. Some SCADE blocks can be further decomposed, using other SCADE blocks that may not exist in the UML model.

Figure 15 :Figure 16 :Figure 17 :

 151617 Figure 15: Behavior of the ThrottleCmd blockThe "ThrottleCmd" block (defined in Figure16) refers to another SCADE block called "SaturateThrottle".

Figure 18 :

 18 Figure18: Behavior of the CruiseStateMgt SSM block 2.5 Considerations for an iterative and incremental development process with UML and SCADE More often than not, the UML part of the specification will not be definitive, and might undergo significant changes even after work has begun specifying behavior within SCADE. It was therefore of the utmost importance that the UML/SCADE bridge allow for incremental synchronization between the UML and the SCADE models. Changes made in UML can be merged without losing work.

Hybrid Applications

Principles

In hybrid applications, a sub-system whose behavior is specified with SCADE is connected to other subsystems (not necessarily specified with SCADE) through the communication framework as prescribed by UML. The behavior of the blocks has to conform to the run-to-completion scheme of UML and blocks have to use message queues for their communications. Since some blocks in the system are done in SCADE, it is important to reconcile the asynchronous nature of the framework with the synchronous nature of individual SCADE nodes. Our work is inspired of existing work [START_REF] Camus | Combining SDL with Synchronous Data Flow Modeling for Distributed Control Systems[END_REF] done in the context of SDL instead of UML. The most natural way to achieve this integration is for the SCADE block to consider some specific input signal(s) as a special "clock" signal. Such an input clock signal will not be turned into a boolean input data-flow of the SCADE node. Instead, reception of a clock signal (only) will trigger the actual execution of the SCADE node. Other incoming messages are also processed and removed from the queue: They are "combined" upon arrival in the input vector of the SCADE node, which summarizes all inputs the node will consider altogether at once when executed later. The principles are illustrated in Figure 19 below. Whereas in the previous "purely safety-critical" case a UML structure diagram could be considered directly as an extended view of a plain SCADE block diagram (with a one-to-one mapping of block interfaces, parts and connectors), here a <<SCADE>> UML block on a UML structure diagram is better considered as a surrogate/capsule/wrapper for an encapsulated SCADE node. There is no more a complete one-to-one mapping of interfaces (because of clock signals), and the connection semantics can no more be considered as "plain synchronous data-flows" (because the framework uses message queues of unknown size a priori). The clock signal can be external to the <<SCADE>> UML block (it is an input of the block in UML) or internal to the <<SCADE>> UML block (through a periodic timer for instance). The wrapping of SCADE nodes within <<SCADE>> UML blocks is at the same time conceptual (it describes the semantics of the integration) and practical (it leads to the generation of "glue" code for code-level integration, allowing for co-execution/cosimulation of the whole system). The principles explained on Figure 19 give some hints about the code-generation algorithm that will produce the wrappers necessary to integrate the C code generated by the qualified SCADE code generator KCG into the UML run-time framework provided by UML tool vendors (usually in C or C++). We are currently designing a new wrapper codegenerator that implements the idea presented here.

Conclusion

We have presented a complete workflow that combines the respective strengths of UML and SCADE to tackle large-scale safety-critical system development. The high-level structuring capabilities of UML coupled with the precision and expressive power of SCADE behavioral descriptions help deliver clear and correct-by-construction software artifacts. The verification tools part of the SCADE suite can be used to prove the SCADE parts of the system correct and to generate certifiable C code from the specifications. The code-level integration between UML and SCADE will allow to co-simulate hybrid applications, therefore helping spot problems within that kind of applications as early as possible.

Glossary


Frédéric Boniol

Virginie Wiels

Emmanuel Ledinot

Experiences in using model checking to verify real time properties of a landing gear control system

Keywords:

This paper presents experiences in using several model checking tools to verify properties of a critical real time embedded system. The tools we tested are Lesar, SMV, Prover Plug In for SCADE and Uppaal. The application is the landing gear control system of a military aircraft, developed by Dassault Aviation. The property to be verified states that the gear must be down in at most 14 seconds. Results (success and verification time) depend a lot on the way time is handled by the verification tools.

Introduction

Embedded critical systems need to be validated very thoroughly; it usually results in very long and onerous test phases. Formal techniques, fin particular formal specification languages and associated proof tools, could be an advantageous alternative, or at least a good complement and allow a significative reduction of test phases. However, for these techniques to be used in practice, one issue to consider is their efficiency on complex industrial systems.

This paper presents experiences in using model checking tools to verify a real time property of a landing gear control system implemented by Dassault Aviation. The system was originally described in Esterel and included a control software and physical components modelling. A first attempt was made at validating the system against a set of properties using Esterel model checker TiGeR, but some properties were not verified. It was thus decided to test other model checking tools: tools associated to Lustre (Prover Plug In, Lesar), SMV (because we could use an automatic translation from Lustre to SMV), and Uppaal (for the ability to model the physical components in a more realistic way using timed automata).

In order to obtain a finer evaluation of the considered tools, we have defined several versions of the verification task of growing complexity, by considering

• three versions of the system,

• two versions of the property,

• two different sets of hypotheses.

It is important to note that our objective is not to do a classical benchmark of verification tools, but to evaluate the usability of such tools in an industrial context. Our starting point is a specification written by industrial designers (in Esterel) and our concern in the translation process is to stay as close as possible to this original specification, thus forbidding verification oriented optimisations.

Section 2 describes the case study. Section 3 presents the experimentation approach. Sections 4 and 5 are devoted to experimentations. In section 6, we synthesize results and try to analyze them. Finally, section 7 sketches some avenues of future work.

Case study

The case study is the landing gear control system of a military aircraft. This system has to satisfy a list of requirements such as "the gear should not be retracted without pilot order", "the gear should not be retracted when the aircraft is on ground even if pilot orders it", etc. Among these properties, only those requiring that gears react in a given time will be considered in this study, because they are the most difficult to verify.

Description of the system

General description. The landing system is in charge of manoevering landing gears and associated doors. The system is controlled digitally in nominal mode and analogically in emergency mode. The system is composed of three gears: front, left and right gears. Each gear has got a landing gear uplock box and a door with two latching boxes.

Gears and doors are manoevered by hydraulical jacks. Hydraulical power is provided by a command unit that consists of • a set of actuators: solenoid valve to isolate the emergency hydraulical system, electrovalves to open and close doors, to let down and to retract gears;

• a set of sensors giving the current state of different parts of the system: position of landing gear actuating cylinder, of lock actuators, state of landing gear shock absorbers, state of hydraulical system, etc.

To command the retraction and outgoing of gears, the pilot has got a set of buttons with two positions (up and down) and a set of lights giving the current position of gears and doors.

When the command line is working (we will only consider this case in this study), the landing system reacts to the pilot orders by actioning or inhibiting the electrovalves of the appropriated jacks. The outgoing of gears is decomposed in a sequence of elementary actions: In the same way, the retraction of gears is decomposed in a sequence of elementary actions: Because of hydraulical constraints, a given timing must exist between stimulation and stimulation stop of the solenoid valves and electrovalves. Moreover, the previous sequences should be interruptible by counter orders (a retraction order occurs during the let down sequence and conversely).

A general description of the system is given in figure 1.

The control software.

This software is in charge of controlling gears and doors in nominal mode. It is part of a retroaction loop with the physical system, and produces commands for the distribution elements of the hydraulical system from the sensors values and from the pilot orders.

The input of the software are:

• command buttons values (up or down),

• position of the six doors locks,

• position of the three actuating cylinders,

• position of the three landing gears locks,

• state of the drag struts,

• state of shock absorbers,

• an oil pressure switch giving the pressure of the hydraulical system after the isolating solenoid valve.

The output of the software are:

• commands to start and stop stimulation of the electrovalves and solenoid valves,

• a set of warnings for the pilot in case of bad functioning or non response of mechanical components.

The control software consists in a set of specialised functions:

• a monitoring function for gears and doors, that signals the landing system faulty if it detects incoherences,

• a command function that implements the sequences of outgoing and retraction of gears. This function directly controls the mechanical components. It is decomposed into a function that computes stimulation commands for each component and functions to manage the commands emission (management of the timing constraints).

• a monitoring function to verify that the system reacts correctly and to control the functional and temporal coherence of the orders. As faults are not taken into account in our study, we do not consider this function in the following.

All the functions included in the control system are implemented by periodic and sequential processes executed every 40ms.

Requirements / Properties

The properties we want to prove on the system are the following (we suppose that there is no fault):

• if the landing gear command button has been DOWN for 14 seconds, then the gears will be down in less than 14 seconds;

0 0 0 1 1 1 0 0 1 1 0 0 1 1

Figure 1. General description of the system

• if the landing gear command button has been UP for 14 seconds, then the gears will be retracted in less than 14 seconds.

The two properties are very similar, we will only consider the first one in the following. This property characterizes a behaviour of the control software together with the physical system to be controlled, i.e. a model of the real time behaviour of jacks, electrovalves, gears, doors, hydraulical actuators, etc. These models must take into account timings. For example an hydraulical power is operational only after a given time. We will see that these real time constraints are partly responsible for the combinatorial explosion that will prevent verification in some cases.

Experimentation approach

In this section we present the starting point of our study (a first experience made by Dassault), the verification approach and the methodology we adopted to be able to achieve a fine evaluation of the tools.

Starting point

The first attempt to prove the property was made in 1995 by Dassault Aviation with the TiGeR tool (From CMA, Sophia Antipolis). This tool was essentially a BDD library aimed at verifying and optimising electronic sequential circuits. The Esterel compiler translates programs into sequential circuits that can then be verified with TiGeR [START_REF] Berry | The foundations of esterel[END_REF][START_REF] Esterel | [END_REF].

TiGeR proceeds in two steps: it first computes the BDD representing all accessible states, then it verifies the property on this diagram. The first step is crucial, computed diagrams can reach prohibitive sizes. For the verification of the property on the landing system, this first step could not be achieved for lack of memory. Experiences were made on a Sun Sparc with 128Mb at Dassault and on a DEC Alpha with 500Mb at CMA, but both attempts were unsuccessful.

Verification approach

After this first experience without result, it was decided to test other model checkers: on one hand tools associated to the Lustre language [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF], on the other hand a real time tool based on timed automata [START_REF] Alur | A theory of timed automata[END_REF]. Lustre and Esterel use a discrete time model that necessitates a sampling of the behaviour of the system and particularly of the physical components. This sampling leads to an explosion of the number of states that is problematic for the verification tools. This is one of the reasons why we chose to also experiment a tool based on continuous time that does not need sampling. We expected a more realistic and sampling independent specification of the physical components. The tools that were tested are thus:

• Prover Plug In for SCADE (Prover Technology) [START_REF]Prover Technology[END_REF],

• Lesar (VERIMAG) [START_REF] Halbwachs | Programming and verifying real-time systems by means of the synchronous data-flow programming language lustre[END_REF][START_REF] Ratel | Définition et réalisation d'un outil de vérification formelle de programmes LUSTRE : le système LESAR[END_REF]9],

• SMV (Cadence Berkeley Labs) [START_REF] Mcmillan | The SMV language[END_REF][START_REF] Mcmillan | Getting started with SMV[END_REF][START_REF] Smv | [END_REF],

• UPPAAL (University of Aalborg) [START_REF] Larsen | Uppaal in a nutshell[END_REF]16].

The initial specification, provided by Dassault, included

• the description of the control system for the three landing gears-doors,

• the description of the physical components of the system,

• the properties to be verified.

These elements were specified in Esterel. We had to translate these specifications to Lustre and to UPPAAL. Both translations were done manually. The resulting specification in UPPAAL is partly discrete (the control system is specified by a discrete automaton) and partly continuous (the physical components and the properties are specified by timed automata). Figure 2 synthesizes the verification approach.

All the source files for the specifications and properties can be found at http://www.cert.fr/francais/deri/boniol/landing gear/.

Methodology for the experimentations

In order to be able to study tool robustness more finely, we have defined several versions of the case study of growing complexity.

As the system is composed of three similar sets of gears-doors, a first simplification consisted in building

• a V1 version with only one gear-door set,

• a V2 version with two gear-door sets,

• a V3 version with the three gear-door sets.

A second simplification was applied on the property. The property states that gears must be down and doors must be closed at the latest 14 seconds after the pilot order (if there is no fault and no counter order) (P2). As combinatorial explosion stems partly from timings occurring in the system and the property, we proposed to divide the timing by 10 (in the system and in the property) and thus to prove that gears are down and doors are closed 1,4 seconds after the pilot order (P1).

Finally a third simplification concerns the verification hypotheses. The general case (the most complex) only suppose absence of fault (H2). We tried to decrease verification complexity by studying a more restrictive case constraining the initial state of the system and the pilot's behaviour (H1):

• initially, gears are out and doors are closed,

• gears are always relaxed,

Figure 2. Verification approach

• the pilot's behaviour is the following: order to retract gears at time t then order to let down gears at time t', for any t < t'.

These three ways of simplification define 12 cases depending on the version of the system (V1,V2,V3), the version of the property (P1,P2) and the hypothesis (H1,H2) considered. The 12 cases, from the simplest <V1,P1,H1> to the most complex <V3,P2,H2>, allowed to determine more precisely the limits of each tool with respect to growing complexity of the problem.

All experiments described below were done on a Sun ultra 10 workstation with 1Go of memory.

Verification tools associated to Lustre

Lustre is a synchronous data flow language, we will not describe the language here, the interested reader is referred to [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF].

Three tools have been experimented: PPI [START_REF]Prover Technology[END_REF] and Lesar [9] that work directly on Lustre specifications, and SMV [START_REF] Smv | [END_REF] that has its own specification language but a translator from Lustre to SMV exists and was used to experiment the tool.

The size of the Lustre specification depends on the version of the system and the version of the property.

PPI (Prover Technology)

Prover Plug In is a verifier integrated into SCADE (an environment for the development of critical embedded systems, based in the Lustre language and that includes a graphical editor, a simulator and a qualified C code generator) [START_REF]SCADE[END_REF].

PPI did not give any positive result, even in the simplest case <V1,P1,H1>. However, we obtained indirect results using a slightly different strategy. Two proof strategies exist in the tool: prove to be used when one thinks the property is true and wants to prove it formally; and debug to be used first, when one is not sure about the validity of the property or even its correct expression. The debug strategy is usually very quick in finding counter-examples when they exist. We thus decided to use the debug strategy with a too short delay for the property. This approach gave interesting results. For version V1 and for a delay strictly smaller than 1,08 second (27 cycles of 40 ms), PPI immediately found a counter-example to the property. For delays greater or equal to 1,08 second, PPI gave no result (neither with prove strategy, nor with debug strategy). For versions V2 and V3, counter-examples were also found quite quickly for all delays strictly smaller than 1,44 second (36 cycles of 40 ms). Time to find counterexamples are given in the following array: P1,H2 V1, 26 cycles 4 s V2, 35 cycles 21 s V3, 35 cycles 43 s

Lesar (Verimag)

The version of the tool that was used dates from 1999.

Lesar is a model checker for Lustre developed at Verimag. It succeeded in proving the property for versions V1 and V2 of the system, but not for version V3 (after 15 days of computation). Detailed results are given in table 1.

The memory used by Lesar never exceeded 120Mo even in the V3 case.

SMV (Cadence Berkeley Labs)

The version of the tool that was used dates from march 1999.

SMV is a model checker developed at Cadence Berkeley Labs. It has its own specification language but a translator from Lustre to SMV exists. SMV was the most efficient tool, it succeeded in proving the property in all cases. Detailed results are given in table 2.

Memory used by SMV in the case <V3,P2,H2> is 415 Mo, but only 129 Mo in the case <V3,P1,H2>, when timing are shorter. This confirms our hypothesis that the combinatorial explosion is partly caused by timings occurring in the system and also in the property. Remark: cases <V1,P1,H2> and <V1,P2,H2> could not be tested because of a bug of the Lustre to SMV translator.

Verification using timed automata and Uppaal [16]

5.1 Methodology for the translation into timed automata A quick analysis of the case study and its specification shows that timings occur essentially in the physical components models. The idea here is to specify these models using timed automata. The control software will be implemented onboard the aircraft by discrete periodic processes. The translation approach was thus:

• to specify the control system with discrete automata,

• to describe the periodic activation (every 40ms) of the control system by a timed automaton sending "tick" signals,

• to specify the physical components behaviour using timed automata,

• to build the global specification by composition of all the automata,

• to express the property using an observer automaton and a CTL formula.

Moreover, we have to describe the automata environment (emitting the input signals). The pilot and the hypotheses on his behaviour was thus also represented by a timed automaton.

The translation approach is synthesized on figure 3.

Verification with Uppaal

The version of the tool that was used dates from march 2004 (V3.4.5).

Uppaal succeeded for version V1 in the general case (hypothesis H2). For the two more complex versions V2 and V3, Uppaal only succeeded with hypothesis H1 (constraining the pilot's behaviour). In the other cases, failure was due to lack of memory. Detailed results are given table 3.

Synthesis and analysis

Before analyzing this experimentation and the performances of each tool, it is necessary to recall the limits of this experience. The system we considered, that is to say the landing gear control system and its physical environment, is modelled using reactive processes including only boolean flows or signals. The property we try to verify on this sytem deals with the real time behaviour of the system. The scope of the analysis is thus limited to this kind of system and property. Moreover, much better results might have been obtained by optimising the specifications with respect to tools (particularly Uppaal). However, as said in the introduction, our objective is to know whether such tools could be used in an industrial context, where no knowledge of the verification techniques implemented in the tools can be assumed.

PPI

As seen in section 4.1, PPI did not give any positive result, even in the simplest case <V1,P1,H1>. An explanation may be found in the way the tool deals with Lustre specifications. Proofs are built by induction and the number of induction steps directly depends on the length of the delays (i.e. the depth of the "pre" statements in the Lustre specification). The landing gear case study uses a lot of delays and that could explain the bad results obtained by PPI.

To confirm this diagnosis, we made a complementary experience on an untimed property. The property (P3) we tried to verify is the following: "it is never the case that the gear retraction solenoid is excited and that the door is not open." Results using PPI are given in the following array. These results show that PPI can be very efficient (more than Lesar) on non real time properties, even if the considered specification of the system and of the environment still contains long delays. Other experimentations have also been successful on non real time properties in another application context [START_REF] Laurent | Using formal verification techniques to reduce simulation and test effort[END_REF].

Another result concerning PPI is that even if it failed to prove the property, it was very efficient in finding counter examples when the property was not verified. This was possible because PPI provides two different verification strategies: "prove" strategy to ensure that a property is always verified, and "debug" strategy to quickly build a counter example of the property.

Consequently, even if PPI was not able to prove the property on the system, we think it could be an efficient tool to help in designing and debugging a system.

Lesar and SMV

Lesar and SMV are both symbolic model checkers. Lesar is however an academic tool while SMV is a more industrial and performance-oriented tool. We will thus essentially focus our analysis on SMV, keeping in mind that the results obtained with Lesar confirm the good performances of symbolic model checkers for this particular experimentation.

SMV was the only tool to succeed in all steps of the experimentation, even the most complex ones. Two remarks have to be made.

Firstly, memory used by SMV is 415 Mb in the most complex case (<V3,P2,H2>), but is only 129 Mb in the case <V3,P1,H2>, i.e. when we only diminish delay values. This confirms that combinatorial explosion is essentially due to delays in the system and in the property.

Secondly, the evolution of SMV performances with respect to evolution of complexity in the system and in the property (from <V1,P1,H1> to <V3,P2,H2>) is surprising. For example, replacing V2 (two gears-doors sets) by V3 (three gears-doors sets) does not induce an augmentation of verification time. In the same way, replacing H1 by H2 does not lead to a significative growth in verification time. It seems that SMV is able to exploit the characteristics of the system, like its symmetry, to improve the verification performances.

Uppaal

Combinatorial explosion observed with PPI but also with SMV (growing memory size) is essentially due to the kind of property we considered. A time frame of up to 14 seconds after the pilot order needs to be explored for the property to be verified. Esterel and Lustre deal with discrete time, so we have to express the property using the activation period of the system (40 ms) which leads to consider at least 350 consecutive steps of the system. PPI, which works by unfolding of the system on the necessary number of steps is thus handicapped by this kind of property. This discretization of delays is also problematic for symbolic model checkers because of the size of memory used. We made an attempt at circumventing this issue by using a timed formalism that does not necessitate a sampling of the system. Uppaal was chosen to model the system using timed automata.

Unfortunately, Uppaal was not able to verify the system <V2,P1,H2> (two gears without hypothesis on the pilot's behaviour). It nevertheless succeeded in verifying the property when the possible behaviour of the pilot was restricted (<V2,P2,H1>). Memory used by Uppaal in this case is 834 Mb and verification time is 1h56mn, while in case <V2,P1,H1> memory used was 124 Mb and time 2mn. We thus observe the same explosion phenomenon than with SMV, again due to delays in the property. A timed formalism did not allow the reduction of this phenomenon we had expected.

One reason of this failure may be found in the discretization of the control system. This system is activated every 40 ms, this implies that the clock domain will also be discretized. In other words, the sampling of the control part the system implies a sampling of the physical components even if they are described using timed automata. Advantage of using dense time is thus lost. This result leads us to believe that such a formalism and such a tool might not be adapted to low levels of the development cycle (as in our experiment where we used Uppaal to validate a model very close to what will be embedded in the flight computers) and that it would be much more useful at the specification level to verify abstract specifications or help in dimensioning the system. This hypothesis however needs to be confronted with other examples.

The last lesson from this experimentation concerns timed automata formalism. It is a graphical formalism and this is an advantage, in particular it was fairly easy to define scenario classes (for the pilot's behaviour) as timed automata. These scenarios could be obtained from Message Sequence Charts or sequence diagrams. They provide a means to partition the system and its environment into classes of scenarios covering the whole system's behaviour.

Future work

The main possibility to go on with this experimentation would be to explore compositional verification. The three sets of gears and doors are identical, the intuitive idea would be to try to verify the property on each set separately and then to conclude that the property is verified on the whole system. In [START_REF] Halbwachs | Synchronous observer and the verification of reactive systems[END_REF], a way to implement compositional verification on Lustre specification is given. SMV also provides modular verification capabilities that were not explored during this experimentation but could be very interesting.

This idea of compositional verification must however be studied thoroughly and experimented carefully. The intuitive idea about the decompositon of the system is not so simple in practice, for several reasons. The three sets of gears and doors are not isolated from each other, there are several interactions to take into account. Moreover, the system has not been designed in a modular way: the control system does not compute three commands for each set, but computes one global command with respect to the state of each gear and each door.

Another example forces us to be prudent with the idea of compositional verification. In [START_REF] Westhead | Verification of embedded systems using synchronous observers[END_REF], on a similar kind of system (landing gear control system also), modular verification of properties was less efficient than global verification. The global automaton obtained by synchronised product of automata from each process composing the system was of smaller size than the automata of the component processes.

1 .

 1 stimulation of the solenoid isolating the command unit, 2. stimulation of the door opening solenoid, 3. once the doors are opened, stimulation of the gear outgoing solenoid, 4. once the gears are locked down, stop the stimulation of the gear outgoing solenoid and stimulation of the door closure solenoid, 5. once the doors are closed, stop the stimulation of the door closure solenoid, 6. and finally stop the isolating electrovalve.

Table 1 . Lustre-Lesar vrification results

 1

	P3, H2
	V1 3.2s
	V2 7.4s
	V3 8.5s
	For the same property, results obtained by Lesar are as
	followed.
	P3, H2
	V1 4s
	V2 1mn 5s
	V3 1h 9mn 46s

Table 2 . Lustre-SMV vrification results

 2

		Dassault Aviation description
	control software Esterel	Properties PLTL + Esterel	physical components modelling Esterel
		input
		generation
	h=40 tick! h:=0	discrete automaton control software	properties CTL + timed automata	physical components modelling timed automata
		Figure 3. Translation approach
	P1,H1	P1,H2	P2,H1	P2,H2
	V1 1mn 21s (53 Mb)	15mn (184 Mb) 1h 05mn (342 Mb) 5h 57min (761 Mb)
	V2 2mn 24s (124 Mb) no result	1h 56mn (834 Mb) no result
	V3 3mn 8s (176 Mb)	no result	2h 23mn (1,15 Gb) no result

Table 3 . Uppaal vrification results

 3