# A Methodology for Increasing the Efficiency and Coverage of Model Checking and its Application to Aerospace Systems.

ABSTRACTFormal Methods, and in particular Model Checking, are seeing an increasing use in the Aerospace domain. In recent years, Formal Methods are now commonly used to verify systems and software and its correctness as a way to augment traditional methods relying on simulation and testing. Recent updates to the relevant Aerospace regulations (e.g. D0178C, D0331 and D0333) now have explicit provisions for utilization of models and formal methods. At the system level, Model Checking has seen more limited uses due to the complexity and abstractions needed. In this paper we propose several methods to increase the capability of applying Model Checking to complex Aerospace Systems. An aircraft electrical power system is used to highlight the methodology. Automated model-based methods such as Cone of Influence and Timer Abstractions are described. Results of those simplifications, in combination with traditional Assume-Guarantee approaches will be shown for the Electric Power System application.

CITATION: Ferrante, O., Scholte, E., Pinello, C, Ferrari, A. etal., "A Methodology for Increasing the Efficiency and Coverage of Model Checking and its Application to Aerospace Systems," SAE Int. J. Aerosp. 9(1):2016, doi: 10.4271/2016-01-2053.

INTRODUCTION

Model Based Design has been extensively applied in the automotive and aerospace domains. It often relies on the use of virtual prototypes (e.g. models) for validation and verification of system requirements. Many of these approaches rely on simulation in order to cover the operational space, through models, Hardware-In-the-Loop and physical testing. Several instances have shown that depending on the nature of the underlying dynamics it is possible to miss certain corner cases. This is particularly true for hybrid systems where the ordering of events can create challenges to define a good set of tests. To cope with these challenges Formal Methods [6, 11] and in particular Model Checking [2] have been used to augment those approaches. Figure 1 shows the overall Model Checking approach where the two main inputs are the system model and the requirement (i.e. specification).

The application of model checking to Cyber Physical Systems (CPS) including physical, control and communication systems, has received much attention, such as the focus on hybrid systems verification [9], as well as the use of probabilistic model checkers (e.g. PRISM [10]).

The work in this paper focuses on the use of model checking for the application to CPS, but using the traditional finite state representations. Rather than attempting to capture the physical dynamics more accurately the approach here focuses on the automated methods to handle large scale industrial problems.

In order to be able to apply Model Checking, the underlying model is typically assumed to be of Finite State [3], and as is detailed later in this paper often requires the modeler to make the appropriate system level abstractions when dealing with Cyber-Physical systems (CPS). In the recent years Model Checking has been applied to aerospace applications, at both the system and software levels. Traditionally application at the software level has shown great benefits and has led to adoption within the aerospace verification guidelines as an alternate method for creation of verification evidence. Application at the system level has seen less wide adoption due to the challenges involved. Most of these challenges stem from the complexity growth [7] that hampers the efficiency of model checkers, as well as the inherent use of model abstractions of complex dynamics. However, recent advances in both computational capabilities, as well as algorithmic improvements (see the later discussion) have enabled successful applications [1, 4, 5] to more complex systems and can be utilized as a way to detect issues early in the design phase.

MOTIVATING EXAMPLE: AIRCRAFT ELECTRIC POWER DISTRIBUTION SYSTEM

Electric Power Systems for commercial aircraft are becoming more critical as the overall trend toward more electric aircraft continues. The recent trends have resulted in an increased reliance on electrical power on the aircraft. A system level view of a typical power system is shown in Figure 2. It shows a Single Line Diagram (SLD) that consists of generating sources: {LGEN, RGEN, ExtPwr, APU, Batt} that represent the generators, the external power coming from a ground cart, the Auxiliary Power Unit, and the battery. In addition it shows the electro-mechanical switches that can be closed to route power to its appropriate loads. Typically a few loads are connected directly onto the system (either AC or DC power), whereas the bulk of the loads would be distributed by a secondary power distribution system (not shown).

The control of the primary power distribution system has to be designed such that switching of power sources happens in a coordinated manner. The control algorithm itself is usually implemented in a distributed set of physical controllers for redundancy reasons. This system can be expressed as a hybrid finite state machine where the continuous dynamics are due to the generators and the electromechanical switches, and the finite state behavior due to the control system.

The objective is to verify the system level behavior and typically system properties. An example is to ensure that the control system will not erroneously connect two variable frequency sources at any point in time. For the subsystem shown in Figure 3 two sources (S1, S2) are shown and can be connected using two contactors (C1, C2). The specification can be expressed using for example Linear Temporal Logic (LTL) as:

