M Fortes Da Cruz

M Kwiatkowski

S Sharma

Formal assessment of hybrid functions

Keywords: Formal requirements, hybrid functions, model checking, ICP, SAT, LTL, CTL, DPLL, SMT. 1. Introduction and industrial motivation

It is commonly accepted in the academic community that if the use of formal methods were more widely spread and properly supported, then their use would provide substantial development time and cost benefits for the engineering of safety-critical systems. The present work builds upon an increasing imperative to improve continuously the process, methods techniques and tools for analysing the functions/behaviours allocated to hybrid systems in the chosen avionics and mechatronics technologies. Formalisation of requirements and formal expression of models remain the two major representational bottlenecks impeding the wider industrial usage. Our investigations suggest that relatively minor improvements to the prevailing industrial practices can help to overcome these bottlenecks and to start benefitting from the power of formal methods. In this paper, we present a novel method and workflow for formally analysing engineering specifications of hybrid systems that, semiautomatically, bring together requirement and domain engineering model. Both the method and workflow are validated with a case study of the Airbus A350 autobrake model.

Introduction:

For more than three decades, the aerospace industry has been using digital computers as an integral part of the civilian aircraft's flying safetycritical equipments. In turn, the proliferation of digital computers has created an increasing imperative to continuously improve the process, methods techniques and tools for analysing the functions allocated to systems in their chosen technologies. The present work builds on this imperative by exploring ways and means for increasing the automation of formal verification. The proposed automation is through translation of requirements, and their respective design models, into formal logic transcriptions that can be merged and analysed from the same file. The systems of interest are hybrid systems; these are multi-physics systems that exhibit continuoustime and discrete-time behaviours, with event-driven behaviours emanating from the embedded software components. Naturally, hybrid functions are allocated to, and implemented by, hybrid systems. Further, the term hybrid function is used to describe those functions that feature both continuous and discontinuous functions from the multi-physics domain as well as the discrete-event functions from the embedded realtime control software applications. Design is constructed through using models of both the physical elements (using CAD tools) and the avionics elements (using CASE tools). Conversely, the requirements have evolved from being disjoint sets of objective in structured documents, to integrated databases of indexed and linked textual objectives for validation and verification. Applying formal methods to verification of embedded software for avionics requires constructing a coherent formal set of propositions that precisely captures the textual assertions and property objectives into formal logic propositions. Besides, the engineers also need to envision consistently the behavioural logic of their models into a formalised set of declarations, relations, constraints and state transitions. Before any meaningful formal assessments can be conducted, both sets of formal sentences-models constrained by requirements, and the attached objectives-must be correctly merged and prepared for analysis using a model checker.

Industrial motivation:

The Advisory Council for Aeronautics Research in Europe (ACARE) was set up in June 2001 to develop and maintain a Strategic Research Agenda (SRA) for aeronautics in Europe. This was referred to as the ACARE 2020 Vision. By 2004, ACARE identified five challenges and six high-level Target Concepts. These were gathered in two volumes [START_REF]Strategic Research Agenda Volume 1[END_REF].

This work aims to provide some contribution to the following three ACARE challenges:

a) The Challenge of Quality and Affordability:

The Quality of the product is both its attributes and its properties; the attributes are subjectively assigned by the observer, whilst the properties are its intrinsic characteristics. We focus on the extent to which these intrinsic characteristics of the product fulfil its requirements. Affordability is also a subjective attribute; however, from the perspective of the manufacturers, it results from the ability to price the product correctly. Controlling the cost of Design, Development and Build allows the manufacturer to price the product for the market. Specifying the product concisely, so that the supply chain produces the required products, is a key contributor to affordability. b) The Challenge of Safety Safety is the topmost driver for the aeronautics industry. The notions of Safety emerge from the behaviour of the systemelements and their interactions with their operations environment. In turn, the behaviour of the product emerges from the behaviour of its parts and their interactions. We focus on the automatic assessment of those safety properties that are allocated to the product. As one of the contributors to meeting the Challenge of Safety, ACARE identifies -Increase depth of product's dependability assessments‖ during the Design, Operation and Maintenance phases. We focus on increasing the depth of the systems dependability during the design phase. c) The Challenge of Air Transport System Efficiency Improvements in the efficiency of the ATS effects, and is affected by, the reliability of the components that constitute the system. An aircraft is a component of the Air Transport Systems (ATS). From an aircraft manufacturers' perspective, the aircraft must be one of the most reliable components of the ATS. Further, the systems that constitute the aircraft must be reliable as they, in turn, contribute to the reliability of the aircraft. The remaining two challenges; the Challenge of the Environment and the Challenge of Security are outside the scope of this work.

In contribution to this industrial context, we address:

The impediments that occur between the textual requirements and their manually interpreted formal expressions. The effort of interpretation is time and resource consuming, which defeats the object right from the start. One way to clear this bottleneck is to structure the engineering domain text and automate the formal translation.

The need to assess both the continuous and discrete state space, and path of computations.

Aircraft systems, such as the braking system, implement an aggregated set of hybrid functions in their chosen technologies of hardware, software and physical components, which are sensed, controlled and commanded. The Domain and Safety & Reliability Engineers interpret the normal and abnormal behaviours that lead to different envisioning of the models. A common and purpose-specific set of envisioning rules is necessary to assess the different perspectives of a system, for example, addressing a common V&V and safety purpose.

In order to address these areas this paper is organised into three parts. The first part, presented in Section 2, describes the formalisation of the constraints and properties of the models. The second part, presented in Section 3, describes the case study and a validation of the results. The final part, presented in Section 4, concludes with a discussion of our findings and suggests further work.

Formalising models and their properties

In order to analyse avionics models against design requirements automatically, it is necessary to remove all ambiguity from both areas. Furthermore, the resulting formal versions of models and requirements have to be compatible. This presents the non-trivial task of choosing the formal platform on which to conduct our analysis. Because the functions we aim to analyse are hybrid and nonlinear, the formal framework has to be able to faithfully capture these two concepts.

Formal frameworks

