Marius Bozga

Laurent Mounier

Verimag David

Lesens Eads

Launch Vehicles

Model Checking Ariane-5 Flight Program

This paper reports a veri cation experiment carried out on a re-engineered description of a part of Ariane-5 Flight Program. This is the embedded software which solely controls the Ariane-5 launcher during its ight, from the ground, through the atmosphere and up to the nal orbit.

In this case study, the Sdl language was used to describe the main functional behavior of the ight program including the most relevant actions and their associated timing constraints, which are necessary to ensure the correct operation of the launcher. This description abstracts away both complex functionalities such as navigation and control algorithms and also implementation details, such as speci c hardware and operating system dependencies.

Several properties could then be veri ed on this speci cation using the IF toolbox, an open validation platform developed at Verimag for real-time asynchronous systems. The results obtained con rm that model-checking and complementary techniques (such as static analysis or abstraction), combined within a set of methodological guidelines, could be successfully applied to the validation of large real-time embedded systems.

Introduction

It is now well admitted that the increasing importance of software within critical embedded systems will necessarily in uence the techniques used to produce such systems. In particular, embedded systems tend to become more and more complex, economic constraints always impose shorter development times, and classical testing procedures are clearly not exhaustive enough to guarantee a su cient level of reliability at a reasonable cost. All these factors motivate the introduction of new techniques within the software development process, able to better take into account the semantic aspects of the application from the earliest design stages. Formal methods are an example of such techniques. They consist in producing some intermediate descriptions (or speci cations) of the system under development using well-de ned and unambiguous formalisms. Then from speci cations it becomes automatically possible either to verify at early stages some expected high-level properties, or to generate executable code, or even to produce test sequences to be executed on the nal system implementation. In fact, although limited in the past to small academic examples, formal methods seem now mature enough to be used within an industrial context, even for large scale applications. In particular, this evolution is facilitated by two important factors: the existence of well accepted speci cation formalisms, some of them being based on international standards like Lotos 16], Sdl 17] or Uml 19]; the support of validation tools, either commercial (e.g, Tau 1], ObjectGeode 20] or StateMate 15]) or academic ones (e.g, Spin 14], Smv 18], Cadp 10]) able to handle large applications and providing many useful validation facilities (from interactive simulation to exhaustive veri cation and automatic test case generation).

In this context, this work was initiated by Eads Launch Vehicles to better evaluate the maturity and applicability of existing formal validation techniques, both from the description language and from the validation tools point of view. More precisely, it consisted in formally specifying some parts of an existing software, on a re-engineering basis, and to try to verify some critical properties on this speci cation. The software that has been chosen is the Ariane-5 Flight Program. This is the embedded software which solely controls the Ariane-5 launcher during its ight, from the ground, through the atmosphere, and up to the nal orbit. The experiment was carried out using [START_REF] Bozga | State Space Reduction based on Live Variables Analysis[END_REF], a validation environment developed at Verimag. This environment relies on a general intermediate format for timed asynchronous systems, allowing to connect the ObjectGeode Sdl commercial toolset to several academic veri cation tools, including Cadp and Spin. Together, these tools o er e cient veri cation facilities such as on-the-y model-checking, partial order reductions, or static analysis optimizations. Nevertheless, even if recent researches have considerably improved the tool e ciency, it is still di cult to apply them on concrete case studies. For example, our Ariane-5 Flight Program speci cation is about 4000 lines of Sdl, which makes clearly impossible to verify it following a strict push-button approach. From this point of view, this experiment give us some hints for a veri cation methodology of large Sdl systems, taking into account most of advanced tools functionalities. The results obtained illustrate the increasing maturity of model-checking techniques to face industrial applications. The paper is structured as follows. First, we brie y present in section 2 the IF validation environment. In section 3 we describe the Ariane-5 Flight Program. We begin with an informal overview of the program, then we continue with some deeper insights about the formal Sdl speci cation, as well as its surrounding environment and functional requirements. Finally, in section 4 we point out the concrete veri cation results obtained, following a set of general methodological guidelines. Some concluding remarks and perspectives are given in section 5.

IF Toolbox

The veri cation tools we used during this experiment are connected through the IF validation environment 7], which is developed at Verimag. This environment relies on a general intermediate format for timed asynchronous systems, the IF language 8], and integrates several components operating at di erent levels of abstraction.

The IF language

In IF, a system is expressed as a set of parallel processes communicating either asynchronously through a set of bu ers, or synchronously through a set of gates. Processes are based on timed automata with urgencies 4], extended with discrete variables. Process transitions are guarded commands, triggered by synchronous/asynchronous inputs, and performing asynchronous outputs, variable assignments, or clock settings. Communication bu ers have various queuing policies ( fo, stack, bag, etc.), they can be bounded or unbounded, reliable or lossy, and delayed or not. An important feature of the IF language is to provide a well-de ned real-time semantics of asynchronous systems by means of transition urgencies. More precisely, an urgency attribute is associated to each process transition in order to de ne its priority over time progress during simulation: eager transitions are assumed to be executed as soon as possible: time does not progress as long as an eager transition is enabled; lazy transitions are never urgent: enabled lazy transitions do not disable time progress; delayable transitions are a combination of eager and lazy transitions: they are enabled within a time interval, time may progress within this interval, and the transition becomes urgent when its upper bound is reached.