G((ACBUS_powered_by_Sl) &(ACBUSj)owered_by_S2))

Where ACBUS_powered_by_Sl is computed based on the discrete states of SI and CI, and likewise A CBUS_powered_by_S2 is computed based on the discrete states of S2 and C2.

Similarly properties can be expressed based on other system requirements, such as performance as well as timing constraints. In addition, checking properties that are impossible to verify by testing can be a key reason for application of Formal Methods. The absence of deadlock and livelock conditions is a key concern when designing distributed real-time systems.

VERIFICATION METHODOLOGY AND TECHNOLOGY

The verification methodology can be summarized in four main parts as shown in Figure 4.

Design Model Definition

During the Design Model definition the control algorithm and the plant models are developed starting from System Requirements. The use of standard modelling guidelines allows for the disciplined use of Simulink/STATEFLOW language constructs. This step can be seen as the "classical" model-based representation of System Requirements.

Verification Model Definition

During this phase additional modelling artifacts are defined for the subsequent application of the formal analyses. These modeling artifacts represent the requirements or properties against which the model is analyzed or additional constraints that should be provided to the formal engine. The output of this activity is the formal problem to be analyzed.

Compositional Verification

During this phase the formal problem is decomposed using both manual and automatic techniques. The objective of this phase is to produce a set of formal models that are simpler from a verification complexity point of view and that can be used to prove the correctness of the original model composing the proofs obtained using the derived model.

Analysis Execution and Results Evaluation

During this phase the formal analysis is performed and results are evaluated. In case a property is found false, the produced counterexample is analyzed and possible change requests to the System Requirements associated to the model and the property are performed.

In the next sections we will provide a more detailed view of the described steps as well as the technology chain used to perform the analyses.

VERIFICATION MODEL DEFINITION

The input of the verification model definition phase is the Design Model (Figure 6) developed during the previous phase. It contains both the control algorithm model and the physical plant model. The main activities performed in this phase are:

* The property formalization during which the property to be formalized is encoded using a formal language.

* The development of an environment model and property assumptions that are required to perform the verification step efficiently

* The design and plant model abstractions which are required when the original design model contains constructs that are unsupported by the formal engine, or cannot be processed due to model size or complexity.

In the next sub-section an overview of each activity is provided.

Property Formalization

During this step the property to be verified against the system is formalized using formal language. The choice of the formal language to be used for the formalization impacts the effectiveness of the subsequent simplification and analysis phase. Among the different formal languages that have been used we report three approaches currently adopted.

Linear Time Logic Formulae

Often the application of Formal Methods is used to check key properties of distributed control systems and absence (i.e. negative requirements) of deadlock and livelock conditions. Temporal Logic formulae are adopted for the formalization of liveness requirements. In the context of verification for distributed control systems they have been used for the analysis of deadlock freedom and livelock freedom by encoding these conditions as liveness LTL properties.

Finite State Monitors

A monitor (also known as observer) is a finite-state machine that takes as inputs both inputs and outputs signals of the System Under Analysis and that has as output a Boolean value. At every time step the monitor check the value of System inputs and outputs and assigns to its output a TRUE value if they satisfy the property it represents, otherwise it signals a property violation assigning a FALSE value. Monitors are commonly used in both formal and run-time verification. Each monitor encodes an invariant which is a Boolean condition that must always be true and they can be used to represent both safety properties and bounded-liveness properties that can be reduced to (possibly non-deterministic) finite state machines.

Specification Patterns

The definition of properties using LTL formulae or finite state monitors can be time consuming and error prone. In addition, since natural language requirements are inherently ambiguous, the formalization of the same property from different engineers may lead to different encodings of the formal properties. The use of patterns mitigates both aspects. A pattern is a reusable formalized library block that represents a natural language sentence containing free inputs called parameters. Each pattern encapsulates an interpretation of the natural language sentence.

Example

As an example let us consider the following Textual Pattern provided with the Formal Specs Verifier Block-based Constraint Pattern Library [18,19]:

Once [C] goes [V], it remains [V] for [T]

The parameters of the pattern are the Boolean condition [C] the Boolean value [V] and the time internal [T]. This pattern is encoded as an LTL specification as follows:

G[(C = V) [right arrow] [G.sub.T](C = V)]

