Marco Marazza

Orlando Ferrante

Alberto Ferrari

Automatic Generation of Failure

Keywords: Safety-critical Systems, Systems-on-Chip, Safety Analysis, Formal Methods

published or not. The documents may come   L'archive ouverte pluridisciplinaire

I. INTRODUCTION

System-on-Chip (SoC) design and testing complexity seems to fit very well a monotonic non-decreasing function of time. On the one hand, technology downscaling is causing considerable drawbacks, e.g. higher susceptibility of circuits to radiation-induced soft errors [START_REF] Baumann | Radiation-induced soft errors in advanced semiconductor technologies[END_REF]. On the other hand, SoC functions are getting more and more sophisticated as SoCs spread over safety-critical domains such as automotive, aerospace, building automation, railway and medical. The trend of pervasively using SoCs to control physical systems directly interacting with human beings creates the need for new methodologies and tools to quantify the dependabilityand in particular the functional safety-achieved by the system. This requires improving the capabilities of testing techniques and failure scenario identification for SoCs and represents one of the most crucial concerns for engineers and international certification authorities. The service delivered by a system is its behaviour as perceived by another system (human or physical) interacting with it. The deviation of the service delivered by a SoC from the specified service is known as a service failure. Random hardware faults introduce unpredictability to the services provided by the SoC, and can generate service failures. The typical design approach to control service failures, and consequently the system's functional safety, is to introduce redundancies to the system design in the space, time and information domains. However, even if controlled, still radiation-induced soft errors can cause residual service failures for a number of reasons: the techniques to control failures (1) might be based on models, which by nature suppress some information, (2) could cover a subset of the total set of occurring faults, (3) might only cover faults assumed to occur in specific use cases, (4) could have some limitations due to implementation costs. In summary, regardless of the efforts spent for techniques aiming at improving the dependability of delivered services, SoC services will be inevitably affected by residual failures due to soft errors. Standards like IEC 61508 [2] and ISO 26262 [3] introduce metrics and recommend methodologies and tools to quantify the Safety Integrity Level (SIL) of a SoC; for each SIL level the target value for metrics to be achieved by the design is defined and must be guaranteed. In this context, automatic generation of failure scenarios assumes fundamental importance to test the SoC design against fault models and to explore design solutions, including evaluation of the effectiveness of faulttolerant mechanisms and cost trade-off. Several techniques and tools have been described in literature proposing model-based approaches to safety analysis. In [START_REF] Peikenkamp | Towards a unified model-based safety assessment[END_REF] the application of a model based flow for the automatic generation of fault trees based on generation of minimal cut sets is shown. In [START_REF] Gdemann | Using deductive causeconsequence analysis (DCCA) with scade[END_REF] the SCADE formalism is used to perform Deductive Cause-Consequence Analysis (DCCA) using Design Verifier as formal engine. In [START_REF] Joshi | Model-based safety analysis of simulink models using scade design verifier[END_REF] Joshi et al. describe some results on exploiting Simulink and SCADE for the safety analysis based on Simulink models. In [START_REF] Bozzano | Safety, dependability and performance analysis of extended aadl models[END_REF] Bozzano et al. describe the SLIM language for the formalization of hybrid systems in presence of faults and an automatic fault analysis tool-flow using NuSMV. All the previously described approaches use high level models of the system under analysis for the automatic generation of faulttrees and binary decision diagrams (BDDs) as formal analysis techniques.

In this paper we propose an extension of existing approaches to perform automatic failure scenario generation during the design of complex System-on-Chip architectures. The main contributions of the paper can be summarized as follows: [START_REF] Baumann | Radiation-induced soft errors in advanced semiconductor technologies[END_REF] an algorithm for the generation of Minimal Critical Failure Set (MCFS) based on Bounded Model Checking (BMC) is described (2) a methodology and a Simulink-based tool for the automatic generation of failure scenarios for SoC is described and (3) the application of the proposed analysis flow to a concrete SoC use case is presented and discussed. Our approach differs from the previous described ones in several ways. The algorithm is not founded on the construction of BDDs but relies on Bounded Model Checking (BMC) technique taking full advantage of the last advances in parallel SAT solving [START_REF] Ferrante | Parallel nusmv: a nusmv extension for the verification of complex embedded systems[END_REF]. The use of BDD limits the applicability of existing techniques to models containing hundreds of Boolean memory elements whereas the use of Parallel SAT solvers in conjunction with BMC allows for successful algorithm application to industrysized level problems tackling models containing thousands of Boolean variables. The analysis tool automatically explores all the minimal critical failure sets starting from a functional model of the SoC and the specification of components' failure modes relying on an internal model transformation engine [START_REF] Ferrari | DesyreML: a sysml profile for heterogeneous embedded systems[END_REF] that automatically builds the error model starting from a functional formalization of the SoC and a list of failure mode functions allowing the designer focusing on the SoC architecture and fault-tolerance mechanisms design aspects. The minimal nature of injected faults intuitively ensures that only the failures significant to the analysis will be considered in the generated scenarios as will be described in detail in the following sections. Finally, our analysis process supports the MATLAB R Simulink/Stateflow [START_REF]Matlab[END_REF] framework as modelling and analysis front-end that represents the standard de-facto for system design.

II. MOTIVATING EXAMPLE

As a motivating example we refer to a simple function generating a Pulse Width Modulated (PWM) waveform with period and active time specified by an external module. The example models the implementation of the function on the eTPU IP [START_REF] Freescale | Enhanced Time Processing Unit[END_REF]. The eTPU is a programmable CPU co-processor designed for timing control (real-time input capture/analysis and output generation) provided with configurable hardware channels operating in parallel. A previous work [START_REF] Rodrigues | A case study for formal verification of a timing coprocessor[END_REF] successfully applied formal verification to the eTPU based on System Verilog Assertions (SVA) language and Cadence TM IFV tool for static formal verification. As shown in Fig. 1, at top level our model takes three main inputs: a reference source of ticks -representing the reference in the time, angle or similar domains-modelled as a counter register and a couple of values, representing the desired period and active time of the PWM waveform to generate. We can consider them as constants, with no loss of generality. The function is modelled as a composition of two main FSMs: the the hardware FSM and the software FSM. The hardware FSM (PWM OUT HW in Fig. 1) represents an eTPU channel configured in "eithermatch, non-blocking" mode [START_REF] Freescale | Enhanced Time Processing Unit[END_REF]; it is composed of two "action units" operating in parallel: each action unit is provided with a comparator and three latches. Fig. 3 shows the finite state machine representation of one action unit in Simulink/Stateflow. The comparator seeks for a match in value between the ticks reference (TCRA) and a software-defined value (MatchA). When these two match, the comparator triggers the channel pin-action logic, which drives the output pin. The modelled actions on the output pin are: set pin-high (PinA=1 in Fig. 3) and set pin-low (PinA=0 in Fig. 3) [START_REF] Freescale | Enhanced Time Processing Unit[END_REF]. The effective output pin behaviour is modelled by another FSM (not shown here) that keeps into account the events coming from both the action units. The three latches operate as follows: one latch notifies that a match event occurred, the service request latch notifies the eTPU scheduler that the channel has required service and a Flag latch reflects a Boolean variable set by software; in our example the Flag latch is set by eTPU-software to reflect its state in hardware. At the match event both the service request latch and the action unit's latch are raised. With reference to Fig. 3, the variables used to represent these two latches are respectively SR A and setMRLA. Depending on the current state of hardware latches a specific eTPU-software routine is selected by the eTPU scheduler and executed by the eTPU engine. Such a routine updates the proper matchregister of the hardware channel with the next-match time value and (re)sets the related action unit latches. The eTPUsoftware FSM (PWM OUT SW in Fig. 1) consists of three states: (1) an initialization state that sets the initial hardware configuration, (2) a state handling the actions related to the end of the active time and (3) a state handling the end of the PWM period. For sake of simplicity, the interaction between hardware and software has been modelled as a finite positive delay, with the intention not to explicitly model the whole channels operating in parallel and the scheduler managing their concurrent requests. We use this example to analyse unwanted functional behaviours (top-level events) through our algorithm in order to automatically generate failure scenarios. Unwanted functional behaviours are typically identified through hazard analysis techniques, exploiting pre-defined sets of keywords. An example of possible unwanted top level events is: (1) wrong duration of the generated period and (2) wrong duration of the generated active time. We modelled functional faults as stuckat-value occurring to hardware signals and variables (Fault injection blocks in Fig. 1). The functional specification for the stuck-at-value fault is depicted in Fig 2 . Until the Boolean SaV Enable signal equals zero, the Switch block lets the input value flow directly to the output (as an ideal wire). Once the SaV Enable signal goes to one (no matter how many time it stays at one) the control of the Switch makes it isolate the input: the output is stuck at its last assumed value and cannot change any more (represented by Memory1 block in Fig. 2).

III. ANALYSIS METHODOLOGY

We propose a model-based methodology for the automatic generation of failure scenario. The main steps are summarized in Fig. 5 and in this section we briefly review each of the activities. It is important to stress that the developed methodology and algorithm have also been applied to different application contexts, in particular as part of the effort in exploiting synergies between formal analyses and testing for Fig. 5. Methodology.

the verification of complex embedded systems in the MBAT project [13] and as part of the effort in defining methodology and tools for the design of Systems-of-Systems in the DANSE project [14].

A. Error Model Construction