By o ering a precise control of time during system simulation, the urgency mechanism provides a exible way to specify the real-time constraints associated with each action performed. In particular the use of eager transitions allows to guarantee an immediate response of the system to some critical events (like a timer expiration), whereas lazy and delayable transitions allow to introduce some time non-determinism in the handling of partially constrained events.

The IF validation environment

The IF validation environment provides a complete veri cation chain consisting in several components organized into three levels of system representation (see gure 1).

The speci cation level components. This level corresponds to the initial program description, expressed for instance in a high-level speci cation language. The formalism we considered here is Sdl, and we used the The semantic level components. This level gives access to the labeled transition system (Lts) representing the exhaustive behaviour of the IF system. This Lts is obtained by running a simulation program, generated by the if2c component. The simulation program integrates several advanced veri cation techniques like partial order reduction and on-they model-checking. The resulting Lts can be used within Cadp 10], a veri cation toolset developed by the Vasy team of Inria Rhône-Alpes and Verimag. In particular we intensively used in this experiment two components of this toolset, Aldebaran, a bisimulation based minimisation/comparison tool, and Evaluator, an alternating-free -calculus modelchecker. Each of these tools are able to compute diagnostic sequences at the Lts level that can be translated back into Msc to be observed at the speci cation level. Other components like Kronos 22] (a Timed-Ctl model-checker) and Tgv 11] are also applicable at this level.

Ariane 5 Flight Program

In order to understand the functionalities of the ight program, we begin the presentation with a short informal overview of the whole Ariane-5 ight1 . Then, we present how the ight program was formalised using Sdl. We detail the main design choices and the abstraction of the environment. Meantime, we try to illustrate both the bene ts and the limitations of using Sdl as a description language for this kind of systems. We end the section by presenting the set of safety requirements needed in order to ensure the well-functioning of the ight program.

Overview

An Ariane-5 launch begins with ignition of the main stage engine (epc -Etage Principal Cryotechnique). Upon con rmation that it is operating properly, the two solid booster stages (eap -Etage Acc el erateur a Poudre) are ignited to achieve lift-o . After burn-out, the two solid boosters (eap) are jettisoned and Ariane-5 continues its ight through the upper atmosphere propelled only by the cryogenic main stage (epc). The fairing is jettisoned too, as soon as the atmosphere is thin enough for the satellites not to need protection. The main stage is rendered inert immediately upon shut-down. The launch trajectory is designed to ensure that the stages fall back safely into the ocean. The storable propellant stage (eps -Etage a Propergol Stockable) takes over to place the geostationary satellites in orbit. Payload separation and attitudinal positioning begin as soon as the launcher's upper section reaches the corresponding orbit. Ariane-5's missions ends 40 minutes after the rst ignition command. A nal task remains to be performed -that of passivation. This essentially involves emptying the tanks completely to prevent an explosion that would break the propellant stage into pieces. The ight program entirely controls the launcher, without any human interaction, beginning 6 minutes 30 seconds before lift-o , and ending 40 minutes later, when the launcher terminates its mission.

Formal speci cation

In order to build a formal speci cation, the Sdl 17] language was preferred for this case study among other formalisms for several reasons. First of all, it is based on asynchronous communicating nite-state machines. Thus, it is particularly adequate to describe, at some level of abstraction, the whole ight program as a collection of processes asynchronously interacting each other. In addition, Sdl provides an explicit notion of time and some corresponding real-time primitives. Since there exists an automatic translation from Sdl to IF, it becomes possible to enforce the Sdl time semantics using urgencies in order to express all the required timing constraints associated with the ight program components. Finally, Sdl is currently supported by several integrated environments such as ObjectGeode 20] and Tau 1], which makes it very attractive from a development point of view. As explained in the informal description, the main functionalities of the ight program are the following:

Ground

ight control, which consists in navigation, guidance and control algorithms, ight regulation, which consists in observation and control of various components of the propulsion stages (engines ignition and extinction, boosters ignition, etc), ight con guration, which consists in managing changes of launcher components (stage separation, payload separation, etc).

The speci cation we treated in this case study focuses on regulation and con guration parts.

The ight regulation part is modeled by six Sdl processes. With few exceptions, we have two loosely coupled Sdl processes for each stage: one describing the ring and the other the extinction of the stage. In general, they work as follows. Both the ring and the extinction process receive as input the ring date, provided by the ight control part. Then, the ring process executes the ring sequence i.e, the set of actions to be done, with the right deadlines, in order to properly re the stage at the given date. If some malfunctioning is detected during this sequence, the extinction process takes over and attempts to stop the ring, using an adequate stop sequence. Otherwise, the extinction will occur later, eventually prior to the moment when the stage is dropped out. Example 3.1 An over-simpli ed ring process is illustrated in gure 4. The informal actions action 1, ... action n must be executed precisely at time T0-d1, ... T0-dn respectively, where T0 is a parameter received by the process and d1, ... dn are constant values. The informal actions abstract external commands which have to be initiated by the process (external sensors reading, opening or closing engine valves, etc.) at the right moments in time. The ight con guration part contains seven Sdl processes. Each process implements some particular con guration task: eap separation, epc separation, payload separation, etc.

In their case too, the separation dates are provided by the control part, based on the current ight evolution.