where [G.sub.T] is shorthand for globally for a number of steps and it is implemented as a Simulink monitor block exposing at the interface the three inputs related to the three conditions and as output a Boolean output representing the satisfaction of the pattern.

Patterns libraries can be developed for specific domains representing modeling assets that reduce the time required for the properties formalization and verification. In addition the use of patterns allows the use of complex temporal logic expressions without requiring the knowledge of temporal logic.

Assumptions Identification

A key aspect of a verification analysis is the definition of the assumptions under which the property to be evaluated should be verified. Assumptions represent "enabling conditions" that the system should satisfy in order to evaluate the property. Even if from a formalization point of view assumptions can be encoded as part of the property, the identification of an explicit assumption identification step allows for better identifying such enabling conditions mitigating the risk of limited or incomplete property formalization.

Environment Model

In addition to the formalized property and related assumptions, during this phase the environment model is identified and formalized. In the context of verification, the environment is defined as the collection of external actors that interact with the System. These actors are both physical - such as the pilot that can interact using the switches - and functional - such as the occurrences of faults that leads to a specific failure in the plant. The environment model contains a formal representation of both requirements and domain knowledge related to what is external to the controlled system. From a methodology applicability perspective, the identification of such component is fundamental to avoid the generation of spurious counter-examples that are corner cases that violates the properties but shows unreasonable or unlikely scenarios such as the simultaneous occurrence of two inputs or opposite faults. It is important to stress that the environment represents a different set of constraints w.r.t. property's assumptions: the latter are property-specific condition and belongs to the single property verification "knowledge domain" while the former are system-wide constraints that need to be taken into account by all properties hence representing a global set of constraints. The combination of these two "levels" of knowledge - model and property - is a key part of the verification methodology pruning unnecessary behaviors and focusing the search only to relevant behaviors sub-sets.

Abstractions

Classical Model-Based Design methodology places emphasis on the use of models for simulation and automatic code generation. Detailed control and plant models represent a key aspect of such techniques since the effectiveness and usefulness of the results strictly depend on the quality and fidelity of the models. This is true also for the application of formal analysis in the context of Model-Based Design with some additional complexities. Formal engines, due to the exhaustive nature of the search they perform, are inherently limited in terms of supported modeling constructs and model size. In order to successfully overcome such limitations several abstractions should be applied in order to reduce the size of the search space or avoid the use of unsupported constructs (such as non-linear operations). Every applied abstraction should be proved to be sound to ensure that the abstracted model represents an over-approximation of the original and that the analysis of the abstracted model does not eliminate possible system hazardous behaviors. In the next sub-sections some of the abstraction techniques we adopted during the verification of the EPS systems are summarized.

Time Discretization

Cyber-Physical Systems models contain both discrete-time and continuous-time evolutions. To apply model checking at an industrial scale it is required to reduce the model to have discrete-time evolutions only. This results in abstracting plant's components

continuous evolution to the discrete time domain.

Regions Abstraction

Regions abstractions represent (possibly infinite) values domains as finite sets of discrete values. In the EPS case this technique has been applied extensively for the abstraction of complex plant evolution. An example of region abstraction has been applied for the representation of plant power flows that have been represented by Boolean values with logical TRUE the presence of power and logical FALSE the absence of power.

Control systems contain different level of counting processes in forms of timers. A timer is enabled by a triggering event and after a predefined number of counting steps, expires asserting a Boolean timeout output. The presence of counters increases the complexity of the model checking problem. The objective of timers rescaling simplification is to reduce the overall diameter of the model by reducing the number of steps before timeouts occur, ensuring at the same time that the relative sequencing and order of timeouts is preserved.

COMPOSITIONAL VERIFICATION METHODOLOGY

The use of abstraction, environment modeling and property assumptions produces verification models that can be processed by formal engines. Current engines are already at a level of maturity that can tackle a significant portion of the verification models without additional manual intervention. However, for complex, closed loop distributed cyber-physical systems, additional actions should be performed to further simplify the formal model and to allow the application of off-the-shelf model checkers. The main objective of the compositional verification activities is to define a set of steps and guidelines to reduce the overall complexity of the formal model before executing the verification step.

Defining a single complexity measure for the application of model checking to finite state machines is in general not possible. As a consequence the compositional verification methodology we propose is based on best practice and heuristics that have been proven effective on an extended portfolio of Electrical Power System models. The main driver of complexity reduction is the model size which can be defined for model containing only bit vectors as the cumulative size in bit of the model state (inputs and state variable). The described heuristics aims at reducing the effect of state space explosion by reducing the size of the model to be verified. The followed approach is represented in Figure 7 and in the next subsection a brief overview of adopted heuristics is given.