A theory, a notation, a language and a platform support each of the formal frameworks below. The maturity of the first two frameworks led to industrial applications in the area of hardware verification (e.g. Collins proprietary AAMP5 Microprocessor) [START_REF] Miller | Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods‖[END_REF].

Design Verifier (SLDV, DV plugin) [START_REF] Au | Da Cruz: -Two-ways traceability between Requirements Based Engineering and Model Based Engineering using DOORS and SCADE tools[END_REF]:

SLDV is an option for the MathWorks MATLAB/Simulink © and the SCADE © tool set. It performs an exhaustive formal analysis of dataflow and controlflow models, restricted to the interface boundaries and to the scope of the relevant selected set of sub-systems or functional operators. The model coverage assessment is deduced from the analysis, which follows from that scope assumption. Dataflow refers to the Simulink and SCADE approach to modelling functions. Controlflow refers to Stateflow/SSM approach to modelling behaviours and mode logic with transitions. SLDV/DV can confirm or refute the consistency and correctness of Simulink/Stateflow or SCADE/SSM models with respect to the given properties. Domain engineers specify these properties directly in a Companion Observer Block Diagram, as claims to be guaranteed from assumptions about the interface. The constraints are specified in the models using assertion blocks.

NuSMV (LTL/CTL) [3]:

NuSMV is a symbolic model checker that originated from the re-design, re-implementation and extension of CMU SMV; a BDD-based model checker originally developed at CMU [McMillan 1993]. The input language of NuSMV is designed to take a description of Finite State Machines (FSM). The types of FSM can be completely synchronous to completely a-synchronous, and can feature full details up to more abstraction. NuSMV specifications are expressed in either of two different temporal logics: Computation Tree Logic CTL, and Linear Temporal Logic LTL extended with Past Operators. NuSMV evaluates CTL and LTL specifications in order to determine their truth or falsity in the FSM. If a specification does not to hold, then NuSMV constructs and presents a counterexample, i.e. a trace of the FSM that refutes the property.

HySAT [START_REF] Fränzle | Verification of Hybrid Systems[END_REF][START_REF] Fränzle | Efficient Solving of Large Nonlinear Arithmetic Constraint Systems with Complex Boolean Structure[END_REF]:

In essence, satisfiability (SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in a way that the formula evaluates to TRUE. Martin Davis and Hilary Putman (DP) devised the first algorithm in 1960. In 1962, George Logemann and Donald W. Loveland proposed a refined DP as DPLL-algorithm. HySAT is a SAT solver developed at the University of Oldenburg. It checks for satisfiability of arithmetical formulae that might involve non-linear and transcendental functions. HySAT processes elements of discrete and continuous domains (e.g. integer and real) as intervals on the real line and thus the solver is particularly suitable for analysis of hybrid functions. HySAT integrates the DPLL-based SAT proof search algorithm with the interval-based arithmetic constraint propagation. This allows HySAT to take advantage of handling conventional model checking whilst handling similarly large Boolean combinations of non-linear arithmetic constraints involving transcendental functions. Because the functions under analysis are hybrid and non-linear, the formal framework must faithfully capture these two concepts. Theory of hybrid satisfiability, and in particular the SMT solver extension in HySAT, appears suitable to solving this class of problems.

HySAT accepts input files consisting of four sections. The first three define the dynamic model that is the subject of analysis by listing all the state variables and the relationships between them (called constraints). The last section contains the target formulae that encode questions about the present and future behaviour of the model. Design requirements are represented as target formulae and models as sets of constraints. This achieves the integration of the two domains; described in more detail in the next sections.

The choice of HySAT was based upon the following three reasons. Firstly, it handles discrete and continuous variables in a uniform fashion, namely as intervals on the real line; therefore, it provides an elegant and powerful (through the use of interval arithmetic) framework for hybrid analysis. Secondly, it supports the use of non-linear as well as transcendental operators in constraints and targets, and hence copes with the inherently non-linear characteristics of physical laws. Finally, it supports relatively free mixing of Boolean and arithmetical constructs, which are useful when analysing signalprocessing diagrams. For a detailed comparison of HySAT with other satisfiability software, see [START_REF] Clarke | Model Checking[END_REF].

Certain analysis and verification tasks can be performed directly by Design Verifier (DV) [START_REF] Au | Da Cruz: -Two-ways traceability between Requirements Based Engineering and Model Based Engineering using DOORS and SCADE tools[END_REF]. Whilst a useful tool, DV is not able to handle the complex non-linearities inherent in the majority of the requirements that industrial engineers deal with; further Simulink and Stateflow are not based upon a synchronous language.

Formalising a Dataflow block diagram model

Simulink: The starting points of the model formalisation tasks are Simulink (*.m files) design specifications (*.mdl files). Here, the point of interest is on signal-processing diagrams. Such diagrams are translated to HySAT model specifications. More precisely, a state variable is assigned at first to every line in the model. Then, one or more constraints are produced for every block, hence linking variables corresponding to its input and output signals in a way that reflects the block's intended behaviour. Finally, a limited type and range inference for the output variables is achieved. A by-product of this translation is an association table of signals and variables, which proved very useful for debugging.

As an example, consider a summation block with two input signals and one output signal. In the first step, variables for the signals are created; say "x" and ‗y" for the inputs and ‗z" for the output. The second step yields the invariant constraint "x+y=z", which obviously reflects the normal behaviour of the summation block. Finally, assuming that input signals (x, y) are floats with ranges ([0,100], [-50,50]), the type of the output signal, z, is inferred also to be a float, with the range ([-50, 150]). An output might be an input to another block; such information can also be used to infer type and range of the output of that block. Implementation: The procedure described above was implemented using the Target Language Compiler (TLC), a code generation language for Simulink, allowing annotation of the model files and generation of a coded format file in HySAT format.

The Simulink to HySAT translation consists of three stages using TLC: (a) Pre-processing of the Simulink model (setup.tlc) (b) Creating appropriate constraints (blocks.tlc) (c) Inferring the types and ranges of variables (bounds.tlc).

Formalising constraints from requirements

Formalisation starts with a design requirement given as an English sentence. The ideal route to take would be to automatically parse, recognize and translate such sentences; however, current state of natural language processing makes this an impracticalif not infeasibleoption. As the first step, therefore, requirements are re-written into an equivalent, human-readable form; however, a form that is sufficiently constrained and parsimonious to be machine-readable. In a second step, a procedure was devised to automatically translate such semiformal sentences to Linear Temporal Logic (LTL) expressions. Finally, those sentences were automatically translated into the HySAT target formulae.

Step 1: A formal grammar is built to make requirements expressed in natural language to be machine-readable. A formal grammar is a set of rules (called productions) for generating text by successive rewriting a pre-defined string. Grammars generate sentences that resemble original natural language requirements. A computer can understand (parse) such sentences precisely because a grammar constrains their structure (syntax). To give an example, the original requirement « The autobrake shall disarm after take-off » becomes « It shall always be true that the autobrake is not armed after the aircraft takes off. » Here, this translation is done manually but can be enhanced by a user-interface to guide the requirements engineer (Appendix 1).

Step 2: Once the semi-formal requirement is parsed, it is possible to identify the atomic statements, i.e. those that are the most basic assertions about the system. In the above example, these are « the autobrake is not armed » and « the aircraft takes off ». We manually match them to appropriate conditions on state variables, such as "AB_DISARMED = TRUE". Having done that, we use the internal structure of the semi-formal requirementconstructed using the grammarto build an LTL expression encoding this requirement. This is further facilitated by the fact that most productions directly correspond to specific LTL constructs (Appendix 2).

Step 3: The translation of LTL expressions to HySAT target formulae is relatively straightforward and amounts to little more than syntactic manipulations. Here we have to bear in mind, however, that certain LTL expressions are too complex to have a HySAT representation. Moreover, it is possible that the requirement holds when the target formula is unsatisfiable, and dually, fails when the formula can be satisfied. These cases are properly reported during the automated translation (Appendix 4). Implementation: The procedure detailed above was implemented as a standalone program using the functional programming language Haskell. The program requires three input files; one containing the semi-formal requirements, one matching the atomic sentences to simple conditions on state variables and one containing the HySAT model definition produced from the Simulink diagram. The program then outputs the complete HySAT input file, ready for analysis.

Architecture of the Requirement Analyser:

The main program file accepts two input files: i.e. requirements (reqs) and variable/condition association table (leaves), and communicates with the different target language specifications via a standardised interface (interface.hs)

Formal assessment of hybrid functions

Case study using HySAT

The Airbus A350 autobrake analysis model consists of 1288 Simulink blocks and a similar number of lines. A HySAT model consisting of 658 variables, 238 constants and 822 constraints were obtained after the translation. The type and range inference procedures were successful for 81% of signals; the remaining 19% were involved in feedbacks, where the naïve iterative method failed. Manually inserting proper types and bounds in the loops and re-running the algorithm refined this method with a final result (Appendix 3). Three requirements were positively verified on this model. Both the formalisation and verification tasks were completed within minutes on a standard desktop computer (Appendix 4).

Validation using Gryphon/NuSMV

The formalisation of Simulink models can be performed using more established software tools. The Reactis tool (by Reactive Systems) preprocesses the models to an intermediate format recognizable by the Gryphon tool (by Rockwell Collins) [START_REF] Miller | -Formal Methods for Critical Systems[END_REF]. Gryphon produces a formal NuSMV specification and runs the NuSMV model checker. This NuSMV based workflow supports a wide range of Simulink blocks, but has one crucial shortcoming from our point of viewit does not yet fully support continuous variables, and hence hybrid systems. In order to compare our approach with the Reactis, Gryphon and NuSMV workflow, we have isolated a fragment of the A350 braking and control system where all but one variable are discrete, and discretised the only continuous one. We then wrote several study requirements for this module and checked them using both workflows. The results were identical, which validated our approach and implementation.

Conclusion

Discussion

Our work was exploratory in nature; we set out to gauge the potential of formal verification techniques in the context of industrial design of hybrid systems. This is why the integration of our framework with the existing industrial tools is not as complete as possible. The same is true of our specific analysis results, which lack in breadth. Nevertheless, we can report the following several conclusions with conviction.

Simulink diagrams are not formal enough. Simulink diagrams, like the one formalised during the course of this project, do not contain enough information on their own to make the formalisation process fully automatic. This is because Simulink was primarily used as a simulation engine, and actually not as a formal modelling language. Quite often, Simulink signals do not carry any information about their domain (range), units, and their loose type information cannot be reliable upon. Whilst this information can be partially recovered from supporting documents, such as Interface Control Documents (ICDs), this still requires human intervention. In summary, Simulink is a modelling tool used for simulations that can also serve as a general-purpose modelling and formal analysis environment if the diagrams carry more annotations on their lines of input and output ports as well as interface boundaries.

S-functions are difficult to verify. While native Simulink blocks have reasonably clear meaning (function) and can be readily represented in any formal setting, the semantics of S-functions is often unclear. The supporting documentation, while perhaps sufficient for everyday modelling, falls short of the rigour required for formal verification. As a result, the engineer performing formal verification of a diagram containing S-functions must access, or possess expert knowledge of this subject, in order to write tailored representations of their behaviour in the target formalism. Moreover, we have found that the use of S-functions promotes the lack of rigour described in the preceding paragraph.

Verification can be fully automated. The three instances where human intervention in the formal verification process was found to be necessary were:

(a) setting the proper types and ranges of variables, (b) reformulating the textual requirements in the constrained language, and (c) linking the basic propositions with model signals.

We believe that all three human interventions can be eliminated. Elimination of (a) can be achieved through more standardised and rigorous modelling practices; (b) can be eliminated by introducing a standard requirement language, where textual requirements can be parsed by a computer directly; and (c) can be performed during the modelling stage.

Medium-sized models can be verified efficiently. The autobrake model analysed here consisted of 1288 blocks. The translation to HySAT had 658 variables, 238 constants and 822 constraints. The requirements could be verified in a matter of seconds on a desktop computer. While these results are encouraging, some sensitivity to the number of variables and to their domains was found. Hence, we believe that models that are larger by an order of magnitude than the autobrake modelfor example, the full A350 BSCS modelcannot be practically verified, unless strict typing and range discipline is followed (see the paragraph on Simulink) and/or advanced modular (compositional) verification techniques are developed.

Requirements exhibit different levels of ambiguity.

Most of the autobrake requirements we analysed were ambiguous, in the sense that it was possible to assign more than one distinct formal representations to a single requirement. Some of them were simply too high-level to be translated to the language of arithmetical formulae; others had insufficient indication of their applicability domain; finally, some merely lacked proper tolerance levels. Elimination of these ambiguities, at least of the two latter kinds, would greatly increase the potential of automated requirement verification.

High-level programming languages should be used for verification tools. The Simulink to HySAT translator was implemented using TLC, an internal Simulink scripting language. Lack of advanced programming concepts in TLC makes it difficult to mirror the abstract mathematical constructs in the code, and consequently produces monolithic, inflexible software. In contrast, the use of Haskell for requirement analysis proved here to be the right choice because the result was a flexible and stable program. Of course, these remarks are not intended to cast doubt on the usefulness of TLC within its intended application areas: e.g. code generation (C, FORTRAN).

Future work

We have identified the following directions for further development:

Grammar inference It is possiblealbeit to a limited degreeto determine a grammar, given a sufficient number of sample sentences it produces, by a process known as grammar induction or grammar inference. Given the abundance of example requirements, it is conceivable to use this theory to build a requirement grammar from these examples instead of just postulating one, as we did. The main advantage of this approach is that the resulting grammar would produce sentences identical to the requirements as they are currently used. The main downside is that not all productions of this automatically generated grammar would correspond to any discernible logical or temporal operators.

Compositional verification Our estimates of the computational load of formal testing of requirements suggest that large avionics/mechatronics models cannot be cost-effectively tested yet with existing methods. Developing modular (also called compositional) verification techniques, where a requirement is verified for submodels and the verification results are then combined to yield an assessment of the whole model, would make it possible to also verify large models. While this is an extremely difficult and ambitious challenge in general, it should nevertheless be at least undertaken in a limited industrial scope.

Context-sensitive grammars In this work, we used a context-free grammar, mainly because of their conceptual and theoretical simplicity. However, it may be the case that a more complex contextsensitive grammar is a better fit for an industrialquality requirements language. The first step towards settling of this question should be a detailed analysis of the fine structure of actual requirements. Table 2: Propagation of types and bounds through the same diagram, this time with manual injection of type and bounds into the feedback loop.

Appendix 4: Session

A recording of a short command-line session with the requirement analyser. Seven commands are issued (bold lines numbered in square brackets). Commands [START_REF]Strategic Research Agenda Volume 1[END_REF] and [START_REF] Clarke | Model Checking[END_REF] display two files containing the requirement to be verified; in the second case, the requirement has an empty -while‖ clause, which makes it nonsensical. The third command displays the basic property--variable condition association table. Command [START_REF] Au | Da Cruz: -Two-ways traceability between Requirements Based Engineering and Model Based Engineering using DOORS and SCADE tools[END_REF] invokes the analyser on the correct requirement, and the result is a logical breakdown of the sentence, together with the HySAT target formula. Commands [START_REF] Fränzle | Verification of Hybrid Systems[END_REF] and [START_REF] Fränzle | Efficient Solving of Large Nonlinear Arithmetic Constraint Systems with Complex Boolean Structure[END_REF] produce CTL and LTL target formulae, respectively. Finally, an attempt to analyse a grammatically incorrect requirement is made, and results in an appropriate error message [START_REF] Miller | -Formal Methods for Critical Systems[END_REF].

[1] marek@belafonte:~$ cat req it shall always be true that the autobrake is disarmed after the aircraft takes off [2] marek@belafonte:~$ cat malformed_req it shall always be true that the autobrake is disarmed after the aircraft takes off while [3] marek@belafonte:~$ cat leaves the autobrake is disarmed = y27x136 <= 0 the aircraft takes off = (1 -y27x9) * y27x9' >= 1

[4] marek@belafonte:~$ ./analyser.exe -R req -L leaves This is the Requirement Analyser.

Results:

it shall always be true that the autobrake is disarmed after the aircraft takes off: it shall always be true that the autobrake is disarmed after the aircraft takes off Refute (BMC mode): (!(y27x136 <= 0)) and (((1 -prev_y27x9) * y27x9) >= 1); ================================================================================ [5] marek@belafonte:~$ ./analyser.exe -R req -L leaves -T ctl This is the Requirement Analyser.

Results:

it shall always be true that the autobrake is disarmed after the aircraft takes off: it shall always be true that the autobrake is disarmed after the aircraft takes off AG (((1 -y27x9) * y27x9' >= 1) -> (AX ((1 -y27x9) * y27x9' >= 1))) ================================================================================

  in[-20,20] x: float in [0,5] y: float in [-5,0] z: float in [-5,5] p: float in [-25,25] q: float in [-20,20] r: float in[-20,20]