Example 3.2 A simpli ed con guration process is presented in gure 5. Here, the opening informal action must be executed on the reception of the open signal, eventually in the interval de ned by timers t early and t late. Thus, if the open signal arrives too early, it must be saved or, if the signal does never arrive, the action has to be executed at the end of the interval.

The translation of regulation and con guration processes into IF is straightforward. Nevertheless, an implicit assumption about the time progress was made in all of them: timeout-driven transitions are urgent and must be executed as soon as they are enabled i.e, exactly at the expiration time. This assumption is con icting with the standard semantics of Sdl, which consider that all the transitions are lazy. Fortunately, at IF level we could explicitly de ne timeout-driven transitions as eager, thus modeling exactly the intended behaviour.

Environment

In order to obtain a realistic functional model of the ight program, we have to take into account its surrounding environment. For example, precise human interactions are expected to initiate the launch procedure. Furthermore, both regulation and con guration parts were designed to closely interact with the control part of the program during the ight. Some minimal coordination must be ensured here e.g, that all the components received the same ring date otherwise no meaningful veri cation could be done.

To handle all the assumptions on the system environment, the solution we adopted is to \close" our Sdl speci cation by adding external processes abstracting the actual behaviour of the control part, the redundant program and the ground: the ight control is over simpli ed. It consists on several processes which describe a nominal behavior: they are supposed to send, with some controlled degree of uncertainty, the right ight commands, with the right parameters at the right moments in time2 . Nevertheless, here again the time semantics has to be considered with particular attention in order to obtain the intended behaviour (see example 3); the redundant program: at the initialisation time, the main program requests the status of the redundant one. Hence, the later was abstracted by a simple non-deterministic process, which could respond either positively or negatively to the main's request; the ground part implements the nominal behavior of the launch protocol on ground side. Progressively, it pass the control of the launcher to the on board ight program, by providing the launch date and all the other con rmations needed for launching.

On the other hand, it remains ready to take back the control, completely, if some malfunctioning is detected during the launch procedure.

Example 3.3 In the nominal case, the control part eventually sends the extinction command of the vulcain engine within some given time interval L; U]. Such behavior could be sketched by the Sdl process from gure 6. Nevertheless, its meaning is quite unclear: following the standard Sdl semantics it is possible that the process stays forever at the init state. Following the ObjectGeode semantics, the transition is executed as soon as it becomes enabled, so when now equals min. Unfortunately, none of these interpretations is the intended one. The right solution is achieved only at IF level by de ning the transition as delayable: it will be eventually executed at some time within the interval.

Requirements

With the help of Eads experts, we identi ed a set of about twenty safety functional requirements ensuring the right service of the ight program. The requirements were classi ed into three classes, as follows:

general requirements, which are not necessarily speci c to the ight program but in general, to all critical real-time systems. They include basic untimed properties such as the absence of deadlocks, livelocks or signal looses, and basic timed properties such as the absence of timelocks, Zeno behaviors or deadlines missed; overall system requirements, which are speci c to the ight program and concern its whole behavior. For example, we mention here the global order for the ight phases (e.g, ground, vulcain ignition, booster ignition, etc...), or the vulcain engine extinction in the presence of anomalies; local component requirements, are also speci c to the ight program and concern the functionality of some of its parts. In this category, we consider for example checking the occurrence of some actions in some component (e.g, payload separation occurs eventually during an attitudinal positioning phase, or the stop sequence no. 3 could happens only after lift-o , or the state of engine valves conforms to the ight phase, etc.)

Initially, all these requirements were described using Goal observers 2]. Then, in order to be handled with IF tools, they were translated manually into temporal logic formulae or nite-state automata.

Veri cation

Formal veri cation is certainly the most challenging phase in a formal development process. It is the only way to provide an earlier and e ective feedback about the behavior of the system, regarding its environment and its requirements. In order to master the complexity of the veri cation we propose to split it into ve independent steps, ranging from the simplest static analysis to the most powerful model-checking techniques (see gure 7). This section presents the concrete veri cation results obtained on the Ariane-5 speci cation, following this methodological guidelines.

Requirements

Basic static analysis

During this rst step, simple analysis are applied on the speci cation. They include both sanity tests and some simple static analysis.

In the rst category, we mention basic tests on variables and signals. For instance, the user detects variables or timers never assigned nor used. Furthermore, variables which might be used without being initialised are computed. Moreover, signals which are never sent nor received are also indicated to the user. In the second category, we mention techniques such as live variables analysis or constant propagation. They give us much more accurate information about the use of the variables in the program while detecting various kinds of redundancy, such as unused variable de nitions or any other form of dead-code.

Model exploration

The validation process continues with a debugging stage. With no sake for exhaustivity, the user begins to explore the model of the speci cation, in a guided or random manner. Simulation states do not need to be stored as the complete model might not be explicitly constructed at this moment. The aims at this stage are multiples. Firstly, the user could inspect and validate known scenarios about the functioning of the speci cation. Secondly, the user can test simple safety properties, which might hold on all execution paths. Such properties might range from generic ones, such as deadlocks, signal loss or wrong timer setting detection, to more speci c ones, application dependent. In general, they are tested either using speci c code instrumentation, or using external observers. When an error is found, a diagnostic scenario can be produced at this step by the ObjectGeode simulator.