Additional Abstractions

In case the formulated problem (verification model) is not manageable in terms of verification complexity, an additional abstraction step may be required. During this phase the employed abstractions should be sound so that they preserve properties that are TRUE and be capable of producing counter-examples that can be checked against the original model. In case a spurious counterexample is found, a refinement procedure is performed identifying the root cause of the counter-example and refining the abstraction to avoid its occurrence.

Property Decomposition

Property decomposition aims at exploiting the structure of the design model - i.e. the physical or functional architecture of the model under verification - to split (decompose) a property that is allocated to several components to several properties each allocated to a single component. The underlying assumption is that a localized property is allocated to a portion of the model hence their cone-of-influence is reduced in size and the overall size of the formal problem can be reduced. The decomposition process should be sound i.e. the composition of the local properties should be proven equivalent to the original property. In the following sub-sections we provide a brief overview of two decomposition techniques.

Property Decomposition to Sub-Components

When properties allocated to multiple components can be modeled as a conjunction of sub-properties allocated to the sub-components, we partitioned the property following the model architecture and performing the subsequent automatic simplification and verification phases for each of the new properties. This approach has greater benefit when each sub-properties is allocated to single subcomponents improving the benefit of automatic simplifications such as cone-of-influence [31],

Example

As an example consider the abstract description the Electric Power Distribution system represented in Figure 8. One of the top-level system properties that are required to be verified by the closed-loop controlled system is the absence of deadlocks during power transfer. The deadlock condition is encoded as a monitor that observe the value of specific control algorithms output and identifies a deadlock in terms of absence of bounded response: in case status of the control algorithm does not change for a given amount of time after the occurrence of a triggering event a (time bounded) deadlock is flagged (output DL goes to TRUE).

The overall deadlock property for this system can be stated using an invariant pattern as follows:

[ not DL ]

which imposes that the DL output should never be TRUE. This property is in general complex to be proven for industrial scale EPS models thus further decomposition is required to identify smaller-sized problems to be solved. A possible decomposition of the property can be performed analyzing the functional architecture of the control algorithm. In particular we can decompose the algorithm in two parts: function Fund and function Func2. The deadlock property can be stated by observing the output of the function separately and can be then decomposed in the conjunction of two properties guided by the functional decomposition of the algorithm as follow:

[not DL] = [not DL1 and not DL2]

Where DL1 represent the deadlock property localized observing the output of function Fund and DL2 for function Func2. Verifying the two properties separately allows one to verify the overall deadlock property.

Assume-Guarantee Decomposition

This technique is applicable to properties that can be formalized as a precondition-reaction statement of the form

A[right arrow]C

where A is an assumption and C the guarantee [32, 21, 8].

Assumptions can be interpreted as precondition over inputs of the system under which the guarantee must hold. The property can be decomposed in two sub-properties guided by the architecture of the system. In particular, if we identify an additional property on internal signals B for which the following rule holds

(A [right arrow] B [LAMBDA] B [right arrow] C) [right arrow] (A [right arrow] C)

to prove the original property it is sufficient to prove the two sub-properties A [right arrow] B and B [right arrow] C that are allocated to a sub-set of components. The underlying idea is to decompose the proof of the original property in two sub-properties that are local to subcomponents hence reducing the overall size of the model under verification.

Example

Continuing the previous example, the deadlock condition should be avoided under all possible occurrences of simultaneous faults up to a given number The refined version of this can be formalized as follows (we cover the case of absence of faults to simplify the formalization):

[F=0] implies [not DL]

Driven by the structure of the functional architecture (Figure 9) we can further decompose this property noting that in absence of faults the Fault Detected signal (FD) must be FALSE and in presence of faults it must be TRUE.

Hence we can decompose the property in two sub-properties as follows:

[F=0] implies [not FD] and [not FD] implies [not DL]

By proving each property separately we prove the global property [F=0] implies [not DL]. Since each sub-property is allocated to a sub-set of the subsystem of the original model, proving the two properties separately is usually simpler than proving the single monolithic property since we operate a "cut" on the original model when the FD signal is located splitting the model in two parts that usually are smaller in size w.r.t. the entire model.

Environment Decomposition