Acknowledgements

This work was partially funded by the EPSRC through PhD Internship Programme of the UK Knowledge Transfer Network for Industrial Mathematics (KTN-Mathematics) 2009 and funded and supported by the Airbus Systems Methods and Tools department within an ongoing internal project in the Filton (Bristol, UK) group.

We thank all the reviewers of previous draft of this paper for their supportive and guiding comment.

Appendix 1: Grammar

The definition of the formal grammar underlying the requirements analysis is in the format of Happy (http://haskell.org/happy), a parser generator for Haskell. The first main part, beginning with the %token directive, contains the syntactic atoms processed by the grammar. The second, captioned -production rules‖, effectively defines the form of every correct sentence produced by the grammar. This file can be fully automatically compiled to a parser compatible with Haskell.

%% --Production rules

--Precedence and associativity of tokens. Tokens mentioned early bind weakly. %right assert not %right always never %right possible impossible %right alwayspossible neverpossible %left if then else %left unless until after while %left or and Appendix 2: Model & Formal requirements A snippet of the HySAT input file encoding the A350 autobrake model together with a requirement. The file has four sections: the first (DECL) defines the model variables. Observe that some of them are actually constants, thereby reducing the state space; variables are annotated with the name of the Simulink block to whose output they correspond; the variable marked with the asterisk (*) is involved in a feedback loop, and thus its type and range are set to the most conservative values. The second section (INIT) defines the constraints linking the variables in the initial state of the model, while the third (TRANS) defines the pre-and post-conditions to be met during the evolution of the model. Observe how the initial state conditions are duplicated in order to ensure model consistency after a transition takes place. Finally, the last section (TARGET) contains the target formula produced by the Requirement Analyser. As indicated by the appropriate annotation, the requirement in question is valid iff the target formula is unsatisfiable. The method requires all the information about the inputs to infer type and range of the output and thus it fails for all the variables involved in the feedback loop (Table 1). The solution is to manually specify the type and range of one of those variables and run the algorithm again (Table 2). p: ? q: ? r: ?

Table 1: Propagation of types and bounds through a signal processing diagram involving feedback.

[6] marek@belafonte:~$ ./analyser.exe -R req -L leaves -T ltl This is the Requirement Analyser.

Results:

it shall always be true that the autobrake is disarmed after the aircraft takes off: it shall always be true that the autobrake is disarmed after the aircraft takes off G (((1 -y27x9) * y27x9' >= 1) -> (X (y27x136 <= 0))) ================================================================================ [7] marek@belafonte:~$ ./analyser.exe -R malformed_req -L leaves This is the Requirement Analyser.

================================================================================ it shall always be true that the autobrake is disarmed after the aircraft takes off while: it shall always be true that the autobrake is disarmed after the aircraft takes off while ???

This requirement is structurally malformed. ================================================================================

Glossary

DPLL


M Bozzano

R Cavada

A Cimatti

J.-P Katoen

V Y Nguyen

T Noll

X Olive

Formal Verification and Validation of AADL Models

Keywords: Hardware/Software Co-Design, Model Driven Engineering, Verification

Introduction

Safety-critical systems are increasingly difficult to comprehend due to their rising complexity. Methodologies, tools and modeling formalisms have been developed to overcome this. Component-based design is an important paradigm that is shared by many of them. It helps to master the overall complexity while in addition allowing for reusability. Furthermore, it easily supports the common issues in the engineering disciplines, like hardware/software (i.e., co-engineering), performability, dependability, reliability, availability, maintainability and safety engineering (RAMS). Model artifacts that are typical for a discipline can be encapsulated in the affected components, while staying imperceptible for non-affected components. This leads to different views of the system under development, which subsequently entails the natural distinction in different system abstractions, formalisms and tools. Nonetheless, there is only one system under development. With the current methodologies, there is no single view of this system that links all aspects relevant to all involved engineering disciplines in a coherent manner.

To overcome this problem, the European Space Agency (ESA) has set up the COMPASS project 1 (Correctness, Modeling, and Performance of Aerospace Systems). Its goal is to develop a coherent and multidisciplinary approach towards developing systems at an architecture (i.e., systems engineering) level. The Architecture and Analysis Design Language (AADL) [START_REF]Architecture Analysis and Design Language (AADL) V2[END_REF] and its Error Model Annex [START_REF]Architecture Analysis and Design Language Annex (AADL)[END_REF] is adopted as the key formalism to fully capture model the system under development (see § 2). Furthermore, we base a collection of verification and validation (V&V) activities over AADL models on state-of-the-art model checking techniques, like symbolic and bounded SAT-based model checking, and also probabilistic variants thereof. A mature graphical-driven toolset has been developed to support this approach (see § 3). The toolset and its potential have been evaluated by Thales Alenia Space using several case studies from the satellite domain (see § 4).

1 http://compass.informatik.rwth-aachen.de

Architecture and Analysis Design Language

The AADL modeling language is standardized by several major industrial and academic partners since 2004 [START_REF]Architecture Analysis and Design Language (AADL) V2[END_REF]. Models in this language can capture real-time, performance critical and distributed aspects at an architectural level. It supports annexes to extend the language, among which the Error Model Annex [START_REF]Architecture Analysis and Design Language Annex (AADL)[END_REF] was particularly interesting for our application. We have defined a formal semantics for its core features and added additional elements needed to enable formal validation and verification. The resulting input language has the following design features:

• Modeling both the system's nominal and faulty behavior. To this aim, our input language provides primitives to describe software and hardware faults, error propagation (that is, turning fault occurrences into failure events), sporadic (transient) and permanent faults, and degraded modes of operation (by mapping failures from architectural to service level).

• Modeling (partial) observability and the associated observability requirements. These notions are essential to deal with diagnosability and Fault Detection, Isolation and Recovery (FDIR) analyses.

• Specifying timed and hybrid behavior. In particular, in order to analyze continuous physical systems such as mechanics and hydraulics, our input language supports continuous real-valued variables with (linear) time-dependent dynamics.

• Modeling probabilistic aspects, such as random faults, repairs, and stochastic timing.

A complete specification consists of three parts, namely a description of the nominal behavior, a description of the error behavior, and a fault injection specification that describes how the error behavior influences the nominal behavior.

The nominal model describes the system under normal operation. It is a system decomposition of interacting components in which system detail can be abstracted by defining a hierarchy among components.

The interaction interfaces are specified using port connections of which there are three types. Data port connections expose component variables to other components, flow port connections are evaluatable functions based on incoming data ports and event port connections are used to define (multi-way) hand-shaking communication between components. These port interfaces are complemented by a mode transition system, which describe changes over the ports, and thus essentially capture a component's behavior. The transition system can be annotated with linear differential equations and timing constraints to model the evolution of physical aspects, like temperature, pressure and scheduling of tasks. Modes can also be used to represent degradation of the system. Transitions between these modes can lead to dynamic reconfigurations by (de)activating components and port connections.

An error model as defined by AADL's Error Model Annex [START_REF]Architecture Analysis and Design Language Annex (AADL)[END_REF] expresses in which ways the system can fail, i.e., it models how faults may affect normal operation, how failure effects propagate throughout the system and may lead to a degraded mode of operation. It is modeled as a probabilistic finite-state automaton. Transitions occur due to spontaneous events or propagations. Events may be annotated with a rate that indicates the expected number of occurrences per time unit. Propagations occur between components when they are in a super-subcomponent relation or when they access a common bus. This implicit linking reflects the oblivious and pervasive nature of error models.

As error models bear no relation with nominal models, an error model does not influence the nominal model unless they are linked through fault injection.

An injection describes how a failure event lead to data failures in the nominal model, thereby changing the system's operation. There is an automatic procedure, called model extension, that integrates nominal and errors models with the given fault injections. The principal idea is that the nominal and error models are running concurrently. Using the fault injections, error transitions from the error models are interwoven in the nominal model via an interleaving semantics. The specified data failures override the nominal data effects. Failures hold as long as the error model is in an error state. They can be made transient by allowing the error model to leave erroneous states. The resulting model after model extension is an integrated AADL model, also called the extended model.

Toolset for Verification & Validation

A graphical toolset, named COMPASS Toolset, has been developed to conduct verification and validation analyses over AADL models. Its development has reached its final phase, and has been accepted by the ESA during its Acceptance Review meeting of March 2010. A public release is planned for May 2010.

The toolset leverages existing mature tools like the NuSMV symbolic model checker [START_REF] Cimatti | NuSMV: a new symbolic model checker[END_REF] and the MRMC probabilistic model checker [START_REF] Katoen | The ins and outs of the probabilistic model checker MRMC[END_REF]. The inputs of these tools are obtained by fully automated semanticpreserving model transformations from AADL and the requirements specification patterns. These patterns act as parameterized templates [START_REF] Grunske | Specification patterns for probabilistic quality properties[END_REF][START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] for a comprehensible and easy-to-use method of capturing safety, correctness, performance and dependability requirements. Several analyses have been defined using these inputs.

Their outputs are transformed back to a graphical and engineer-friendly form.

The next subsections introduce the analyses and their applicability in the system design process.

Requirements Validation

The validation activities are centered around the requirements. In order to ensure the quality of requirements, they can be validated independently of the system. For this, the requirements are converted automatically to their underlying formal logics (like Linear Temporal Logic and Computational Tree Logic), after which the analyses can be run. This includes both property consistency (i.e., checking that requirements do not exclude each other), property assertion (i.e., checking whether an assertion is a logical consequence of the requirements), and property possibility (i.e., checking whether a possibility is logically compatible with the requirements) [START_REF] Pill | Formal analysis of hardware requirements[END_REF]. Altogether these features allow the designer to explore the strictness and adequacy of the requirements. Expected benefits of this approach include traceability of the requirements and easier sharing between different actors involved in system design and safety assessment. Furthermore, high-quality requirements facilitate incremental system development and assessment, reuse and design change, and they can be useful for product certification.

Functional Verification

The formalized requirement and the AADL model are the input for analyzing operational correctness, which is the first step to be performed during the system development life cycle. It consists in verifying that the system will operate correctly with respect to a set of functional requirements, under the hypothesis of nominal conditions, that is, when software and hardware components are assumed to be fault-free. One particular instance of this general model-checking problem that is specifically supported by the toolset is deadlock checking, i.e., ensuring that the system does not give rise to terminating computations. This is usually required for reactive systems. Moreover the toolset offers the feature to interactively simulate the execution of the system.

Safety and Dependability

Analyzing system safety and dependability is a fundamental step that is performed in parallel with system design and verification of functional correctness. The goal is to investigate the behavior of a system in degraded conditions (that is, when some parts of the system are not working properly, due to malfunctions) and to ensure that the system meets the safety requirements that are mandatory for its deployment and use. For this the toolset generates common-practice artifacts, namely (dynamic) fault trees, (dynamic) Failure Modes and Effects Analysis tables (FMEA), fault tolerances, and criticality numbers [START_REF] Bozzano | The FSAP/NuSMV-SA Safety Analysis Platform[END_REF].

Performability

To guarantee the required system performance in the presence of faults, integrated hardware and software models can be evaluated with respect to their performance behavior in degraded modes of operation. The measures resulting from this analysis can be used to evaluate design decisions for costs and risks. The analysis is based on the input AADL model extended with its error models and fault injections. The resulting extended model is transformed to its underlying Markov model, which enables MRMC to compute the measures of interest like reliability, maintainability and survivability.

Fault Detection, Isolation and Recovery

System models can include a formal description of both the fault detection and isolation sub-systems, and the recovery actions to be taken. Based on these models, tool facilities are provided to analyze the operational effectiveness of the FDIR system, especially on how faults are detected, whether observability requirements suffice for system diagnosability [START_REF] Cimatti | Formal verification of diagnosability via symbolic model checking[END_REF], how the FDIR system isolates faults and whether recovery actions, in presence of failures, lead to an operational system state.

Case Studies

Two distinct case studies have been used to evaluate the AADL modeling language and the applicability of the COMPASS toolset in an industrial context. The first case study is related to the definition of satellite mode management and its associated FDIR strategy. The second case study models the thermal regulation function, where two sub cases have been derived at functional and behavioral levels. Both case studies are described in the next subsections

Global FDIR Strategy

The global FDIR strategy case study deals with the definition of satellite mode management and with the FDIR strategy management. The case study models the satellite mode management, the AOCS (Attitude and Orbital Control System) mode management, the configuration and reconfiguration sequences and an abstracted model of the AOCS equipments and other functional subsystems.

The satellite mode management consists of three modes and seven elementary transitions. The AOCS mode management has six modes and about 20 transitions. Five AOCS units have been considered. The model of the equipment is based on a six-state automaton, which can include timed transitions. The two functional chains are represented in an time-abstracted way. No behavioral part is modeled, only flags have been used to inject the faults, and emit the system alarm. The fault flag represents the level 1 faults (detected by software), which occur on the equipments. Examples of such faults are transmission error, electrical default and data inconsistency. The system level alarm represents several hardware detected faults (loss of pointing Earth or Sun). They are used as last barrier before losing the satellite and a direct reconfiguration to the satellite's safe mode.

The configuration and reconfiguration sequences represents sequences of commands, which are send to the AOCS units. Each AOCS mode has a configuration sequence to set up the right configuration of the AOCS units. The reconfiguration sequences are used in case of a detected failure. Both sequences used the same mechanism to initiate. An event is sent by the monitor (reconfiguration) or by the mode transition between two AOCS modes. The event is caught by a sequence manager, which emits an event for starting the procedure. Initially all the procedures are in an Idle state, waiting for the start event. This mechanism is similar to the one provided by the ECSS Packet Utilization Standard (PUS) for communication between ground and onboard application (see Figure 2). Service 5 is used to raise events, service 12 is dedicated to on-board monitoring, and service 19 allows one to launch an action on the reception of an event. These services are chained as such to achieve a reconfiguration that starts from a monitoring failure.

Verification

The COMPASS toolset was used to analyze the three following items:

1. Identification of all the failures leading to a given level of FDIR. It should allow to validate that the classification of failures by each level is well done.

For instance, for level 1 (equipment failure), only the monitor can be the root cause. Level 4 (ultimate one) can only be reached by a system alarm or a combination of failures from lower levels 2. Identification of the failures, which can lead to the activation of a reconfiguration sequence. The information is then used to check the absence of border effects on the design.

3. Impact of a reconfiguration sequence on the satellite mode and AOCS mode. It allows one to verify the correctness and completeness of the satellite and AOCS modes automata with regard to the equipment configuration.

The analyses for this case study have been conducted on a standard computer (2GHz processor and 2GB memory). The duration of analysis is dependent on the model. All the analyses completed in less than one hour.

Simulation

Before the verification of the above items, the AADL model was checked for deadlocks. This analysis checks for any dead ends in the system, and it is also needed to ensure the correctness of the verification results. Simulations were then used to generate traces of the model. Both random (where the evolution of the trace is determined by a randomly choosing successor transitions) and guided (where the user interactively chooses successor transitions) have been used. Also traces have been generated with and without fault injections. The main goal of the simulations was to check the sanity and fidelity of the model.

Fault Tree Generation

The first two analysis items (identification of failures leading to a given level of FDIR and the activation of reconfiguration sequence) have been verified by generating fault trees. For each FDIR level, one fault tree has been generated. Each leaf represents a fault, which can lead to this level. In this case, the FDIR level is considered as the feared event. Figure 3 shows the resulting fault tree for the most critical event (level 4).

From the requirements, level 4 can only be reached, when one of five system alarms occurs. The expected result is manually verified using the fault tree.

The second item has been verified similarly. The feared event is the occurrence of the first step of the reconfiguration sequence. Moving to this first step means that the fault occurrence is related to this sequence. One fault tree has been generated for each reconfiguration sequence. Each fault set leading to the reconfiguration sequence has been identified. Then we checked manually, that the FDIR level of the reconfiguration sequence and of the faults set are the same. Each time we identified the same FDIR level for the faults and the sequence. This analysis validates the FDIR level classification of the faults and reconfiguration sequence, by crossing both.

Model Checking

The third item, the impact of the reconfiguration sequence on the satellite, was verified using model checking. We wanted to check that the AOCS units will be in the right status (from requirements), depending on the AOCS mode. The requirement was formalized using the global universality requirement pattern. This pattern must be used for system invariants. Informally, the requirement states that being in mode M implies that unit U has states S. Twenty properties (five units times four modes) have been model checked this way.

Thermal Regulation System

The second case study is a thermal subsystem that regulates the satellite's temperature. It is a co-designed system and performs both active and passive regulation. Passive regulation is achieved by optical solar reflectors, shields, and heat pipes. They have no behavior and are therefore not modeled. Active regulation relies on sensors and heaters at dedicated positions in the satellite. Their position is not taken into account as no requirement uses that information.

Functional Model

The model at functional level covers the whole perimeter of the thermal regulation function. It consists of five subfunctions and twelve elements (five passive and seven active). As the functional representation is represented by the tree decomposition, we have defined a formal pattern used for all functions. The pattern for a function was defined only once (see Figure 4). The AADL code of that pattern is shown in Figure 5.

Safety analyses have been performed to identify the critical path on the function tree. The fault trees allow one to identify the single failure point. This kind of analysis can be used at system level to trade-off different architectures. FMEA tables have been generated too. Due to the simplicity of the model, the results of the analyses were obtained in less than one second.

This functional model's fidelity is interesting at system level. It permits to take into account the passive component and to have a global representation of satellite. For further analysis, this functional model was completed by a more detailed logical model. It takes into account the behaviors of the thermal lines.

Logical Model

The thermal subsystem consists of thermal lines, heaters and sensors. A thermal line consists of two heater lines (nominal and redundant), two safety switches and three thermistors in hot redundancy. If a failure occurs, the software switches the nominal heater line off and enables the redundant one to continue temperature regulation. Figure 6 shows the decomposition of a thermal line. The behavior of the line depends on the computation of the median of the three thermistor's measurements. Based on this value, it switches the heaters on or off, according to the thresholds of the measured temperature.

AADL Model

We only present the interface of the AADL model, which is shown in Figure 7. The descriptions of the interface is presented in Table The AADL model contains the seven active components from the functional model. Each function has been mapped logically on one or several of these components. Two error states have been considered for each unit of the model: (i) for temperature sensor, stuck at min value and stuck at max value, (ii) for the heater, no heating and always heating and (iii) for the switch, stuck at ON and stuck at OFF. An environment model has been used to describe the evolution of temperature. Several reconfiguration sequences have been modeled to move from nominal to redundant switches and to move from nominal to redundant heaters. Three models, describing alternative system designs, have been developed: (M1) without any reconfiguration, (M2) with a reconfiguration from nominal to redundant, and (M2) from nominal to redundant and back (case of transient failure based on ground expertise). The models were analyzed for correctness, reliability, safety and diagnosability capabilities.

Verification

All models have been checked for deadlock-freedom. Model checking was used to verify that the temperature is regulated between the lower and upper bounds of the safe range under nominal operation. Several simulations has been performed for sanity-checking the model. Figure 8 shows a simulation with an injected fault on a heater and the switch to the redundant one.

Safety & Dependability

Fault trees and FMEA tables have been generated. They conform to the expectations. The general form of the fault tree shows the absence of a single point of failure. All the fault sets have at least cardinality two. Fault detection analysis has been used to verify that there exists a means of detecting each feared event. Fault isolation analysis has been conducted too. It provides for each observable the list of faults set to which the observable is sensitive. The two analyses are sufficient to validate the observability of the modeled system. The collected data have been used to improve the dependability of the thermal regulation line from a hardware and software point of view.

Recovery Analysis

The main objective was to determine which designs were able to sustain multiple faults by recovering from them. The three configurations of the model (without reconfiguration, with simple reconfiguration and with double reconfiguration) have been checked with the fault recovery analysis. The results are outlined in Figure 9. The columns names indicate failure configurations for the nominal heater (named H1 in Figure 9) and the redundant heater (named H2 in Figure 9).

Scalability

Two synthetic benchmarks have been crafted to measure the scalability of the toolset. The adder benchmark is parametric in the number of input modeled. Higher number of inputs increase the model's size. The sensorfilter benchmark is parametric in the degree of redundancy. A higher level of redundancy increases the model's size. The three analysis engines fundamental to all the supported analyses were benchmarked using these two synthetic benchmarks.

The BDD-engine is used for time-abstract models. The results for this engine (see Figure 10) shows that an increasing number of bits (indicating the model's complexity) leads to a higher computation time. As the figure shows, the increase grows exponentially.

The SAT-engine can be used for time-abstract models and is mandatory for timed and hybrid models. The results from the synthetic benchmarks (see Figure 11) shows a similar trend akin to the BDD-engine although this engine can cope with larger models easier. Table 2: Scalability of the probabilistic engine. The complexity is measured as the degree of redundancy.

The probabilistic engine is computationally heavier. Our results with the sensorfilter benchmark (see Table 2) have shown that the computation time increase exponentially with the model's complexity.

The nature of the algorithms used by the toolset show that the computation time increases exponentially with the model's size. The evaluation by the industrial partner has however shown that the current engines are fast enough to allow for mildly complex models, provided they are modeled with reasonable care.

Conclusion

We introduced a comprehensive and coherent methodology for the design of complex safety-critical systems. Our approach is applicable to any domain where, e.g., timing, system performance and safety are at stake. Examples are avionics, transportation, including railways and automotive, power and the medical domain. The methodology is based on a formal specification language that is derived from AADL and its Error Model Annex. It supports a variety of V&V activities such as consistency analysis, simulation, correctness verification, performability evaluation, dynamic fault tree generation, FMEA table generation, FDIR, and diagnosability analysis. These are implemented by a graphical toolset which integrates state-of-the-art analysis and verifica-tion tools.

An industrial partner evaluated the methodology using their own case studies has taken place as part of the COMPASS project. They have shown that AADL provides enough expressiveness to model all the hardware and software subsystems in satellite avionics. They found that the hierarchical structure and the component-based paradigm enabled them to reuse models from one satellite to another. Also the approach supported their incremental modeling approach. The results provided by the RAMS analyses allowed the evaluation of design alternatives. An issue was however scalability. It is foreseen that larger models come with increased computation time. A follow-up research project has been approved by the European Space Agency to tackle this issue.

A comprehensive report of the COMPASS project can be found in [START_REF] Bozzano | Safety, dependability, and performance analysis of extended AADL models[END_REF]. It describes the modeling language, its semantics, the toolset and the supported analyses in more detail.

Figure 1 :

 1 Figure 1: Main screen of the COMPASS toolset with AADL models loaded.

Figure 2 :

 2 Figure 2: Synopsis of PUS mechanism used for reconfiguration.

Figure 3 :

 3 Figure 3: Generated fault tree for FDIR level 4.

Figure 4 :

 4 Figure 4: Automaton pattern of a function.

then

  Operational := true ] -> Activated ; Idle -[ Deactivate then Operational := false ] -> Deactivated ; Deactivated -[ Activate then Operational := true ] -> Activated ; Activated -[ Deactivate then Operational := false ] -> Deactivated ;end Function . Impl ;

Figure 5 :

 5 Figure 5: AADL code pattern of a function.

Figure 6 :

 6 Figure 6: Structure of a thermal line.

Figure 7 :

 7 Figure 7: Interface of thermal line component.

Figure 8 :

 8 Figure 8: Simulation with fault injection.

Figure 10 :Figure 11 :

 1011 Figure 10: Scalability of the BDD-based engine. The size N means the number of Boolean variables needed to hold a model's state.

Figure 9 :

 9 Figure 9: Results for fault recovery analysis.

  1.

	system Function
	features
	Activate : in event port ;
	Deactivate : in event port ;
	Operational : out data port bool
	default false ;
	end Function ;
	system implementation Function . Impl
	modes
	Idle : initial mode ;
	Activated : mode ;
	Deactivated : mode ;
	transitions
	Idle -[ Activate

Table 1 :

 1 Meaning of thermal line component ports.

	Input Port	Type Description
	T1, T2, T3	data measured values from thermistors
	enable line	event externally switch line on
	disable line	event externally switch line off
	enable monitor event switch monitoring on
	disable monitor event switch monitoring off
	do	event used for simulation
	Output Port	Type Description
	nom is heating data status of nominal heater
	red is heating data status of redundant heater
	is enabled	data status of thermal line
	is monitored	data status of monitoring
	current used	data	currently used heater (nominal/redundant)
	done	event used for simulation