Example 4.1 By inspecting a diagnostic scenario leading to a timed exception (e.g, unexpected timeout signal) we found an inconsistence between several constants used to control the ring of the epc. A simpli ed Msc corresponding to this scenario is presented in gure 4.2. On one hand, the sending of the desactivation signal is conditioned by the reception of the status signal. On the other hand, status is sent at time H0+t1 while desactivation must be sent at time H0+t2. The error occurred here because t1 and t2 were de ned such that t1 was greater than t2.

Advanced static analysis

The aim at this step is to prepare the speci cation to an exhaustive simulation. Optimisation based on static analysis results are intensively applied in order to reduce both the state vector and the state space, while completely preserving its behavior. Di erent kinds of optimisations are currently available. The rst one is variable and timers recovery, which consists in diminishing the number of variables and timers respectively used inside the speci cation. This optimisation exploits results obtained by live and dependency analysis:

a variable (respectively clock) is live in a control state if it will be used before being assigned on some path starting on that state; two variables (respectively clocks) are dependent in a control state if their di erence is constant and can be statically computed at that state;

The theoretical result used here is that any program can be rewritten using at most n variables, where n is the maximal number of live and functionally independent variables at some point in the program. Example 4.2 The initial Sdl version of the ight program used no less than 130 timers.

Using our static analysis tool we were able to reduce them to only 55 timers, functionally independent ones. Afterward, the whole speci cation was rewritten taking into account the redundancies discovered by the analyzer.

A second optimisation attempts to identify live equivalent states by introducing systematic resets for dead variables in the speci cation. In this way, it prevents to distinguish between simulation states which di er only by values of dead variables. This technique is very e ective given that it can be applied locally at control-state level (contrarily to variable recovery which applies only if some condition holds on all control states of the program).

Example 4.3 For this case study, the live reduction was not so impressive due to the reduced number of variables (others than clocks) used in the speci cation. Anyway, our initial attempts to generate the model without live reduction failed. Finally, using live reduction we were able to build the model but still, it was of unmanageable size, about 2 10 6 states and 18 10 6 transitions.

Finally, the last optimisation we mention here is slicing 21]. This technique consists in statically extracting the part of the speci cation which is relevant to a slicing criterion i.e, here derived from a xed property to be veri ed. The sliced part might be signi cantly smaller than the entire speci cation since, contrarily to previous optimisation techniques, slicing does not aim to preserve all the behaviors but only those which might in uence the validity of the chosen property. In particular, we used this slicing technique to automatically eliminate some silent Sdl processes, which do not perform any \relevant" action.

Model generation

The model generation step aims to explore completely the model of the speci cation by exhaustive simulation. By speci cation we mean here either the complete one, or a sliced version with respect to some xed property. This step might be extremely di cult given the apriori exponential size of the model. In order to deal with, the user controls both the representation scheme for states and sets of states and the exploration strategy. For example, the use in IF of a symbolic representation for timers i.e, using di erence-bound matrixes to represent zones and regions 3], is particularly useful when dealing with a large time horizon and irregular timing constraints. Instead of representing each single particular point in time, this kind of representation allow us to handle set of equivalent points with respect to their future behavior. In particular, such symbolic representation is of real interest here because of the wide spectrum of timers values: for example, very short ones for regulation timers (measured in milliseconds, see gure 4) and longer ones for control timers (measured in minutes, see gure 6).

Concerning the exploration strategy, the use of partial order techniques 12] is clearly of value in the exploration of asynchronous communicating systems. Thus, spurious interleavings initiated either by internal actions or by the consumption of messages from communication bu ers could be eliminated still preserving all the observable behavior of the speci cation. Nevertheless, special care must be taken with respect to time: since time is global and clocks are synchronised there exists implicit dependencies induced by time progress (e.g, time progress may disable some observable, relevant actions). In order to avoid this problem, we implemented in IF a restricted variant of partial order reduction in which outputs and time progress transitions are always considered as observable.

For example, let us consider a generic situation which occurs frequently in the ight program: a multicast communication which involves one sender and n receivers. As the communication in Sdl is asynchronous bu ered, even if all the bu ers are empty we obtain 2 n intermediate states, due to all possible interleavings of receiver inputs. Fortunately, using partial order reduction, the combinatorial explosion disappears: inputs are executed in some order, and only n intermediate states are explored. Example 4.4 The use of partial order reduction was mandatory in order to construct models of reasonable size. Here, we reduce the size of the model with 3 orders of magnitude i.e, from 2 10 6 states and 18 10 6 transitions to 1:6 10 3 states and 1:65 10 3 transitions, which could be easily handled by Cadp model-checkers.

In practice, we consider two di erent situations regarding the environment. The rst one is time-deterministic, which means that all environment actions (in particular the control part) take place at precise moments in time. The second one is time-nondeterministic which means that environment actions take place with some degree of time uncertainty (within a prede ned time interval). From the environment point of view, the later situation corresponds to a whole set of scenarios, whereas the former situation focus only on a single one.

Model-checking

Once the model being generated, several model-checking techniques can be applied to verify expected properties on the speci cation. Nevertheless, on-the-y veri cation methods i.e, which combines the model-generation and model-checking steps, might be used.

Using the IF validation toolbox, two approaches can be followed to express these properties. First, temporal logic formula could be veri ed using Evaluator, the Cadp -calculus evaluation tool.