The environment identifies the constraints that the inputs of the controlled system must satisfy and it allows for a reduction of the state space to be analyzed by the analysis engine. To further reduce the variability of system inputs, the environment admissible behaviors can be further decomposed in sub-sets of behaviors by imposing additional constraints that can be exploited by the automatic simplification and verification engine.

Example

The deadlock property can be stated more precisely as follows

[count( F ) < N ] implies [not DL]

That states that the deadlock condition should not occur when the maximum number of simultaneous faults is less than a given number N (let us assume N to be 2). The fault condition occurrences can be further decomposed into a set of possible cases as follows

[count(F) = 0 or count(F) =1 or count(F) = 2] implies [not DL]

And each case can be separately verified in order to prove the absence of deadlock using the following logical rule:

[(A [disjunction] B [disjunction] C) [right arrow] D] [left and right arrow] [(A [right arrow] C) [LAMBDA] (B [right arrow] D) [LAMBDA] (C [right arrow] D)]

Hence the verification of the property can be decomposed in three sub-properties each focusing on a specific fault occurrence scenario (no fault occur, at most one fault occur, at most two fault occur) decomposing the environment behavior in three equivalence classes. Environment decomposition is usually combined with property decomposition splitting a single property that insists on the entire model in a conjunction of properties that are allocated to sub-systems reducing the complexity of the formal model to be verified.

VERIFICATION METHODOLOGY

Depending on the complexity of the model under analysis, different algorithms can be applied among the rich portfolio proposed by current model checkers tools. Defining the application of a single algorithm for the class of system under analysis is not possible since different algorithms may perform differently for different models or, within the same model, for different property. The verification methodology we found effective for the evaluation of properties for EPS represented in Figure 10.

The inputs of the verification process (in addition to the model to be verified) are the maximum timeout of the verification and the maximum bound that should be reached using bounded verification techniques (such as bounded model checking). The verification strategy is based on three steps. During the first phase a bounded model checking algorithm is chosen and bounded verification is performed. If the verification does not succeed (e.g. results are not produced within the expected bounds), a falsification algorithm is selected and the property is checked using a deep bound. Finally, if the property has not been still verified or falsified a verification algorithm, such as a BDD-based algorithm, is selected and used to prove the remaining properties within the given timeout.

Automated Simplification Methods

The adopted tool chain allows for the application of several off-the-shelf model simplifications algorithms currently offered by state of the art model checkers. The main objective of the previously described techniques is to produce models that can be effectively processed by automatic algorithms reducing the complexity of the formal problem to be solved by the model checking engine. Our toolchain is mainly focused on the simplification algorithms provided by the NuSMV/nuXmv toolset [14, 24]. Among the most effective we cite the cone-of-influence simplification that allows for pruning parts of the model that are not syntactically connected to the property under analysis, the timers acceleration technique implemented in nuXmv, the constant propagation simplification and state space reduction model transformation based on static analysis techniques. We refer to [1_4] for a more detailed explanation of such simplification techniques.

TOOLCHAIN ARCHITECTURE

The methodology described in previous paragraphs is based on an industrial strength toolchain that is architected in three major layers (Figure 11). The modeling layer is based on the Simulink/STATEFLOW modeling environment [12]. Both the distributed control system and the plant models have been represented as Simulink/STATEFLOW finite state machines. The models are processed by the Formal Specs Verifier (FSV) verification Framework (model transformation layer). The final layer (model checking layer) includes the engines that are employed to perform the proof. In the next sub-section the model-transformation and engine layers will be described in more details.

Model Transformation Layer

The model transformation layer is based on the Formal Specs Verifier (FSV) verification framework. The FSV is an ALES/UTC Framework that processes Simulink/STATEFLOW models producing a formal model that can be elaborated by state-of-the art model checking tools. A high-level representation of the model transformation flow is provided in Figure 11.

During a model parsing phase a full MATLAB API-based procedure extracts the entire set of information associated with the verification model reconstructing it in memory and producing an intermediate formal representation of the parsed data. The produced intermediate representation is processed during the Formal Problem Formulation step that produces as outputs a formal model that can be processed by model checking engines and mappings information that can be used to reconstructs the mapping between the source Simulink model elements and formal model elements. The model transformation step is performed using a Java implementation of the QVT standard language [13] called JQVT and it is built on top of the Eclipse Modeling Framework [29].

The produced formal model is optimized exploiting domain-specific information embedded in the verification models (specification patterns and environment model). At the end of this phase the optimized model is serialized using the standard XMI technology [30].