As a first step the Error Model of the SoC architecture is formalized (Activity 1 in Fig. 5) by modelling its functional architecture. For each component the nominal behaviour is described in terms of Simulink/Statechart blocks and the specification of the failure modes that can affect it is provided. This step should be guided by a previously performed hazard analysis or by the expertise of the designers. In the general case a failure mode is represented as a state machine (directly modelled by the designer or selected from a specific library) and formalizes how the nominal behaviour of the component is modified in presence of a failure. After an automatic model transformation step an error model is constructed. In Section V the formal aspects of the transformation step will be described in detail.

B. Top Level Event Specification

The top-level event (TLE) is a hazardous behaviour that must not occur. It is an invariant property that must hold when the model behaves correctly (as expected). The TLE can be either addressed by deductive safety analysis such as fault tree analysis (FTA), or it can be identified directly from system requirements specification. The top-level event is a function involving the outputs and possibly the inputs of the subsystem. The evaluation of the function modelling the TLE should always be FALSE except in case of property violation, for which it switches to TRUE and the TLE is said to be activated. Faults occurring across the system have the potential of activating the TLE. For example, the TLE modelled in Fig. 4 formalizes the following property: in absence of faults the value of Pin Out (an output of PWM OUT HW in Fig. 1) delayed by one step and the value of Flag (an output of (PWM OUT SW in Fig. 1) must not be equal to one simultaneously.

C. Algorithm Execution

The Error Model is processed by the fault analysis (FA) algorithm that takes a top-level event specification as an additional input. The objective of the fault analysis is to exercise the error model by exhaustively exploring the inputs space and injecting failures in order to reach this unsafe behaviour. The outcome of this activity is two-fold: on the one hand a list of minimal sets of failures is produced (the minimal critical failure set). Each set collects the failures to be injected in order to assert the TLE and its minimal nature guarantees that if any of the collected (minimal set of) failures is not injected, the hazardous behaviour is not reached. On the other hand a set of execution traces is produced, each exposing a sequence of failure injections and input values that leads to the hazard for each minimal critical failure set. The traces can be used to effectively exercise the Error Model to show how the SoC evolves to a hazardous state and to help reasoning on its expected and unexpected unsafe behaviours.

D. Fault tolerant architecture design

The information collected in the previous activity is reviewed by the safety engineers to drive the design of one or more fault-tolerant versions of the SoC. It may be needed to iterate between activities 1, 2 and 3 (Fig. 5) to reach a mature description of the functional design before terminating the activity. The result of this activity is a fault-tolerant version of the SoC produced as an executable (and possibly synthesizable) model.

IV. RUN-TIME VERIFICATION

The traces generated during activity 3 (Fig. 5) are used to exercise the fault-tolerant model to check the effectiveness of the fault identification, detection and recovery (FDIR) mechanisms. During this phase flaws in the fault-tolerant SoC design may be discovered and iterations with both the safety engineering and the SoC design teams may be needed. The use of a model-based flow for the safety analysis of complex SoC has several advantages with respect to the classical manual process. At first the use of executable models helps the different teams to reason on a shared formal representation of the system, which helps minimizing the misinterpretation of requirements and communication issues between designand safety-engineers. Then, models can be processed automatically using model-transformation engines easing the design exploration process and reducing the occurrence of design errors, costs and time-to-market. Finally, a formal model is important for supporting the certification process needed for the qualification of fault-tolerant SoCs [2], [3].

V. FORMAL SPECS VERIFIER -FAULT ANALYSIS TOOL

In this section the Formal Specs Verifier tool for Fault Analysis (FSV-FA) is described. At first an overview of the tool architecture will be provided and then the detailed description of the underlying exploration algorithm will follow.

A. Tool Overview

The FormalSpecs Verifier (FSV) is a framework for the verification of complex embedded systems. The core of the tool is based on a translator from a Simulink model to the NuSMV tool native language [START_REF] Ferrante | Parallel nusmv: a nusmv extension for the verification of complex embedded systems[END_REF]. The transformation process produces a semantically equivalent NuSMV representation of the input model taking into account the non-determinism resolution that may be introduced during the transformation step. For the execution of the Fault Analysis the FSV tool has been enriched with additional modules that implement part of the flow described in Section III. The enrichment covers in particular the automatic generation of the Error Model and the algorithm execution, summarized as follows: the tool translates a Simulink model to an internal format performing a model transformation step. The model is then processed by a second transformation that enriches each component with faulty behaviours taking into account the specification of the failure modes provided by the user obtaining a NuSMV model that can be processed by the internal formal engine.

B. Algorithm Description

The tool supports fixed-step discrete time Simulink models. A nominal model is formalized as a function F [u, x, f , k] that at each discrete time k maps inputs u[k] and current state x[k] vectors to a vector of outputs y[k] and next-state values x[k + 1]. The error model is produced by enriching the behaviour of the nominal model with the failure mode functions: for each component's failure mode an additional input variable, called the failure mode enable input, is created. Let F = {f 1 , . . . , f N } be defined as the set of all the failures added to the model: a failure enable input is a discrete-time Boolean function f j [k] that is TRUE if the failure f j is active at the k -th step, FALSE otherwise. The error model is then modelled as a function over the discrete time F [u, x, f , k] where f is the vector of failure mode enable inputs. In case the latter is a constant vector of false values (identified as 0) we have that F [u, x, 0, k] = F [u, x, f , k]. In other terms, in case all failures are disabled, the nominal and error models are equivalent. Finally, the Top-Level Event is modelled as a Boolean function over discrete time H[k] that is TRUE if the TLE occurs at time step k, FALSE otherwise. For the execution of the failure scenario generation algorithm additional variables called monitors are introduced. Each monitor is a Boolean function over the discrete time m j [k] such that m j [k] is TRUE if there exists a step i ∈ [0, k] for which the failure enable input f j [i] has been TRUE, and it is FALSE otherwise. In other terms, each monitor is associated to a failure enable input that goes and remains to TRUE if the corresponding failure input has been TRUE in the past or in the current step. Our fault analysis algorithm (Algorithm 1) loops until a given discrete time limit bound provided by the user is reached (line 2). At step 3 the formal engine searches for a counter example that, at the given time step k, both minimizes the sum of the values of the monitors m 1 , . . . , m N and verifies the hazard predicate H[k]. The counter example is obtained iteratively by applying bounded model checking on the error model taking into account the dynamic behaviour of the SoC. Notice that the use of BMC in conjunction with a parallel SAT solver allows for successful application of the technique to real-life industry sized models. The minimization procedure ensures that only a minimal number of failures are injected to trigger end if 11: end while the TLE. If a counter example is found, then the monitor values configuration is extracted and a new constraint is added to the model in order to exclude the found configuration from future searches (lines 5 and 6). The test case is extracted from the counter example storing inputs, outputs and internal variables of the system (lines 7 and 9). The loop is executed again to look for additional minimal possible monitor configurations until no more configurations can be found. The algorithm ensures that (1) every failure enable set produced is a minimal critical failure set for the TLE under analysis and (2) it is true by construction that there are no two traces exposing the same minimal critical failure set.

VI. APPLICATION TO THE REFERENCE EXAMPLE

The failure scenario generation methodology has been applied to the eTPU case study described in Section II using the FSV-FA toolset. A total number of 45 faults have been modelled in MATLAB Simulink using a predefined library. The simulation time was limited to k = 28 steps for a waveform with period p = 100 and active time a = 25. After 60 minutes of computation 5 failure scenarios have been found using a platform based on an Intel i7 2.4 GHz with 8 GB of RAM. One of the 5 property violations was observed at time step k = 2, while the other four occurred at time step k = 28. Fig. 7 reproduces one of the generated scenarios. The TLE has been modelled as the Simulink subsystem shown in Fig. 4; referring to the failure scenario shown in Fig. 7 such a TLE is activated when a stuck-at-one fault affects the output pin of the eTPU channel (Pin Out). In order for the property to be violated, the fault is to be active from the beginning (k = 0). The lower sub-plot of Fig. 7 shows the value of the output pin (an output of PWM OUT HW in Fig. 1) and the value of the Flag signal (an output of PWM OUT SW in Fig. 1). The Flag signal is a local variable of the PWM OUT SW machine set to zero when the software is expected to be handling the hardware state "pin high" of PWM OUT HW, and set to one when the software is expected to be handling the state "pin low" of PWM OUT HW. At the init time (k = 0) the eTPU software sets the output pin value to zero (Flag=1), the "next match" to occur at time k = 1 and the action related to the match event to "set pin high". The pin is stuck at one all the time, in particular from the beginning of the simulation. The expected sequence of events is the following: at time k = 1, the pin should transition to 1 and at time k = 2 the value of Flag should transition to 0, representing a change in state of the eTPU software FSM (PWM OUT SW). Since the stuck- at-one fault prevents the pin from changing, the property is violated and the TLE activtes.

VII. CONCLUSION

In this paper we presented a model-based methodology for the automatic generation of failure scenarios. The methodology has been applied to the analysis of a SoC architecture using a Simulink-based tool that implements a novel algorithm based on bounded model checking exploiting the recent advances of parallel SAT solving. A concrete SoC use case has been proposed to show the effectiveness of the described approach. In future work we will apply the presented methodology to more complex Systems-on-Chip models. In particular, we are interested in evaluating the effectiveness of cross-layer dependability mechanisms employed in safety-critical SoCs. Cross-layer dependability mechanisms allow distributing the fault/error detection phase and the diagnosis and handling phases across the whole system stack, thus reducing production costs. To this purpose hierarchical models of the various hardware and software abstractions (e.g. gate, circuit, hardware architecture, firmware, operating system, middle-ware and application) will be developed, exercised and analysed with the proposed methodology.

Fig. 1 .

 1 Fig. 1. Top-level view of the HW/SW composition.

Fig. 2 .

 2 Fig. 2. Functional model of a stuck-at-value.

Fig. 3 .

 3 Fig. 3. Representation of one of the two action units in PWM OUT HW FSM as a Statechart in Simulink/Stateflow.

Fig. 4 .

 4 Fig. 4. Functional specification of the top-level event (TLE).

Fig. 6 .

 6 Fig. 6. Tool Overview.

Algorithm 1

 1 Fault Analysis Algorithm 1: Initialize bound: k ← 0 2: while k < M AX BOU N D do 3: find a counter example s.t. m 1 [k] + m 2 [k] + . . . + m N [k] is minimal and H[k] is TRUE 4: if counter example exists then 5: define m * = [m * 1 , m * 2 , . . . , m * N ] the found monitor configuration 6: exclude m * from the admissible solutions of the future searches 7:extract input and failure enable values from the found counter example and store as a failure scenario

Fig. 7 .

 7 Fig. 7. Analysis Results.

ACKNOWLEDGMENT The research leading to these results was partially funded by the EU ARTEMIS Joint Undertaking under grant agreement n. 269335 MBAT and the Italian Ministry of Education, University and Research (MIUR) and by European Commission for funding the Large-scale integrating project (IP) proposal under the ICT Call 7 (FP7-ICT-2011-7) DANSE (Contract Number: INFSO-ICT-287716).


Subeer Rangra
email: subeer.rangra@edu.esiee.fr

Emmanuel Gaudin
email: emmanuel.gaudin@pragmadev.com

SDL to Fiacre translation

Keywords: Model Checking, Formal Methods, SDL, MSC, Fiacre, TINA 1

The translation of a system model to an intermediate format is an important step towards formal proofs of properties. This paper presents the formulation of rules to enable the translation of SDL standard models to Fiacre language. The translated model is then provided as input to a suitable toolset that performs model checking and other analysis. The formulated translation rules are discussed in view of the correctness of translation and ease of implementation. Implementations of some of the translation rules in an industrial tool (PragmaDev RTDS), and a proof of the concept on a simple SDL model are presented to ascertain the validity of the proposed translation.

Introduction

Validation of software is a major concern in the domain of software engineering. Currently, industries engage their efforts in testing and simulation processes. The coverage of the test sets decreases gradually as modern day embedded systems increase in complexity. Under such circumstance, it becomes necessary to use new methods to ensure the reliability of software.

Over the last two decades, model checking has emerged as an attractive approach for ascertaining the correctness of control computer based systems. Model checking is a formal verification technique which allows for desired behavioral properties of a given system to be verified on the basis of a suitable model of the system through systematic inspection of all states of the model. [START_REF] Baier | Principles of Model Checking[END_REF] The approach of formal verification is not limited to any domain and can be used in multitude of scenarios where a formal proof or validation of a system is required.

In order to formally verify a design, it must first be converted into an appropriate format. This can be accomplished after needed transformations from a user defined model described in a precise modeling language such as SDL. In the context of this work, we focus on porting SDL models to a pivot language called Fiacre. This can then be used by various toolsets to perform various analyses or verify the system.

All through the development cycle of the Fiacre language there have been various translations from many DSMLs (Domain Specific Modeling Language). One such translation to SDL has been done at LAAS-CNRS [START_REF] Saad | Schema de Traduction SDL vers Fiacre[END_REF], with an aim to translate SDL to Fiacre. The present paper differs on many levels. First, the work reported in [START_REF] Saad | Schema de Traduction SDL vers Fiacre[END_REF] was performed in the very early life cycle of Fiacre language and one of the aims of the translation was to build Fiacre language itself. Second, it did not aim to enable the formal verification of the model in SDL. The focus was to translate the language schematics, which is one of the two main goals of present work. We also aim for the translation to be able to verify the system and for the results to be easily interpretable. Further, the implementation of such a verification tool chain in an industrial tool like PragmaDev Real Time Developer Studio will enable industries to use formal methods in real world scenario.

The translation and subsequent formal verification is a rather complex problem in itself and may cause issues ranging from the state space explosion problem, inability to conserve the semantics and incomprehensibility of verification results due to different formalisms used. Therefore, for the sake of correctness and simplicity a fresh approach is necessary. Also, in this domain of formal verification of SDL with the use of Fiacre, published literature is very limited. Similar model transformations from other languages to Fiacre do exist but this particular translation opens another bridge to formal verification of SDL models.

In this paper, brief introduction to SDL and Fiacre is given in Section 2. Section 3 presents various translation rules concerning the selected notions of SDL. Section 4 briefly describes the encoding of these translation rules in PragmaDev RTDS. Section 5 covers the proof of concept, accomplishing a two part goal, first that the proposed translation works and produces an accurate translation of the system, and second that the system can be correctly verified by the use of a verification tool.

SDL and Fiacre

Specification and Description Language (SDL) [START_REF]Specification and Description Language -Overview of SDL-2010[END_REF] is a formal language standardized by the International Telecommunication Union (ITU-T) as the Z.100 recommendation. It can be used easily in combination with other languages, such as SysML or AADL. It is an object-oriented language, created to describe complex, event-driven and interactive applications involving many concurrent activities and communicating with each other through messages. SDL is often used in combination with MSC (Message Sequence Charts), which is a graphical and textual notation for the description and specification of the interactions between system components. It helps in better visualization of the messages that are being exchanged in the system internally and with the environment. The objectives of SDL include a language that is easy to learn, use and interpret, while implementing a precise system specification and description. The five main aspects to formally model the system e.g. structure, behavior, communication, data, and inheritance make SDL a favorable candidate amongst the various DSMLs currently used in system modeling to describe an executable model. While SDL former versions presented difficulties in dealing with some of the Real-Time embedded concepts, SDL 2010, the latest release, inspired by SDL-RT [START_REF]Specifications and Development Language-Real Time[END_REF], provides the required balance between the high level concepts of SDL and technical effectiveness of C code in dealing with such systems. FIACRE [START_REF] Berthomieu | The syntax and semantics of Fiacre[END_REF][START_REF] Berthomieu | Fiacre: an Intermediate Language for Model Verification in the TOPCASED Environment[END_REF] stands for "Format Intermédiaire pour les Architectures de Composants Répartis Embarqués", French for "Intermediate Format for the Embedded Distributed Component Architectures". It is an intermediate format language formally defined for representing both the behavioral and timing aspects of embedded and distributed systems for formal verification and simulation purposes. It was defined as a pivot language to provide gateway for the Domain Specific Modeling Language (SDL, SysML, AADL etc) into the domain of formal verification supported by tools such as TINA, CADP and OBP.

Fiacre was designed and developed in the framework of several projects, involving industry and academic partners, such as TOPCASED [START_REF] Topcased | Toolkit in OPen-source for Critical Applications and SystEms Development[END_REF], the VASY project of INRIA [START_REF]VASY Validation of systems[END_REF], VerTICS Team [START_REF]VERification des Systèmes Temporisés CritiqueS[END_REF] of LAAS-CNRS, and the ACADIE team [START_REF]Assistance à la Certification d'Applications DIstribuées et Embarquées[END_REF] of IRIT. This multi-team development has led to the creation of Fiacre as a pivot language. Thus giving it a clear advantage of being able to easily translate, and then provide formal verifications in a variety of different model checking tools [11], developed by these teams. Some modified versions of Fiacre have been proposed to help writing generic libraries of protocols, for example communication and scheduling protocols used by the AADL runtime [START_REF] Bodeveix | On the Mechanization of an AADL Subset[END_REF]. Examples of translation and verification such as AADL to Fiacre [START_REF] Berthomieu | Transformation de modèles UML vers des programmes Fiacre[END_REF], done under the framework and context of TOPCASED project, are available. Attempts have also been made to make translations from UML to Fiacre [14]. Projects such as Quarteft [15] aim to improve the usability of Fiacre by proposing real time extensions among other things. Extensions like various real-time constructs and real-time verification patterns have been proposed in [START_REF] Abid | Real-time Extensions for the Fiacre modeling language 17[END_REF]. Methods have also been proposed to make Fiacre more useful in itself, for example the feedback of verification results from model checking tools [17].

There are three toolsets that accept a Fiacre description and are briefly mentioned as follows. The very development life cycle of Fiacre ensured that these tools can be used with a Fiacre file as input and the required transformations and analysis be carried out.

TIme petri Net Analyzer (TINA) [START_REF] Berthomieu | The tool TINA -Construction of Abstract State Spaces for Petri Nets and Time Petri Nets[END_REF] is a toolbox for editing and analyzing Timed Petri Nets [START_REF] Merlin | Recoverability of communication protocols: Implications of a theoretical study[END_REF]. TINA works with Timed Transition Systems (TTS) [START_REF] Henzinger | Timed Transition Systems[END_REF], a generalization of Time Petri Nets with data variables and priorities. TINA employs a State/Event LTL model checker [START_REF] Chaki | State/Event-Based Software Model Checking[END_REF] in the form of a tool : selt. Construction and Analysis of Distributed Processes (CADP) [START_REF] Fernandez | Mihaela Sighireanu CADP A Protocol Validation and Verification Toolbox. 23. Information processing systems --Open Systems Interconnection --LOTOS --A formal description technique based on the temporal ordering of observational behavior[END_REF] is a toolset that accepts high-level protocol descriptions written in the ISO language LOTOS (Language Of Temporal Ordering Specification, ISO 8807) [23]. Observer-Based Prover (OBP) Toolset [START_REF] Obp-Cdl | Lab STICC[END_REF] is an implementation of CDL (Context Description Language) [START_REF] Dhaussy | Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation[END_REF][START_REF] Dhaussy | Improving Model Checking with Context Modeling[END_REF] developed at ENSTA-Bretagne. It is a modelchecker based on observers and context descriptions.

Advantages regarding the usage of Fiacre lie in its ease of translation to a format or language used by these verification tools. Binaries can be used (viz. flac (CADP), frac (TINA)) or there are meta-models available in Eclipse environment [START_REF]Signal metamodel to Fiacre metamodel[END_REF][START_REF]ATL Use Case -Compiling a new formal verification language to LOTOS[END_REF] to perform the required model transformation.

Formulating the rules

The disadvantage of any intermediate or pivot language is that each step of retranslation introduces possible mistakes and ambiguities. Using a pivot language involves at least two translation steps, one from the model to the pivot language and another from the pivot to the final abstraction. A simple and fresh approach is hence necessitated.

The translation rules we present here aim to satisfy the following main points:  The semantics of SDL are preserved.  The verification of the system using one or more toolsets mentioned above is possible.  The verification results are observable to the very least.

To comply with the above points, a full translation of SDL is not mandatory; focusing on some selected SDL semantics help in getting initial results faster. Once the initial proof is accomplished the addition of more exhaustive rules is comparatively an easier task.

Architecture

SDL supports a hierarchical structure with blocks and processes connected with channels. Blocks are structuring elements that do not imply any physical implementation on the target, rather are used to represent hierarchical structures; processes are used to describe their functionality.

As there are no constructs except the process and component in Fiacre, a few propositions are made in this work to retain some structural aspects of SDL, which can be obtained from the configuration of Fiacre data structures and component. Fiacre components allow for a hierarchical structure of the system to be defined and the processes describe the behavior of sequential components. Processes cannot contain other processes while components can contain other components enabling recursive specifications.

A few propositions which use components to give a hierarchical notion to a system in Fiacre are given in Table 1. In this translation rule the SDL system name forms the name of the main Fiacre component and is called first when a Fiacre file is compiled.

Components can declare local variables to be passed to sub-processes (or sub-components). All the shared variables and labels must be declared and initialized inside the component that they are being used in. This structure is used to define the internal structure of a single block or even a system in which the processes or procedures are all communicating among themselves. The par...end structure is the composition operator which describes what labels are to be synchronized with among the enclosed elements. This along with the right use of component can be used to represent a hierarchical structure in Fiacre. As explained by the use of a hierarchical SDL structure given in Figure 1. The above SDL hierarchy represents relation between agents and procedures in a system. A structure representing an SDL system is illustrated in top left of Figure 1 (let's call it SystemExample), the rest are the internal hierarchical structure represented by the use of blocks (Block1, Block2) and processes inside those blocks. The textual description below (Pro-cess2) is a process definition that is written in Fiacre when defining a process.

_________________________________________

Using * denotes universal label sets in Fiacre, such that all the labels in use are shared between the processes, this can be changed to selectively synchronize different SDL processes.

Unlike SDL there is no special provision for an Environment variable in Fiacre. An accurate definition of the system is needed to have an exhaustive and mathematically correct verification. This presents a problem as to whether make a custom translation and build an environment process automatically, by looking at all the communications of the processes with the Environment; or on the other hand ask the user to model a process which accomplishes what the user needs the environment to do (generally send initial signals to start the system, input or output messages). The conclusion was drawn that for the translation to remain true to the nature of the original system, it is better to ask the user to model an environment process, rather than modeling one automatically in the translation. This way the user can be certain of the system being correct to his specifications and we get a closed system for the needed abstraction.

Communication

Messages, processes and their associated message queues are fundamental SDL constructs to enable communication. Fiacre has ports/labels as modes of communication which offer synchronous communication, however these are not used, as SDL communication is asynchronous. Instead, in this context shared variables are used as a user defined data type to keep communication asynchronous in Fiacre. A shared variable also gives a way to work around the Fiacre's single communication rule which states that at the most only one interaction label can be used along any execution path.

The idea of message passing among processes is translated and implemented as part of the proof of concept. Each process has a message queue of its own processQueue which is initialized at the beginning of the program. The message information is stored in the message queue as an enumerated type of all the possible message names in the system. All the queues are stored in an array messageQueueArray. The array contains each of the process queues (indexed by a constant integer value associated with each process). This array is a globally shared variable. It can be accessed by the processes which in turn can access the queue of the relevant process to send messages and also their own queue to read messages. This queues and array construct is shared as references because Fiacre variables can only be shared among several processes if passed by reference. This method is valid in the present context, for the limited scope of this translation it is an acceptable compromise to reduce complexity.

Translation of the communication aspects of SDL are presented through a simple example which has two processes: pProcess1 and pProcess2, communicating by passing messages message1, message2 between each other as given below and shown in Figure 2.

_____________________________________________

State Machines

The dynamic behavior of the system in SDL is described in the processes through extended FSMs (Finite State Machines), communicating with messages. A process state determines what behavior the process will have upon reception of a specific message. Fiacre allows for simple state declarations and we have used a prefix to denote the start state and differentiate it from other state declarations. Stop state of SDL is not translated because such a state will inevitably lead to a deadlock preventing an exhaustive analysis of the system.

States are declared inside a process as states RTDS_start, state1. Transitions from one state to another in Fiacre is a simple structure of from <initial_state> followed by the operations and conditions ending with to <final_state>. _____________________________________ from state1 // TRANSITION BODY to state2

_____________________________________

The start state in SDL is translated into a simple state (RTDS_start) in Fiacre with no conditions in the transition. This allows for automatic initialization of the process transitions and aids in translating concept of modeling the environment process as explained in Section 3.1.

Fiacre has two types of decision statements:

 non-blocking (if-else), if the optional else branch is omitted the control is passed to the statement following the condition. Table 2 gives a simple decision statement translation into if-else condition in Fiacre.  blocking (select, case, on, where) in which if no match is found, then the construction is blocking: no transition is possible through that statement.

Data types

Fiacre only supports three standard data types (integer, natural and boolean) but complex data types if needed can be created with records and unions. Such elaborate data type declaration constructs allow for easy translation of predefined data types in SDL.

In SDL, the index type for an array can be of any type. However in Fiacre, only numeric indices between 0 and an integer value are supported. Thus SDL arrays only based on an integer index type with 0 or a positive value as lower bound can be translated. The translation rules for various data types that are used in SDL are given as in the Table 3. RTDS parses the SDL model and generates an Abstract Syntax Tree. All export mechanism and code generators in the tool are based on this Python AST. The above mentioned rules were written in a Python class. This allows for automatic and accurate generation of a Fiacre file that can either be exported for manual use or coupled with a shell script to be given as input to the desired verification toolset. The verification using TINA performed in the proof of concept uses the shell script that can be customized to use the various tools of TINA on the generated Fiacre file.

Proof of concept

Using TINA and the translation rules coded in the PragmaDev RTDS, a simple SDL example given as follows is verified against some properties.

This example system in SDL comprises of four processes and six signals namely go, m2 (message2), m3 (message3), m2f (message2Forward), m3f (mes-sage3Forward) and done. The environment process initiates the system to begin by sending message go to pProcess1. pProcess1 upon receiving go, sends out m2 and m3 to pProcess2 and pProcess3 respectively. pProcess3 on receiving m2 forwards a message m2f to pProcess4. Similarly pProcess3 upon receiving m3 sends out m3f to the pProcess4. Now pProcess4 is where we have two messages arriving namely m2f and m3f. Only when the messages are received in this order, pProcess4 forwards a message done to the environment process. In other cases we have the system not emitting done even after a go was sent.

Figure 3 is an MSC diagram of the system described above that shows the sequential flow of messages between the environment process and the four processes described above.

Expectations. One important aspect of SDL i.e. asynchronous message passing is tested in this example. The goal is to check that every time the messages go is sent by the environment process, it is not guaranteed to receive the message done. We expect the property stating as such to be false when verified. It also allows one to observe the translation and see if the schematics of SDL were preserved and there are no errors in the automatically generated Fiacre file.

The MSC trace of this system in Figure 3 is inconclusive as to whether the properties that we are verifying are true or false in all possible executions of system.

Fig. 3. MSC of our example system

Once generated, the path we take here to verify our Fiacre system description with TINA is as follows:

1. frac analyzes a Fiacre description and compiles it in a Time Transition System description (extension .tts) suitable for analysis with the TINA tools. 2. tina (tool) constructs the reachability graphs by generating the state space of a TTS in the ktz format, which is a compressed, binary format for Kripke transition systems. 3. selt which is a State/Event LTL model checker checks the Kripke transition systems built in the previous step, against S/E LTL formulae.

All of these tools are called by an external shell script that runs these commands in order to give the correct files as inputs to the appropriate tools.

5.1

Properties for verification

To perform model checking using TINA we need to write properties. All Fiacre items are observable (states, local variables, events); all the information of a Fiacre description is available for model checking by writing properties in LTL. One way to write properties is inside the Fiacre file and another is in the command line of selt (for the TINA tool used in this case). We chose to add the properties to the generated Fiacre file for this demonstration as it is easy to understand and write from the user's perspective.

The properties are written in Fiacre format [29]. Properties are defined from observables (or probes); the languages of properties include LTL properties, Dwyer et al. patterns [START_REF] Matthew | Property Specification Patterns for Finite-state Verification[END_REF].

The following property checks if there are any deadlocks in the system. _____________________________________________ property ddlf is deadlockfree assert ddlf

_____________________________________________

The second property says that receiving go in Pro-cess1, leads to done received in pEnv, which behaves as the environment process that we have modeled. _____________________________________________ The properties and observables given as input to selt must be in the format of place or transition identifiers. If one choses to write properties in the Fiacre format (as in this case) they are automatically converted to appropriate format for use in selt by the frac compiler.

Results of the verification

The selt tool generates the following output which is a transitional description (scn format) leading to the case where the properties are being violated. ___________________________________________

_____________________________________________

The operator ddlf is the property where we verified the system to be deadlock free. The result is FALSE. This signifies the existence of a deadlock in the system. _____________________________________________ operator goLeadsToDoneState : prop 0.000s # [] (pProcess1_1_sidle => <> pProcess4_1_sidle) |-FALSE pEnv_1_t0 pProcess1_1_t0 pPro-cess1_1_t1 pProcess2_1_t0 pPro-cess2_1_t1 pProcess3_1_t0 pPro-cess3_1_t1 pProcess4_1_t0 pPro-cess4_1_t3 pProcess4_1_t1 pEnv_1_t1 pProcess1_1_t1 pProcess3_1_t1 pPro-cess2_1_t1 pProcess4_1_t4 pPro-cess4_1_t3 # loop accepting 0.000s _____________________________________________ The result for the second property namely goLead-sToDoneState is also shown here to be FALSE, as expected. Because of asynchronous message passing in SDL, the messages might not maintain their order. This output not only gives the TRUE/FALSE result of verification, but also prints out a counter example of the transitions in the system (TTS description), which is the series of transitions taken that led to the aforementioned property being violated. On closer observation of these series of events, it was found coherent with our expectations; the conflict arose because of the order of messages (received by pProcess4), not being maintained as required. It is generated from the description format of the Aldebaran tool of the CADP toolset, using nd editor supplied inside TINA. The last transition on the left-bottom is a deadlock and also the second property that we verified is being falsified here. The transition sending a done message back from pProcess4 is absent here hence the deadlock. The above results not only prove the correctness (although in limited context) of the translation rules, but also established that TINA is capable of adequately perform model checking with our automatically generated Fiacre file.

Discussion

A custom Start state was added in the Fiacre description as an empty transition to translate the SDL's semantics appropriately. In the process of this change it was discovered that only by adding a simple state which simply points to the first state of the process; the total number of states in the transition system changes drastically causing a state space explosion problem. This kind of problem is rather expected while using a formal method like model checking. Hence, for any future work this needs to be addressed in an appropriate way.

A loopback for analysis of the verification results has not been implemented as part of this paper. It was originally proposed to have the verification results generated in a graphical representation, preferably in the form of an MSC, as it is often used with SDL. This would be an added advantage, as the user would not need to know the inner working of the verification tool chain; the results shall be displayed in close representation to the original SDL model making them easier to understand.

The problem seems to be that the output of the verification results have gone through too many translation themselves that it was difficult to understand what the counter examples generated by selt represented in SDL or even in Fiacre terms.

Manual parsing allowed verifying that the results were in fact correct. But parsing them line by line, referencing back not only through the generated Fiacre file but the TTS format; was not only a complex task and needed more time, but the risk of introducing errors also ran high. This was due to the fact that the counterexamples produced by selt are at TTS level rather than at Fiacre level, representing transitions from one state space to the other. The messages that are pushed on to the message queues also have a different representation in the TTS description.

Such problems are a part of using a complex tool chain in which multiple transformations of the system description take place not only in terms of the language used but semantic changes as well. The major importance of messages in SDL does not translate well when dealing with transition systems impacting the ability to observe, verify and write accurate properties for verification. Any future work hence needs to focus on such issues and address them carefully, in order not only to have a feedback of some sorts but also to ensure an accurate translation.

Conclusion

In this paper we discussed the rules to translate standard SDL models to the Fiacre language. Their implementation in PragmaDev RTDS has also been achieved as part of an internal version of RTDS due to the very limited scope of this translation. With some of the propositions presented here, it can very well be released as part of PragmaDev RTDS to those interested.

A fresh and simple translation scheme has been adopted in this work to keep the original semantics and easy interpretation of transformations. However, further additions if required can easily be done to further enhance the SDL support. Verification with TINA done as part of proof of concept generated the results as per expectations establishing evidence that the translation does not add any unnecessary ambiguities and is correct. The whole chain of model checking the system with TINA works satisfactorily.

The feedback of the verification results was investigated but the semantic difference between different translations the system went through would require a substantial amount of work to implement. There is ample scope to investigate further with TINA or other toolsets to understand various formalisms they embody, properties they use and the results that they generate to arrive at a robust verification tool chain for system models defined in SDL.

The proof of concept presented in this paper has a flash demonstration with the internal build of RTDS, which is available on PragmaDev website. It is a screen-capture of the whole process from the SDL model in RTDS down to verification results using TINA.

[http://www.pragmadev.com/product/viewlet/FIACRE/ fiacre_viewlet_swf.html]

Fig. 1 .

 1 Fig. 1. A hierarchical structure in SDL

Fig. 2 .

 2 Fig. 2. Message passing in SDL __________________________________________________

Fig. 4 .

 4 Fig. 4. selt tool of TINA

Fig. 5 .

 5 Fig. 5. Graphical view of Kripke Transition system

Table 1 .

 1 SDL architecture to Fiacre component

	SDL	Fiacre
	SYSTEM system_name; component sys-
		tem_name is
	BLOCK block_name;	component
		block_name is
		par * in
		.
		end
		end Block1
	PROCESS process_name; process_name()

  The component structure is just used to call them with appropriate arguments.

	end Block2
	//SystemExample IS CALLED
	SystemExample
	_____________________________________________
	component SystemExample is
	component Block1 is
	par * in
	// PROCESS1 IS CALLED
	// PROCESS2 IS CALLED
	end
	end Block1
	component Block2
	par * in
	// PROCESS3 IS CALLED
	end
	par * in
	// PROCESS4 IS CALLED
	end

Table 2 .

 2 Condition statements translation to Fiacre

	SDL		Fiacre
	DECISION cond;
	(true):	if cond then
	/* action1 */		/*action1*/
	(false):		else
	/*action2*/ ENDDECISION;	end	/* action2*/

Table 3 .

 3 Data types translation rules

	SDL	Fiacre
	SYNONYM maxCount	const maxCount :
	integer = 3;	int is 3
	DCL	var v int,
	v integer,	var b bool
	b boolean,	//Can be declared
		and initialized as
		var b : bool:=
		false;

ACKNOWLEDGEMENTS

We acknowledge the support from ESIEE especially Associate Prof. Yasmina Abdeddaïm for proofreading and help in placement at PragmaDev. Help from Mr. Bernard Berthomieu (LAAS CNRS) regarding literature and discussion on Fiacre and TINA were crucial to this work. Inputs from Mr. Philippe Dhaussy (ENSTA-Bretagne) are also greatly appreciated.


Alexandre Cortier

Marie-Hélène Deredempt

Jacques Seronie-Vivien

Jean-François Rolland
email: jean-francois.rolland@atos.net

François Bossard
email: francois.bossard@cnes.fr

Modeling On-Board Software Dynamic Architecture: A Related Experience using UML-MARTE

Keywords: OBSW, UML, MARTE, dynamic architecture, computational model, use case

MARTE (Modeling and Analysis of Real-Time and Embedded Systems) is the UML extension profile dedicated to the modeling of

) the lack of experiences relating to the use of MARTE on realistic and operational system in space domain. This paper presents an experience of using UML-MARTE to model the dynamic architecture of an operational space On-Board Software (OBSW) to make a step towards the adoption of UML-MARTE. The modeling methodology adopted in this study is illustrated by a use case based on an operational OBSW.

INTRODUCTION

Objectives of dynamic architecture modeling. The expected benefits of modeling dynamic architectures are to bring capabilities of:

-Providing an unambiguous communication support and an unambiguous expression of requirements and architecture; -Supporting the use of automated documents generation (as for instance SW-ADD document as required by ECSS standards in space domain); -Supporting the use of analysis tools, especially schedulability and performance analysis tools; -Supporting the use of automated code generation.

Encapsulating in a unique model the necessary information to bring these capabilities is a precondition for the adoption of an operational modeling methodology because it allows ensuring the coherency between documentation, analysis and generated code. In the scope of this study, we focus our effort on defining a dynamic architecture modeling strategy which allows handling the three first objectives. Although the use of automated code generation still requires additional investigations, the adopted modeling strategy and produced models have been conceived by keeping in mind this capability.

UML-MARTE.

The UML-MARTE [START_REF]UML Profile For MARTE: Modeling And Analysis Of Real-Time Embedded Systems[END_REF] notation has been chosen to support our modeling strategy for three main reasons. First, this profile extension for the modeling of real-time systems is a wellaccepted OMG standard which provides support for specification, design and verification/validation stages. The second reason is the existing of Open Source modeling platforms and model editor which support customization features (Topcased platform and Papyrus editor in this study). The last reason is a more specific one and relies on the internal experience of Astrium: UML is already used in operational projects to model the static architecture of the OBSW. These models are used for automated documentation and code generation. In this context, the MARTE solution was the most adapted to ensure a consistency in terms of modeling techniques used in a global design process, and to ensure traceability of modeling artefacts.

Organisation of this paper. This paper proposes in section 2 an overview of the methodology used to model the dynamic architecture of an operational system. Section 3 presents in details the formalization of the computational model used to model the dynamic architecture. Notice that MARTE is mainly used for the description of this computational model: other sub-models and diagrams make a sporadic use of MARTE concepts. Section 4 presents how to capture the dynamic architecture of the system by instantiating the computational model entities. Section 5 briefly discuss about the use of this model for schedulability analysis. To conclude, section 6 gives some feedbacks on the use of MARTE and associated tooling.

MODELING METHODOLOGY OVERVIEW

The Figure 1 presents the model organisation which supports the adopted methodology. 2. The Hardware Platform model describes the hardware part of the system. The hardware execution platform is formalised using the MARTE Hardware Modeling Resources sub-profile (HRM). In the scope of this study, the main purpose was to evaluate the use of MARTE for schedulability analysis purpose. As the use case was very simple (mono-processor), notice that this model as well as the deployment model is not very useful here for the schedulability analysis. For this reason, this model will not be discussed in the following.

The Clocks Definition package allows modeling the full clock hierarchy of the system using the MARTE Time profile. The Time Expression language of MARTE allows to formally defining the clocks tree of the system by specifying the clock derivation constraints from one clock to another.

The Dynamic Architecture describes the run-time instances of the system: tasks, synchronizations, protection mechanisms for shared resources… All entities defined in the dynamic architecture are instances of the basic entities defined in the Computational Model view.

The Deployment package allocated application components on hardware platform component. This view will not be detailed in this paper.

COMPUTATIONAL MODEL

The modeling of dynamic architecture and its use for schedulability analysis is intrinsically related to the Computational Model on which it relies. A computational model describes how computations are carried out in a system by prescribing the form of legal basic entities and their associated properties in the dimension of execution and synchronization, in time and space, of run-time entities. A computational model is significant and useful if:

1. It can be related to analysis theories such as schedulability analysis theory for instance;

2. It can be related to a Programming model which allows to convey the implementation of the dynamic properties statically asserted by analysis and so allows automated code generation perspectives;

3. It is compliant with services offered by the operational system.

Formal analysis tools rely on well-defined computational model such as the Ravenscar profile [START_REF] Burns | The Ravenscar tasking profile for high integrity real-time programs[END_REF] which allows performing Rate-Monotonic Schedulability Analysis (RMA). However operational project uses rarely this computational model in concrete implementation. Keeping in mind the related objective to exploit the produced models at ends of code generation, the modeling strategy adopted in this paper relies on an explicit modeling of an operational computational model. This computational model is then a re-usable resource package which defines the types of dynamic entities to be used to describe the dynamic architecture of the OBSW. UML-MARTE is principally used for this purpose.

As a consequence of this strategy, a transformation has to be defined to produce a model which can be analysed by existing analysis tool. This transformation needs to be formally defined to ensure that the source model relying on the operational computational model is equivalent to the transformed analysis model. The Figure 3 shows the translation of the Astrium Computational Model in MARTE::SRM. Each core elements of the computational model has been successfully mapped onto MARTE::SRM except the Execution Block concept. The stereotype << NFP>> which stands for non-functional property has been used to add the significant properties of this concept: the execution duration and the deadline of the pure sequential piece of code. The meaning of each MARTE stereotypes is not the purpose of this presentation : more information is available in the MARTE standard.

DOMAIN MODEL: CORE ELEMENTS

Notice that this model has to be done once and can be used as library artefact in others dynamic architecture models which relies on the same computational model.

CLOCKS DEFINITION

According to the computational model defined in the previous sections, periods of cyclic tasks are implicit in our model. This period attribute can be derived from the referenceClock property of the Periodic Synchronisation which releases the task.

The clock tree hierarchy of the system is formalized using the MARTE::Time sub-profile. The first step is to define a type of chronometric clock. Then, all clocks are derived from the ideal clock using clock constraints. The Figure 4 presents a part of the clocks hierarchy defined in the AS250 case study.

Clock constraints are formalized using the Time Expressions package of MARTE. For instance, the fastest 16Hz clock is defined using a clock constraint which stipulates the discretization step (62.5ms) and the stability of the clock. The other clocks (8Hz, 4Hz) are defined by under-sampling of the fastest clock. The "aocs_avb_end_acq" clock is defined has a 16Hz periodic clock with a 13700 us phase.

DYNAMIC ARCHITECTURE MODELING

Once the modeling of the computational model has been done, the dynamic architecture can be formalized. This model is defined in three main steps as described in the following sub-sections.

Identification of Execution Blocks

The first step is to identify the execution blocks of the system. High Level Execution Block (HLEB) and Basic Execution Block (BEB) are identified in a UML Class diagram using a generalisation link pointing to HighLevelExecBlock and BasicExecBlock entities defined in the computational model. Lock instances which models mutual exclusion constraints are represented in the same way.

Tasks. As stated in section 3.2, a task is linked to a high level execution block which catches its execution flow. This link is represented in the same composite diagram. In the example provided in OCL structural constraints have to be defined on activity diagrams to ensure that called operations are in the scope of visibility of the execution block as specified by the composite diagram and the structural rules previously defined. Figure 8 shows the activity diagram associated to the AOCS_CYCL High Level Execution Block.

SCHEDULABILITY ANALYSIS

The model presented in this article describes a dynamic architecture and temporal constraints. We want to check that these constraints can be matched by the architecture. To achieve this validation, we want to use the model as an entry point for a scheduling analysis tool. As it is a common approach different studies have proposed a mapping between MARTE and a scheduling analysis tool: from the GRM to Cheddar [START_REF] Maes | MARTE to Cheddar transformation using ATL[END_REF], from SRM to Cheddar [START_REF] Thomas | Contribution à la prise en compte des plates-formes logicielles d'exécution dans une ingénierie générative dirigée par les modèles[END_REF] and from SAM to MAST [START_REF] Medina | From composable design models to schedulability analysis with UML and UML profile for MARTE[END_REF].

In this experimentation, the starting point was an existing project with its own design rules. Some of these rules can be different from the traditional concepts of the scheduling theory. It implies specific translation rules to a scheduling analysis tool (Cheddar). Our model is has too much details, the translation act as an automatic abstraction.

Identification of tasks.

In our model, tasks consist of different HLEB. HLEBs have their own activation properties and consequently our tasks can have suspension points due to a wait on event synchronization. A task in the model cannot be mapped directly on a Cheddar task. In the most general case the HLEB is the closest concept from a Cheddar task. Some specific HLEB have a synchronisation with a periodic event during their execution. In this case the block must be divided in two tasks.

Properties of Cheddar tasks. The priority is defined by the priority of the MARTE task on which the HLEB is allocated. The capacity corresponds to the sum of the WCET property of the BEB executed by the HLEB. The deadline is given by the deadline NFP of the last BEB executed by the HLEB. The activation is defined by the type of synchronisation resource that triggers the activation of an HLEB.

Shared resource. Each lock instance corresponds to a shared resource in Cheddar. The access to shared resource is represented in the model by the connectors between an HLEB and a lock instance.

In Cheddar we have to set the date of begin and end of the critical section. This information is given by the activity diagram of the HLEB. The begin date correspond to the sum of each BEB WCET called before the call of the "requestLock" service of the lock instance. The end date is the sum of the WCET steps until the "releaseLock".

Processor. The different properties used to describe a processor in Cheddar (scheduling policy, preemption) are defined by attributes of a MARTE scheduler. The association between a task and a processor in Cheddar corresponds to the property "schedulers" of the swSchedulableResource MARTE stereotype.

CONCLUSIONS

Results. This paper has presented an experimentation which proposed a specific use of the UML-MARTE language to model dynamic architectures of space On-Board Software. This modeling strategy has been successfully applied on an operational use case using the Papyrus Editor on an Eclipse Platform. The resulting use case model has been exploited for schedulability analysis purpose using the Cheddar formal schedulability analysis tool. The proposed modelling strategy relies on a selected sub-set of UML-MARTE. The cornerstone of this methodology is the use of the SRM profile of MARTE to formally specify the computational model upon which is constructed the dynamic architecture. The deep encoding of this computational model allows defining a dynamic model very closed to the actual implementation of the application software. Such detailed dynamic model can be productively used for documentation generation, schedulability analysis and we hope for code generation purpose. Even the gain is marginal in terms of coding effort, using automatic code generation could be a real benefit in terms of quality as it ensures a strong coherency between analysis results and actual implementation.

Using UML & MARTE in Operational

Context. This study shows that MARTE metamodel provides all the necessary concepts to model space OBSW dynamic architecture. However its adoption in an operational design process requires defining home guidelines to be respect by dynamic architecture designers. From Astrium point of view, the use of a home specific editor which enforces these guidelines is required to improve usability of MARTE and consequently reduce the cost of modelling activities. For instance, editors should not allow the user to use MARTE stereotypes which don't belong to the MARTE sub-set defined by the modelling guidelines and mask the access to stereotype properties which are not relevant for its concern. Notice that Papyrus provides broad capabilities of customisation which could be sufficient to design such domain specific editor.

Perspectives. The design of dynamic architecture is an iterative process. The SRM profile is probably not adequate in first stages of the design process. The use of the HLAM sub-profile for these first stages and links between such abstract model and the detailed models proposed in this paper have to be investigated. Automatic code generation using the SRM profile also needs investigation.

The last perspective is to improve the tooling environment to be able to capture in the same modelling environment results coming from the formal analysis tools used for schedulability analysis.

Figure 1 : 1 .

 11 Figure 1 : Overview of the Modeling Methodology The model is structured in 5 packages which catches different views of the system: The Static Architecture package contains the static architecture of the on-board software. This model, formalized in term of class diagrams, has not been developed in the context of the CNES study: this model is the one operationally developed for the AS250 program. This model has been used to generate the C source code skeleton of the AS250 OBSW using the Acceleo UML2EC plugin of the Topcased platform. Some class operations of this model are referenced by the dynamic architecture via the activity diagrams which model the tasks control flows. The Execution Platform package contains the description of the Software and Hardware parts of the execution platform:

Figure 2 :Figure 3 :

 23 Figure 2 : Domain Model: Core Elements The Figure 2 presents the Computational Model used for the architecture definition of the AS250 observation satellite. The Dynamic Container is an abstraction which describes the handle by which the RTOS schedules the various processing. Execution Blocks. A Dynamic Container owned a main Execution Block. Execution Blocks are closely related to actual implementation of functional behaviour. An Execution Block can be decomposed in sub-blocks. Leafs of this tree structure represents a pure sequential piece of code which is characterised by its execution duration (WCET of the Execution Block). An Execution Block can wait and release Synchronisation through the Wait() / Release() interface to conform to the constraints of strict behaviour sequencing and can request and release Locks to access shared resources by respecting mutual exclusion constraints. In order to ease schedulability analysis, some restrictions are imposed:  If an Execution Block waits for a Synchronisation, this wait is "at the beginning" of the Execution Block, before any CPU usage;  If an Execution Block releases a Synchronisation, this release is "at the end" of the Execution Block, after all CPU usage.  If an Execution Block requires use of Lock, it requires it for its whole duration, excluding Synchronisation accesses;  If an Execution Block is not a leaf Execution Block, its CPU use is zero (all CPU use is assigned to the leaf Execution Block). Tasks & ITHandler. ITHandler is a specialisation of Dynamic Container which have the following restrictions: it is associated which a single Execution Block that has limited capabilities: no Lock request, no "IN Synchronization" and has one "OUT Synchronisation". Task is the other specialisation of Dynamic Container. It is associated with a set of Execution Blocks that includes at least one "IN Synchronization". Task is characterised by its priority which is used by the RTOS scheduler to determine CPU allocation in case of competition. Tasks are specialized in

Figure 4

 4 Figure 4 : Clocks definition

Figure 5

 5 Figure 5 shows the decomposition of the Attitude And Orbit Control System (AOCS) of the AS250 OBSW. A main class AOCS_Appli is defined. This functional chain is composed of three HLEB. The AOCS_CYCL_HLEB which captures the cyclic functional behaviour of the AOCS is further decomposed in seven basic execution blocks.

Figure 5 : 4 . 1 . 2 Instantiation

 5412 Figure 5 : Execution Blocks Definition (UML Class Diagram) 4.1.2 Instantiation The second step is to associate a UML Composite diagram to the class which represents the considered functional chain. Figure 6 shows the composite diagram associated to the AOCS_Appli class.

Figure 6 :

 6 Figure 6 : Dynamic Architecture of AOCS_Appli (UML Composite Diagram)

Figure 6

 6 Figure 6 three parts typed by the Task entity of the computational model are defined: AOCS_cycl, AOCS_MAN and AOCS_Async. Links between execution blocks and tasks is formally defined using an <<Allocate>> dependency.

Figure 7 :Figure 8 :

 78 Figure 7 : Instance Diagram to specify the values of NFP

This experience has been conducted in the scope of a R&D study founded by the CNES


Critical Jose Reis

Brett Bicknell

Michael Butler

John Colley

Innovative Approach for Requirements Verification of Closed Systems

Keywords: Closed Systems, COTS, Event-B, Rodin, formal methods, integration, verification, model checking, simulation, safety case, assurance

Requirements quality has long been an

Requirements are generally verified early in the lifecycle using manual inspections. However, while the manual approach is valid for less complex systems, it is not adequate for systems with greater complexity and a complicated hierarchy of requirements. Another trend within UK Defence is the adoption of Closed Systems for mission-and safety-critical systems. As the name suggests, a Closed System is a solution which is available as a black box, where access to internal modules and design artefacts is not possible. In the context of this paper, we will refer to a Closed System as a software-based system which can refer to either of the following contexts:

1. Systems developed by a third party that are commercially available to the public domain as readymade solutions; also known as COTS solutions.

2. Systems developed by a third party that are not commercially available but, due to legal, export controls or other commercial reasons, are not open to the system integrator.

The use of Closed Systems raises several challenges from a safety certification perspective: limited information, limited test coverage and non-deterministic behaviour of the Closed System in use. When the system under test is closed, a classic isolation testing approach is inadequate to demonstrate the reliability of safety-critical software, because proper coverage cannot be measured. Lacking proper coverage during the testing phase, the scenarios used may only test certain functions within the Closed System software. When the software is then used, functions that have not been tested may generate faults that could cause the system to behave in unexpected ways.

A system architecture based on Closed Systems is particularly sensitive to obsolescence management issues. When a component (software, hardware or firmware) is upgraded, the system needs to go through regression testing. The key issues are to determine which tests need to be run to ensure that the integrated system operates correctly with the new part, the impact of the new version of the software/hardware on the rest of the system and how to validate assumptions made about the new version of the software/hardware.

Verification and Integration of Closed Systems through Formal Methods (VICS-FM), a new approach developed by Critical Software Technologies and the University of Southampton, uses a rigorous approach to extend the evidence provided by software verification processes 1

. The approach involves generating formal models to help provide further evidence relating to the behaviour of architectures with integrated Closed Systems, before having to run the Closed Systems in a test environment. This saves time and costs, increases confidence in the system and allows for any proposed updates to the Closed System to be assessed before they take place.

The additional evidence provided by the formal modelling includes:

 The ability to precisely define functional coverage and to measure the functional coverage of test sets.

 The generation of test sets using the tools available in the formal approach.

 Strong validation of models using proof and simulation tools, which validate the definition of functional behaviour and the functional coverage of tests.

 The ability to support the evaluation and impact assessment of changes when a new version of the software/hardware is released.

The VICS-FM approach offers a rigorous method to:

 Strengthen the requirements and design of the system.

 Validate assumptions about the solution.

 Conduct 'what-if' analysis.

 Identify which scenarios, if any, lead to the system being left in an unforeseen or undesired state, such as deadlock.

 Generate an animated model and visualisations of the system using a graphical user-friendly interface, to help test and validate the formal models.

The VICS-FM approach is based on the use of a formal modelling language (Event-B) which is based on set theory and supported by mathematical proof and model checking technology. Due to the formal method used, the responses provided by VICS-FM are unambiguous and trustworthy. VICS-FM is best used at earlier phases of the lifecycle, because it can identify problems with the requirements and can be used to confirm the suitability of the Closed System. The approach can also be used once the Closed System has been procured and installed.

VICS-FM complements more traditional verification & validation approaches. In particular VICS-FM can be used to verify elements on the left-hand side of the V-Model. System, integration and acceptance tests are still required, but their scope can be reduced. When the VICS-FM approach is used with bespoke applications, unit tests are not normally required.

Innovation

The VICS-FM approach is described below in the context of Closed Systems verification but it could also be applied to a bespoke system.

The innovation in VICS-FM stems from the application of an existing method (Event-B) plus a toolset (Rodin) to solving the problem of how to verify and integrate Closed Systems. The model of the Closed System is sufficiently generic to be reusable in different contexts. The specific VICS-FM innovation did not involve any significant developments to the Rodin toolset.

The approach proposed represents a considerable change in the use and successful integration of Closed Systems, using formal methods to guarantee their integration and functionality.

The VICS-FM approach could be used in:

 Verification and Validation of complex systems that use Commercial Off-The-Shelf (COTS) solutions.

 Verification of safety properties in mixed risk environments where COTS solutions are used by the underpinning platform. Typically in these environments, single failure scenarios can be verified through classical testing approaches but multiple failure scenarios are more difficult to verify. The VICS-FM approach will increase the assurance of these systems.

 Supporting the integration of legacy systems with COTS solutions (for example, virtualisation middleware). Legacy systems do not always integrate directly with COTS solutions, therefore bespoke solutions are required. These solutions can be modelled and proven correct using this approach.

 Requirements and design specification: VICS-FM can be used to verify properties and highlight gaps in requirements and design early in the development process.

Solution

The VICS-FM approach requires that the input specifications are translated to an Event-B model. This is done manually, using the Rodin toolset 2 . The Event-B models are constructed of variables, events -which perform actions on variables -and invariants, which allow the designer to specify the properties of the system that should be upheld. The proving and model checking capabilities of Rodin help indicate whether these invariants, and hence the associated properties, are maintained over the possible behaviour of the system that is encapsulated by the modelled events. The approach not only provides an indication of the changes that need to made in the case of the violation of any of the properties, but it also provides examples -i.e. particular sequences of events -where the properties are violated; from which the associated scenarios can be identified to help inform areas of uncertainty in the system behaviour as soon as possible.

A case study used to evaluate the VICS-FM approach involved the integration of a closed COTS solution within an end-user system with particular safety and critical operational constraints. The COTS solution is a virtualisation middleware (VMWare) and the end-user system is a military system (mission critical) which, due to the security classification level, cannot be disclosed in this paper. Issues were found with standard testing approaches due to some inherent, non-deterministic behaviour of the COTS solution. In an attempt to combat this, some additional bespoke software was created to constrain the behaviour of the COTS solution, although it was not fully understood how the combination of the COTS solution with the end-user system and bespoke software element affected the safety and operational constraints; partly due to the closed nature of the COTS solution, but also because of the complexities of the interaction. The VICS-FM approach was used to assist in the verification of the behaviour of the composed system in terms of the identified constraints. The Event-B model produced consisted of several parts:

1. A model of the relevant behaviour of the COTS solution, based on documentation of the COTS solution and discussion with domain experts. It was not a requirement to model the entire COTS solution, only the subset of the behaviour which was relevant to the properties to be verified. As mentioned in the limitations later in the paper, it must be ensured that the assumptions and exclusions made during this process are recorded and agreed with the safety and engineering teams.

As the verification involved the non-deterministic behaviour of the COTS solution, this was reflected by considering all possible combinations and sequences of the defined events for the model of the COTS solution in an abstract way. This meant that, not only was it possible to construct a suitable model of the COTS solution without requiring in-depth knowledge of the exact process sequences followed in different scenarios, but also that during model checking, any of the potential paths of the COTS solution could be encountered.

2. A model of the applicable elements and available actions of the end user system, including the bespoke software mentioned above, and how these interact with the COTS solution.

3. Global properties of the system, specified as invariants, corresponding to the constraints that require verification. In the case study identified above, the invariants corresponded to the properties of the system that the behaviour of the COTS solution should maintain due to the limits imposed by the bespoke software solution.

To facilitate the generation of the models, especially for users who are less experienced in the approach, UMLlike diagrams and state machines can be generated in Rodin, from which the tool automatically generates the underlying Event-B model. In a simulation of the model, the user can step through the transitions (depicted in the example state machine, Figure 2 which provides the capability to produce and translate these diagrams, was used to generate the models of the COTS solution and end-user system mentioned above during the case study.

After generating the Event-B model of the system the following actions can be conducted automatically using the Rodin toolset:

1. A model consistency check, run using simulation and model checking (using the ProB tool 4 ).

2. Proof obligations are generated which, when proven, can demonstrate whether any of the defined actions invalidate any of the invariants regarding the variables being modified. In other words, proof obligations are generated to demonstrate that all possible outcomes of each action maintain the properties specified by the invariants. There are automatic proving capabilities within Rodin which assist in completing these proof obligations.

3. The model checker can be run to find scenarios where particular invariants are violated, if the proof obligations cannot easily be discharged. This is useful for more complex behaviour and invariants, such as those encountered during the case study. These scenarios can be identified and typically correspond to areas of uncertainty, where it is important to have feedback as soon as possible. During the case study mentioned above, a scenario was highlighted which violated some of the safety and operational constraints. By examining the trace of events corresponding to this scenario -provided by the model checker -it was possible to understand which limitation or specific behaviour of the bespoke software caused the violation of the constraint. Figure 3 below gives an example of the use of the model checker; the violated invariant is shown in red and the trace of events that led up to the violation is displayed in the history tab on the right-hand side. Using the tool, it is possible to generate an animated front-end to the simulation of the model in the form of a user-friendly graphical interface, which corresponds to the system's GUI (see Figure 4). The user can interact directly with this animated front-end, while the tool continues to run the formal analysis in the background, reacting to user choices and checking the model and invariants at each step. This was utilised during the case study, to produce a representation of the GIU provided as part of the end-user system. As this graphical representation is tied to the underlying Event-B model, it can not only be used to run through the model and confirm that the model is the correct representation of the system, but can also be used to explore further scenarios. This graphical representation of the system can be used without necessarily requiring any experience with the Event-B language or the toolset.

Benefits

The VICS-FM method lends itself to finding inconsistencies in the requirements specification. The set theory that supports the method and the proof obligation mechanism forces the engineer to think further and to specify properties that are implicit, but not necessarily specified in the requirements, as inputs. Any inconsistencies between the requirements are identified and fed back to the requirements owner.

Another useful mechanism offered by the Event-B method is refinement. This allows the model to start in a very abstract form, and gradually be refined by adding further properties and detail at each step, whilst ensuring that consistency is maintained with all previous refinement levels of the model. In the context of Verification and Validation (V&V), this mechanism enables the tailoring of the Event-B model to include only that which is strictly required to prove specific properties. This mechanism is critical in the context of Independent Software Verification and Validation (ISVV) activities, because the time available for conducting an ISVV activity is often limited and therefore it is not possible to translate the entire system into an Event-B model.

Another advantage of this approach is that is promotes model reuse. The model of the Closed System can be considered separate and therefore reused and applied to validate the integration of other systems that interface with the same Closed System. In addition, if further properties need to be specified for the system in the Event-B model, this can be factored into the process by refining the existing system model and adding the relevant extra behaviour in this additional refinement. Adding extra properties (for instance, an extra requirement) does not necessarily involve modifying the existing model, or having to re-prove any of the existing proof obligations, as these extra properties are introduced and tested in an additional refinement level. This adds flexibility as to when the formal verification is used: the main model can easily be picked up at later stages should the customer be unsure about a particular, perhaps newly-developed, property.

The project in which the VICS-FM Approach was used had a duration of 5 months and for that reason the chosen case study and the Event-B model generated had to be tailored. Considering these constraints it was possible to identify one scenario where the real system would be left in an undesirable state. This finding was achieved with an effort of approximately 3 man-months, which includes analysis of the requirements and discussion, generation of the Event-B models and "execution" of models. The provider of the case study came to the same conclusion using a classical testing approach but with an effort of approximately 12 man-months. The reason for the extra effort using the classical testing approach is mainly because of the non-deterministic nature of the virtualisation platform and the use of the manual approach in testing. Using the VICS-FM approach the identification of scenarios where the system could be left in an undesirable state requires less time and effort. In terms of scalability, it is known that the underlying toolset has been used with models of considerable size 5, 6, 7

.

The key issue when the size of the models increases relates to proof generation, which is not fully automated and sometimes requires manual intervention to discharge. This is not an issue with the VICS-FM approach but rather an issue with the Rodin toolset and the theorem provers used.

In summary, the VICS-FM approach:

 Provides a sound model of the requirements selected for modelling, so that any ambiguity within these can be removed.

 Improves the integration of Closed Systems, supporting the relevant safety cases and reducing costs throughout the V&V cycle.

 Enables precise definition of functional coverage.

Limitations

1. The resulting Event-B model is only a representation of a subset of the end system and Closed System.

To address any potential shortfalls of the Event-B Model, a strategy has to be identified and agreed with the safety and systems engineering team with regard to which properties need to be formally verified. This will then define which aspects of the Closed System are modelled and which elements of the rest of the system remain to be modelled. The level of confidence in the evidence collected using other approaches (classic testing), plus scenarios which are hard to verify or simply cannot be verified by running the system over longer and longer timescales, should be taken into account to decide what will be formally modelled using Event-B.

2. Due to the fact the Event-B model generated covers only a subset of the real system, the outputs of the proofs and simulations run are limited to the elements modelled in Event-B. Depending on the issues that need to be verified, this could become a limiting contingent on the expected outcomes of the verification activity and the dependencies within the inner elements of the Closed System. Using abstractions, it is possible to focus on and expand higher-level elements of the system, if that makes the model more representative.

3. Any assumptions about the underlying behaviour of the Closed System must be documented and discussed with the safety and engineering team to ensure that they are justified.

4. The Event-B method and the Rodin toolset are not yet capable of verifying certain performance requirements such as confirming the time it takes to perform particular tasks. Therefore, the required availability of certain resources used by the system must be ascertained using a different approach.

5. VICS-FM is fundamentally geared towards the verification of safety-critical software. It is a sound approach that provides rigorous evidence to support the safety case. Nevertheless, the approach still requires specialist knowledge in set theory and the Event-B method, hence it is not straightforward to learn and must be practised by an experienced engineer.

3 ,Figure 1 :

 31 Figure 1: VICS-FM Approach

Figure 2 :

 2 Figure 2: Example of Event-B State Machine

Figure 3 :Figure 4 :

 34 Figure 3: Example of the model checker in use

Copyright Critical Software Technologies Ltd © 2013 CSWT-2013-DOC-00125

For information purposes only. Information contained herein is provided as an output from a UK MoD/DSTL Centre for Defence Enterprise funded research programme. All rights reserved.