Example 4.5 The requirement expressing that the stop sequence no. 3 occurs only during the ight phase, and never on the ground phase can be expressed by the following temporal logic formula, veri ed with Evaluator: : X: < EPC!Stop 3 > tt ^< EAP!Fire > X Intuitively, it express that it is not possible to reach a state where is possible to perform the stop sequence no. 3 without executing in the past the ring of the eap (which denotes the beginning of the ight phase).

A second approach, usually much more intuitive for a non expert end-user, consists in computing an abstract model (with respect to a given observation criteria) of the overall behavior of the speci cation. Such a model can be then visualised and possible incorrect behaviors can be detected. These abstract models are computed by Aldebaran and, depending on the (bi)-simulation relation used, they preserve di erent classes of properties. and epc, and the detection of anomalies are preserved on the graph from gure 9 generated by Aldebaran. It is the quotient model with respect to safety equivalence 5] while keeping observable only the actions above. For instance it is easy to check on this abstract model that, whenever an anomaly occurs before action EPC!Fire 3 (ignition of the Vulcain engine), then nor this action nor EAP!Fire action are executed and therefore the entire launch procedure is aborted. Table 1 gives the average time required for verifying each kind of property (by temporal logic model checking and model minimisation respectively).

Conclusions

In this paper we described a practical experiment on the validation of a real-time embedded software speci cation, the con guration and regulation part of the Ariane-5 Flight Program.

First, this software has been formally speci ed in Sdl by reverse engineering. Then, following a set of general methodological guidelines, the speci cation has been continuously improved and the twenty expected requirements were all veri ed on the nal version. In particular, the combination of di erent optimisation techniques, operating either at the source level (like static analysis or slicing) or at the semantic level (like partial-order reductions) happened to be particularly useful in order to deal with large size state spaces. Nevertheless, this work covers only a limited part of the development process of real-time embedded systems: the speci cation that has been developed and validated is abstract and rather \far" from the existing executable code. This approach is therefore well-adapted in the earlier phases of development but applying it to more concrete designs could become problematic in practice.

The main di culty of this case-study comes from the combination of various kind of time constraints. On one hand, the functionality of the ight program strongly depends on an absolute time: coordination dates are frequently exchanged between components in order to synchronise their behaviour during the whole ight. On the other hand, this system has to be veri ed within a partially constrained environment, reacting with some degree of temporal uncertainty. In this experiment, this expressivity problem was solved at the IF level thanks to explicit urgency attributes. Clearly, such features should be made available at speci cation level. In particular, ongoing work address the introduction of high-level time and performance annotations in Sdl 9]. Another future direction of investigation is the synchronous/asynchronous interaction. Currently, with Sdl we were able to build an abstraction of the ight program, as an asynchronous interaction of several processes, which express the overall sequential behavior and the most important timing constraints on it. However, this speci cation is not complete, at least because very important program parts, such as navigation and control, must be almost completely abstracted away, because they cannot be described in Sdl. Such parts describing intensive data-ow transformations have to be executed in a synchronous manner, and are usually described using synchronous languages such as Lustre 13]. Unfortunately, from the synchronous side, inherently sequential parts with asynchronous interaction also could not be properly expressed. Nevertheless, this kind of dual design where coexist both asynchronous components and synchronous ones is not an exception and occurs very often in real-time applications design practice. We plan for the future to investigate how to combine, in a sound manner, synchronous and asynchronous descriptions, and the possible tool support for doing it, in order to exploit at best the advantages conferred by both programming paradigms.

Figure 2 :

 2 Figure 2: Ariane-5 launcher.

Figure 3 :

 3 Figure 3: Flight program architecture.

Figure 4 :

 4 Figure 4: A ring process.

Figure 5 :

 5 Figure 5: A con guration process.

Figure 6 :

 6 Figure 6: Control process.

Figure 7 :

 7 Figure 7: Veri cation methodology.

Figure 8 :

 8 Figure 8: Diagnostic trace.

Figure 9 :

 9 Figure 9: Minimal model.

Table 1 :

 1 Table 1 presents in each case the sizes of the models obtained depending on the generation strategy used. Veri cation Results.

	time deterministic non-deterministic time state state explosion explosion + live reduction 2201760 st. ? live reduction ? partial order state generation ? partial order 18706871 tr. model explosion + live reduction 1604 st. 195718 st. + partial order 1642 tr. 278263 tr.
	model veri cation	model minimisation model checking	1 sec. 15 sec.	20 sec. 120 sec.

the description was taken from the Esa -European Space Agency -web page: http://www.esa.int/

The data used here correspond to the ight no. 503 of Ariane-5 launcher