A final model-to-text step produces textual or binary artifacts that can be used to feed model checking engines. Currently the supported output formats are nuXmv [14, 24] and ABC [28].

When a counter-example is generated by the model checkers, an harness model generation step produces a Simulink/Stateflow model that reproduce the counter-example exploiting the mapping information serialized during the formal model production step fFigure 12).

The FSV framework has been extensively used in both industrial and research projects [16. 21.22], and several plugins are available for the verification of embedded systems [15]. synthesis of failure scenarios [17]. automatic test generation [20, 23] and requirements validation [16].

Several frameworks have been developed in the past and are currently under development for the formal verification of Simulink/STATEFLOW model. In [25] the authors describe a framework for the translation of Simulink models to NuSMV based on mdl model parsing and processing. The Design Verifier framework [26] is an industrial strength product for the formal verification of Simulink and Stateflow models and in [27] a toolchain for the formal analysis of Simulink/Stateflow models is described using several back-end engines. The FSV toolchain differs from these approaches in several ways. Our approach is based on a full model parsing based on MATLAB API, not relying on the parsing of an input artifact. In addition the outcome of the model transformation is an intermediate formal model that is optimized and several back-ends are targeted for the verification. The FSV framework can be seen as complementary to the Simulink Design Verifier [26] and similar approaches since the tool supports only a subset of the modeling features allowed by Simulink/STATEFLOW and implements problem specific optimization highly focused on the domain-specific verification challenges encountered in industrial applications.

Model Checking Layer

The toolchain has recently integrated the nuXmv model checkers among the others. The nuXmv model checker is a state-of-the-art tool for the verification of finite and infinite state systems and offers a set of industrial strength model simplification algorithms and a rich portfolio of verification algorithms including Bounded-Model Checking, Interpolation-based algorithms, Property Driven Reachability among the others. In addition, custom extension of the engine has been implemented [15] including additional customized algorithms tuned for the specific verification challenges that are encountered in the CPS verification domain.

RESULTS

The approach outlined in the prior sections was used on a larger scale electric power distribution system, similar to the motivating example shown in the introduction sections. The system consists of a number of distributed controllers that communicate with each other, and a model of the plant. The controllers are mainly based on discrete-time Boolean logic. The system Simulink model has about 220,000 blocks.

A key ability for this approach to work for industrial sized problems is the managing of complexity for the underlying algorithms. A first step in the handling of that complexity is the ability to automatically reduce the problem size, without any abstractions or loss of critical behaviors. Figure 13 shows the results of automated simplification steps as applied to the full original problem. The subsequent steps are: Typically the order in which the simplifications are applied has a minor effect on the final system complexity, but can be applied in an iterative fashion until a steady state problem size has been found. In this figure it shows the complexity decrease for the input variables, the states as well as the decision variables. It is visible that the problem size (decision variables) is almost an order of magnitude less complex than the original starting point.

The impact of the simplification techniques is significant. The main reasons are the following. First, in real designs most variable data types usually allow a much larger data range than actually used. Second, some portion of the system is not related to the system property to be verified. Third, some variables represent the same signal, but may have different names due to model hierarchy.

Subsequently the models are subjected to a bounded model checking approach. Figure 14 shows the depth of the run (number of finite steps) versus the computation time. The exponential growth is clearly visible. Three different trajectories are plotted: original (blue), simplified subsystem (red), and one where an assume-guarantee approach is used (green). The latter approach assumed one of the controllers that hosts part of the functionality to be "correct" and then proving the property (lack of deadlock) is true for the other controller.

By decomposing the problem into two major subsystems a significant increase in efficiency is achieved (10X).

CONCLUSIONS & NEXT STEPS

In this paper we highlighted recent improvements to methods and tools for application of Formal Methods to aerospace systems. As more systems are using complex software control the verification challenge is increasingly difficult to perform. Traditionally simulation based methods have been used to support verification, but are limited in terms of achievable coverage. In order to augment these methods with model checking the designers have to be able to deal with the state explosion challenge. In the paper we proposed an approach that relies on system methodologies and automated methods to aid the designers with the application to industrial sized problems. The results have shown that these methods are now enabling the designers to utilize Formal Methods to aid with the coverage of the corner cases.

The proposed methodologies and technologies have been proven effective in several industrial cases within United Technologies Aerospace Systems and in particular in the area of verification of Electrical Power Systems. However, several areas need to be improved and developed in future research to face the continuous evolving challenges for the verification of complex cyber physical systems