Ariane-5 is an European Space Agency Project delegated to CNES (Centre National d'Etudes Spatiales)


Marius Bozga
email: fbozga@imag.fr

Susanne Graf
email: graf@imag.fr

Laurent Mounier
email: mounierg@imag.fr

Automated validation of distributed software using the IF environment

This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools can cover by itself the whole validation process. The IF environment was built upon an expressive intermediate language and allows to connect several validation tools, providing most of the advanced techniques currently available. The results obtained on several large case-studies, including telecommunication protocols and embedded software systems, con rm the practical interest of this approach.

Introduction

Automated validation of distributed software is a desirable objective to improve the industrial production of correct systems like communication protocols or embedded systems. In spite of the numerous on going researches and tool developments carried out in this area, this activity remains di cult in practice: on one hand the initial software description is usually provided in a high-level formalism (either a programming language or a formal design notation like Lotos 23], Sdl 25] or Uml 30]), and, on the other hand, a wide range of tools are necessary to cover the whole development process, operating at di erent levels of program descriptions. Even if several interesting tools are currently available, either commercial or academic ones, none of them can ful ll in itself all the practical needs. Commercial tools (such as ObjectGeode 32], Tau 1], StateMate 22], Rational Rose 31], etc.) provide several development facilities, like editing, code generation and testing. However, they are usually restricted to basic veri cation techniques (exhaustive simulation, deadlock detection, etc) and are \closed" in the sense that there are only limited possibilities to interface them with others. On the other hand, there exist numerous academic tools (like Smv 28], Hytech 19], Kronos 34], Uppaal 27], Spin 20], InVeSt 2], etc.) o ering a broad spectrum of quite e cient veri cation facilities (symbolic veri cation, on-the-y veri cation, abstraction techniques, etc.), but often supporting only low-level input languages. This may restrict their use at an industrial scale. This situation motivated the development of IF, an intermediate representation for distributed software together with an open validation environment. This environment ful lls several requirements. First of all, it is able to support di erent validation techniques, from interactive simulation to automatic property checking, together with test case and executable code generation. Indeed, all these functionalities cannot be embodied in a single tool and only tool integration facilities can provide all of them. For a sake of e ciency, this environment supports several levels of program representations. For instance it is well-known that model-checking veri cation of real life case studies usually needs to combine di erent optimization techniques to overcome the state explosion problem. In particular, some of these techniques rely on a syntactic level representation (like static analysis and computations of abstractions) whereas others techniques operate on the underlying semantic level. Another important feature is to keep this environment open and evolutive. Therefore, tool connections are performed by sharing either input/output formats, or libraries of components. For this purpose several well-de ned application programming interfaces (apis) are provided. The IF validation environment is quite similar in its philosophy to the one proposed in the Bandera project 12], which also relies on a dedicated intermediate format to translate (abstract) Java source code into the input language of existing model-checkers (like Spin or Smv). However, currently we mainly address with IF distributed software validation from design formalisms (like Sdl or Uml) which are widely used in the application area we consider (communication protocols and embedded systems).

The IF validation environment relies on three levels of program representation: the speci cation level, the IF intermediate level, and the Lts semantic model level. Figure 1 describes the overall architecture and the connections between the toolbox components. The implicit enumerative representation consists in a set of C functions and data structures allowing to compute on demand the successors of a given state (following the Open/C sar 16] philosophy). This piece of C code is generated by the if2c compiler, and it can be linked with a \generic" exploration program performing on-the-y analysis.

In the symbolic representation sets of states and transitions of the Lts are expressed by their characteristic predicates over a set of nite variables. These predicates are implemented using decision diagrams (Bdds). Existing applications based on this api are symbolic model-checking and minimal model generation.

Finally, the explicit enumerative representation simply consists in an Lts le with an associated access library. Although such an explicit representation is not suitable for handling large systems globally, it is still useful in practice to minimize some of its abstractions with respect to bisimulation based relations.

The intermediate level components. if2if 6] implements several algorithms based on static analysis to transform an IF speci cation. A rst transformation concerns dead variable resetting (a variable is dead at some control point if its value is not used before being rede ned). This optimisation can be also applied to bu er contents (a message parameter is dead if its value is not used when the message is consumed). Although very simple, such optimisation is particularly e cient for state space generation (reductions up to a factor 100 were frequently observed), while preserving the exact behaviour of the original speci cation

Case studies

The IF environment was used in several case studies, including as well telecommunication protocols and embedded software. The most relevant ones, from the complexity point of view, and the results obtained are summarized below.

SSCOP Protocol

The Sscop (Service Speci c Connection Oriented) protocol is standardized under reference itu-t q2110 24]. Originally, it was conceived to reliably transfer data between two high bandwidth network entities. Although its design makes it ready to treat signi cant volumes of data, currently its use is con ned in ones of the underlayers of the aal layer (Atm Adaptation Layer). The services it provides are connection control (establishment, ow-control, release), data transfer, and error detection.

The Sscop standardization document contains an Sdl description of the protocol. This description has been coded by France Telecom R&D using ObjectGeode. It consists in approximately 2000 lines of Sdl textual code which describes the protocol as one single process with 10 control states, 134 variables, and 4 timers. The description was centered on signaling and some simpli cations have been made according to Sscop implementations available in France Telecom R&D. Our main goals were the formal validation of the specication and, in addition, automatic test-case generation starting from it. Clearly, the size and complexity of this speci cation made any brute force validation approach not applicable. In particular the data part was very large, and each state of the underlying model could not be stored in less than 2kB. Therefore only a small part of the state space could be explored from this initial speci cation, not su cient to verify interesting properties. Consequently, we adopted a more incremental veri cation strategy. A rst step was to apply a very rough abstraction by (automatically) eliminating all the variables in the speci cation. Thus, it was possible to compare this very abstract speci cation with the one supplied by the standard to model the interactions between adjacent layers of Sscop, to check if the abstract speci cation provides at least the expected behaviour. This comparison was performed using Aldebaran, with respect to the so-called safety preorder 5]. Some subtle errors, such as omission of timers setting, were found using this method. After this debugging phase, the second step was to \prepare" the initial Sdl specication for a more accurate state space analysis. It consisted in basic static analysis techniques like dead code elimination and live variable detection using if2if. The bene ts were really spectacular on this example, and, in particular, the amount of memory required to store a model state fell to 0.2 kB. Finally, these optimisations made possible the use of exhaustive simulation techniques. More precisely we considered a system consisting in a pair of entities, communicating through a bounded fo channel, and we concentrated our validation e ort to a set of representative distinct scenarios (connection establishment, disconnection, data transfer, : : : ). Using speci c slicing criteria, it was therefore possible to (automatically) simplify even more the speci cation, depending on the property under veri cation or the test purpose. The underlying models obtained were about 20 000 states large, and errors were found in the data transfer phase of the speci cation. The complete experiment is reported in 9].

Mascara Protocol

The Mascara(Mobile Access Scheme based on Contention And Reservation for Atm) protocol is a special medium access control protocol designed for wireless Atm communication and developed by the wand(Wireless Atm Network Demonstrator) consortium 13]. A wireless Atm network extends transparently services to mobile terminals (mt) via a number of geographically distributed access points (ap). The task of the Mascara protocol is to mediate between aps and mts via a wireless link. The protocol has a layered structure, where we consider only the highest layer, the Mascara control layer. The overall description of the Mascara protocol which we got is 300 pages of Sdl textual code. We concentrate on the veri cation of the Mascara control layer, for which the Sdl description could be made reasonably complete. Here we brie y present the veri cation of the dynamic control. For complete information, we refer the reader to 17] which reports the complete experiment on the dynamic part. In addition, another veri cation experiment has been carried out on static control 4]. Veri cation should be carried out under a general environment with realistic restrictions. As we have not obtained information on the Mascara upper layer, we considered initially an open system with an unconstrained upper layer, which would allow us to obtain the most general veri cation results. But communication via unbounded channels, leads to in nitely growing channel contents and thus an in nite state model in case that the environment sends requests too often. This is typically the case in reactive systems always ready to treat requests from the environment. The approach we have chosen to provide a more restricted, but still realistic envi-ronment consists in limiting the number of requests it can make per time unit. We assume that within one time unit, no more than N requests can be sent by the environment. The system has never to deal with more than N requests simultaneously which leads, in the Mascara protocol, to bounded channel contents. The success of the method depends on the use of a realistic bound. We use N=4. Unfortunately, even with such a restricted environment, it was impossible to generate the state graph of the global system as a whole. However, we have applied two di erent types of compositional veri cation: the rst one is based on property decomposition 26], and the second one is based on compositional generation of a state graph minimized with respect to a behavioral equivalence 18]. In particular, using in addition both live analysis and partial order reduction for the generation of the subsystems, we were able to compositionally generate a reduced model of the global system using compositional generation. Table 4.2 gives an overview of a subset of the models we have generated using different reduction techniques and allows to compare their sizes and generation times. Finally, several properties ranging for generic ones such as deadlocks and livelocks to more speci c such as association establishment, connection, disconnection, were veri ed on the generated models.

Ariane-5 Flight Program

The work on this experiment was initiated by Eads Launch Vehicles to better evaluate the applicability of formal validation techniques on an existing software, the Ariane-51 Flight Program. This is the embedded software which solely controls the Ariane-5 launcher during its ight, from the ground, through the atmosphere and up to the nal orbit.

The veri cation experiment is reported in 11]. First, this software has been formally speci ed in Sdl by reverse engineering from the existing code. Then, following a set of general methodological guidelines, the speci cation has been continuously improved and all the initial requirements were veri ed on the nal version. In particular, the combination of di erent optimisation techniques, operating either at the source level (like static analysis or slicing) or at the semantic level (like partialorder reductions) happened to be particularly useful in order to deal with large size state spaces. For example, the initial Sdl version of the ight program used no less than 130 timers. Using our static analysis tool we were able to reduce them to only 55 timers, functionally independent ones. Afterward, the whole speci cation was rewritten taking into account the redundancies discovered by the analyzer. The main di culty of this case-study comes from the combination of various kind of time constraints. On one hand, the functionality of the ight program strongly depends on an absolute time: coordination dates are frequently exchanged between components in order to synchronise their behaviour during the whole ight. On the other hand, this system has to be veri ed within a partially constrained environment, reacting with some degree of temporal uncertainty. In this experiment, this expressivity problem was solved at the IF level thanks to explicit urgency attributes. Clearly, such features should be made available at speci cation level. In particular, ongoing work address the introduction of high-level time and performance annotations in Sdl 10]. In practice, we have considered two di erent situations regarding the environment. The rst one is time-deterministic, which means that all environment actions (in particular the control part) take place at precise moments in time. The second one is time-nondeterministic which means that environment actions take place with some degree of time uncertainty (within a prede ned time interval). From the environment point of view, the later situation corresponds to a whole set of scenarios, whereas the former situation focus only on a single one. Table 2 presents the sizes of both models generated according to di erent generation strategies. It gives also the average time required for verifying each kind of property (by temporal logic model checking and model minimisation respectively).

Conclusion and Perspectives