On the methodology side, the definition of the "correct" abstraction to be applied for a specific model type is a broad and not yet completely answered question. The definition of abstraction patterns that encodes the abstractions to be applied and the condition under which they should be applied is a major point of attention to broaden the application of formal techniques to different systems or to improve the applicability of the methodology across different programs.

Concerning the technology aspects, the application of model checkers for infinite state and hybrid systems enlarges the potential scope of applicability of formal methods to a richer set of challenges and represents a point of attention and investigation for future research.

REFERENCES

[1.] Miller, Steven P. and Whalen, Michael W. and Cofer, Darren D., Software model checking takes off, Communications of the ACM. Volume 53, No 2, 2010.

[2.] Clarke E.. "Model checking". In Ramesh S. and Sivakumar G., editors, Foundations of Software Technology and Theoretical Computer Science, volume 1346 of Lecture Notes in Computer Science, pages 54-56. Springer Berlin / Heidelberg, 1997. 10.1007/BFb0058022.

[3.] Clarke E. M., Emerson E. A., and Sistla A. P.. "Automatic verification of finite-state concurrent systems using temporal logic specifications." ACM Trans. Program. Lang. Syst, 8:244-263, April 1986.

[4.] Dutertre B. and Stavridou V.. "Formal requirements analysis of an avionics control system". IEEE Transactions on Software Engineering, 23:267-278, 1997

[5.] Hamilton D., Covington R., Kelly J., Kirkwood C, Thomas M., Flora-Holmquist A. R., Staskauskas M. G., Miller S. P., Srivas M., Cleland G, and MacKenzie D.. "Experiences in applying formal methods to the analysis of software and system requirements". In Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques, pages 30-, Washington, DC, USA, 1995. IEEE Computer Society

[6.] Holzmann G. J.. "The model checker spin." IEEE Transactions on Software Engineering, 23:279-295, 1997.

[7.] McMillan K. L.. "Symbolic model checking: an approach to the state explosion problem". PhD thesis, Pittsburgh, PA, USA, 1992. UMI Order No. GAX92-24209.

[8.] Nuzzo, Pierluigi, et al. "A contract-based methodology for aircraft electric power system design." Access, IEEE 2 (2014): 1-25.

[9.] Henzinger Thomas A., Pei-Hsin Ho, HowardWong-Toi, HYTECH: a model checker for hybrid systems, Int J STTT (1997) 1: 110-122

[10.] Kwiatkowska, M.; Norman, G.; Parker, D. (2011). "PRISM 4.0: Verification of Probabilistic Real-time Systems". In Proc. 23rd International Conference on Computer Aided Verification (CAV' 11), volume 6806 of Lecture Notes in Computer Science, pages 585-591, Springer.

[11.] Owre S ., Rushby J. M., and Shankar N." PVS: Aprototype verification system". In Kapur D., editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748-752, Saratoga, NY, jun 1992. Springer-Verlag.

[12.] http://www.mathworks.com/products/simulink/

[13.] http://www.omg.org/spec/OVT/index.htm

[14.] Cavada R., Cimatti A., Dorigatti M., Griggio A., Mariotti A., Micheli A., Mover S., Roveri M., Tonetta S. The nuXmv Symbolic Model Checker Computer Aided Verification Lecture Notes in Computer Science Volume 8559 pp 334-342

[15.] Ferrante O, Benvenuti L., Mangeruca L., Sofronis C. and Ferrari A., "Parallel NuSM V a NuSM V extension for the verification of complex embedded systems", Computer Safety, Reliability, and Security, Lecture Notes in Computer Science Volume 7613, 2012, pp. 409-416

[16.] Mangeruca L., Ferrante O, Ferrari A., "Formalization and completeness of evolving requirements using Contracts", 8th IEEE International Symposium on Industrial Embedded Systems (SIES 2013), 19-21 June 2013, Porto, Portugal

[17.] Marazza M., Ferrante O, Ferrari A., "Automatic Generation of Failure Scenarios for Sytems-on-Chip", Real Time Software and Systems, ERTS 2014, Tolouse

[18.] Ferrante O, Ferrari A., Mangeruca L., Passerone R., Sofronis C, D'Angelo M., "Monitor-Based Run-Time Contract Verification of Distributed Systems", 2014, 9th IEEE Symposium on Industrial Embedded Systems, Pisa, 2014

[19.] Ferrante O, Ferrari A., Mangeruca L., Passerone R., Sofronis C, "BCL: a compositional contract language for embedded systems", 19th IEEE International Conference on Emerging Technologies and Factory Automation, Barcelona, 2014

[20.] Ferrante O, Ferrari A., Marazza M., "An algorithm for the incremental generation of high coverage tests suites", 19th IEEE European Test Symposium, 2014, Paderborn

[21.] Carloni M., Ferrante O, Ferrari A., Massaroli G., Orazzo A., Petrone I., Velardi L., "Contract-Based Analysis for Verification of Communication-Based Train Control (CBTC) System", SAFECOMP 2014, Firenze

[22.] Carloni M., Ferrante O, Ferrari A., Massaroli G., Orazzo A., Petrone I., Velardi L., "Contract Modeling and Verification with Formal Specs Verifier Tool-Suite - Application to Ansaldo STS Rapid Transit Metro System Use Case", SAFECOMP 2015

[23.] Ferrante O, Ferrari A., Marazza M., Formal Specs Verifier ATG: a Tool for Model-based Generation of High Coverage Test Suites, ERTS 2016, Tolouse

[24.] Cimatti A., Clarke M. E., Giunchiglia E., Giunchiglia E, Pistore M., Roveri M., Sebastiani R., and Tacchella A"NuSMV 2: An OpenSource Tool for Symbolic Model Checking" In Proceedings of the 14th International Conference on Computer Aided Verification (CAV '02), Brinksma Ed and Larsen Kim Guldstrand (Eds.). Springer-Verlag, London, UK, UK, 359-364.

[25.] Balasubramanian, M. and Bhatnagar, A. and Roy, S., Automatic translation of simulink models into the input language of a model checker, US Patent App. 11/545,134, 2008, https://www.google.com/patents/US20080086705

[26.] http://www.mathworks.com/products/sldesignverifier/?refresh=true

[27.] Whalen, M., Cofer, D., Miller S., Krogh, Bruce H, Storm, W. "Integration of Formal Analysis into a Model-based Software Development Process" Proceedings of the 12th International Conference on Formal Methods for Industrial Critical Systems, 2008, Berlin, Germany

[28.] Brayton R., Mishchenko A. "ABC: an academic industrial-strength verification tool" In Proceedings of the 22nd international conference on Computer Aided Verification (CAV 10), Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer-Verlag, Berlin, Heidelberg, 24-40. DOI=http://dx.doi.org/10.1007/978-3-642-14295-6_5

[29.] https://eclipse.org/modeling/emf/

[30.] http://www.omg.org/spec/XMI/

[31.] Clarke, E. M., Grumberg O, Peled D. A. "Model Checking", 1999, MIT Press

[32.] Benveniste A., Caillaud B., Ferrari A., Mangeruca L., Passerone R., and Sofronis C. "Multiple Viewpoint Contract-Based Specification and Design". In Formal Methods for Components and Objects, Boer Frank S., Bonsangue Marcello M., Graf Susanne, and Roever Willem-Paul (Eds.). Lecture Notes In Computer Science, Vol. 5382. Springer-Verlag, Berlin

CONTACT INFORMATION

Orlando Ferrante, ALES S.r.l. Advanced Laboratory on Embedded Systems, United Technologies Research Center, Piazza della Repubblica, 68 - 00185 Rome - Italy

Orlando.ferrante@utrc .utc .com

Eelco Scholte UTC Aerospace Systems, 4747 HarrisonAve., Rockford, IL 61125

eelco.scholte@hs.utc.com

Orlando Ferrante

United Technologies Research Center

Eelco Scholte

UTC Aerospace Systems

Claudio Pinello, Alberto Ferrari, and Leonardo Mangeruca

United Technologies Research Center

Cong Liu

UTC Aerospace Systems

Christos Sofronis

United Technologies Research Center

Printer friendly Cite/link Email Feedback | |

Author: | Ferrante, Orlando; Scholte, Eelco; Pinello, Claudio; Ferrari, Alberto; Mangeruca, Leonardo; Liu, Con |
---|---|

Publication: | SAE International Journal of Aerospace |

Article Type: | Report |

Date: | Sep 1, 2016 |

Words: | 6598 |

Previous Article: | Communication Infrastructure for Hybrid Test Systems - Demands, Options, and Current Discussions. |

Next Article: | Minimizing Aircraft ECS Bleed Off-Take - Virtual Integrated Aircraft Applications. |

Topics: |