The IF environment has already been used to analyze some representative Sdl speci cations such as Sscop, an Atm signalisation protocol, Mascara, an Atm wireless transport protocol and Ariane-5 ight program, a part of the embedded software of Ariane-5 launchers. It is currently used in several on going industrial case-studies, including respectively real-time multicast protocols Pgm and Rmtp-ii, and the session initiation protocol Sip. The bene ts of combining several techniques, working at di erent program level, were clearly demonstrated. In particular, traditional model-checking techniques were not su cient to complete on these large size examples. Several directions can be investigated to improve this environment. The rst direction of improvement concerns the IF language. As currently de ned, it allows only the description of static systems, were the number of components (processes and bu ers) as well as their interactions are xed throughout the execution. This strongly limits our ability to handle complex dynamic speci cations. We work on a less restrictive de nition, were both parameterized descriptions (containing some xed number of replicated components) as well as general dynamic creation and destruction of components are allowed. Furthermore, some improvements will be made regarding the description of components itself, such as the possibility to express structured control using composed states (like in statecharts).

A second direction of improvement concerns the IF simulator, the core component allowing to construct and to explore the underlying semantic model of IF specications. Currently, this model is labeled transition systems, and its construction and exploration are quite restricted: rst, only pure asynchronous execution (by interleaving) is possible and second, no access is provided to the state of the system (e.g, current values of variables, current states of processes). We envisage to improve these points, by implementing a exible simulator able, for instance, to deal with both synchronous and synchronous components, or more generally, to take into account some scheduling policy over components during the simulation. In addition, this simulator will interact with running components through a well-de ned abstract interface, thus allowing to integrate also external components (for example, directly expressed as executable code). A third direction of improvement concerns the validation methods. Clearly, we will continue to adapt and to improve our static analysers as well as our model checkers to handle the extended IF descriptions. Also, some work must be done to reduce the manual overhead, yet important, needed by sophisticated techniques such as compositional veri cation. Finally, another important issue concerns the validation of non-functional requirements. In particular, performance evaluation becomes crucial for an important part of internet protocols (such as Pgm or Rmtp-ii) which are not necessarily designed to achieve full reliability, but only an average correct behaviour with respect to probabilistic assumptions on their execution environment (e.g, propagation delays, message loss, network elements speed, etc). At middle term, we plan to connect to IF environment to simulation environments like Opnet 29] and Ses/Workbench 21]. The IF package can be downloaded at http://www-verimag.imag.fr/DIST SYS/IF.

  The semantic model level components. Cadp 14] is a toolset for the veri cation of Lotos speci cations. It is developed by the Vasy team of Inria Rhône-Alpes and Verimag. Two of its model-checkers are connected to the IF environment: Aldebaran (bisimulation based), and Evaluator (alternating-free -calculus). For both tools, diagnostic sequences are computed on the Lts level and they can be translated back into Msc to be observed at the speci cation level. Kronos 34] is a model-checker for symbolic veri cation of Tctl formulae on communicating timed automata. The current connection with the IF environment is as follows: control states and discrete variables are expressed using the implicit enumerative representation, whereas clocks are expressed using a symbolic representation (particular polyhedra).Tgv 15] is a test sequence generator for conformance testing of distributed systems (joint work between Verimag and the Pampa project of Irisa). Test cases are computed during the exploration of the model and they are selected by means of test purposes.

. A second transformation is based on the slicing technique 33]. It allows to automatically abstract a given speci cation by eliminating some irrelevant parts w.r.t. a given property or test purpose 7]. if2pml 4] is a tool developed at Eindhoven TU to translate IF speci cations into Promela.

Table 1 .

 1 Mascara veri cation results

	generation strategy	ap model time size	mt model time size	ap + mt model size
	-live reduction 7 308 400 st. 207 0 35 00 4 388 765 st. 171 0 58 00 -partial order 30 689 244 tr. 12 811 961 tr. + live reduction 351 202 st. 12 0 22 00 63 628 st. 1 0 03 00 -partial order 1 536 699 tr. 325 312 tr. + live reduction 28 069 st. 1 0 53 00 6 580 st. 7 00 218 130 st. + partial order 52 983 tr. 20 913 tr. 1 142 215 tr. + live reduction 1 630 st. 9 00 977 st. 3 00 + partial order 2 885 tr. 2 845 tr. + slicing

Table 2 .

 2 Ariane-5 Flight Program veri cation results.

			time deterministic non-deterministic time
	-live reduction -partial order model + live reduction 2 201 760 st. na generation -partial order 18 706 871 tr. + live reduction 1 604 st. + partial order 1 642 tr.	na na 195 718 st. 278 263 tr.
	model veri cation	model minimisation model checking	1 00 15 00	20 00 2 0 00 00

Components descriptionWe brie y present here the main components of the environment, together with some external tools for which a strong connection exists.The speci cation level components. ObjectGeode 32] is a commercial toolset developed by Telelogic supporting Sdl, Msc and Omt. In particular, this toolset provides an api to access the abstract tree generated from an Sdl speci cation. We have used this api to implement the sdl2if translator, which generates operationally equivalent IF speci cations from Sdl ones. Given the static nature of the current version of IF, this translation does not cover yet the dynamical features of Sdl (e.g., process instances creation).

Ariane-5 is an European Space Agency Project delegated to CNES France.

Acknowledgements

We gratefully thank Guoping Jia and Lucian Ghirvu for their help on tools development and experimentations.