This paper examines the verification of stability, a control requirement, over discrete control systems represented as Simulink diagrams, using different model checking approaches and tools. Model checking comprises the (exhaustive) exploration of a model of a system, to determine if a requirement is satisfied. If that is not the case, examples of the requirement's violation within the system's model are provided, as witnesses. These examples are potentially complementary to previous work on automatic theorem proving, when a system is not proven to be stable, but no proof of instability can be provided. We experimentally evaluated the suitability of four model checking approaches to verify stability on a set of benchmarks including linear and nonlinear, controlled and uncontrolled, discrete systems, via Lyapunov's second method or Lyapunov's direct method. Our study included symbolic, bounded, statistical and hybrid model checking, through the open-source tools NuSMV, UCLID, S-TaLiRo and SpaceEx, respectively. Our experiments and results provide an insight on the strengths and limitations of these model checking approaches for the verification of control requirements for discrete systems at Simulink level. We found that statistical model checking with S-TaLiRo is the most suitable option to complement our previous work on automatic theorem proving.
The absence of runtime errors (or low-level requirements) such as overflows or arrays out of bounds for fixed data widths, was verified in @cite_7 using model checking for Simulink diagrams. Other tools, such as Mathwork's Polyspace, translate the Simulink diagrams into code before checking for runtime errors. Higher-level requirements in terms of safety and liveness have been verified directly in the Simulink models (e.g., the Prover Plug-In or CheckMate for hybrid systems @cite_13 ), after translating the models (or parts of them) into the language of a specific model checker @cite_17 @cite_19 , or after translating the Simulink diagrams into code @cite_18 @cite_20 . Since model checking is based on the exploration of finite-state decidable models, which implies discretization and abstraction processes over the original systems, formalized translation'' processes are highly desirable. We explored available translation semantics from Simulink to NuSMV @cite_8 and to UCLID @cite_7 .
@cite_18 @cite_7 @cite_8 @cite_19 @cite_13 @cite_20 @cite_17
176400115 2105300531 2171520043 589665961 2131441094 2315317710 2401986398
Embedded systems have become an inevitable part of control systems in many industrial domains including avionics. The nature of this domain traditionally requires the highest possible degree of system availability and integrity. While embedded systems have become extremely complex and they have been continuously replacing legacy mechanical components, the amount of defects of hardware and software has to be kept to absolute minimum to avoid casualties and material damages. Despite the above-mentioned facts, significant improvements are still required in the validation and verification processes accompanying embedded systems development. In this paper we report on integration of a parallel, explicit-state LTL model checker (DiVinE) and a tool for requirements-based verification of aerospace system components (HiLiTE, a tool implemented and used by Honeywell). HiLiTE and the proposed partial toolchain use MATLAB Simulink Stateflow as the primary design language. The work has been conducted within the Artemis project industrial Framework for Embedded Systems Tools (iFEST). Matlab Simulink is widely used for model-based development of embedded systems. In particular, safety-critical applications are increasingly designed in Matlab Simulink. At the same time, formal verification techniques for Matlab Simulink are still rare and existing ones do not scale well. In this paper, we present an automatic transformation from discrete-time Matlab Simulink to the input language of UCLID. UCLID is a toolkit for system verification based on SMT solving. Our approach enables us to use a combination of bounded model checking and inductive invariant checking for the automatic verification of Matlab Simulink models. To demonstrate the practical applicability of our approach, we have successfully verified the absence of one of the most common errors, i. e. variable over- or underflow, for an industrial design from the automotive domain. Model Based Development (MBD) using Mathworks tools like Simulink, Stateflow etc. is being pursued in Honeywell for the development of safety critical avionics software. Formal verification techniques are well-known to identify design errors of safety critical systems reducing development cost and time. As of now, formal verification of Simulink design models is being carried out manually resulting in excessive time consumption during the design phase. We present a tool that automatically translates certain Simulink models into input language of a suitable model checker. Formal verification of safety critical avionics components becomes faster and less error prone with this tool. Support is also provided for reverse translation of traces violating requirements (as given by the model checker) into Simulink notation for playback. In this paper we report on work in progress to extend the QuantUM approach to support the quantitative property analysis of Matlab Simulink Stateflow models. We propose a translation of Simulink Stateflow models to CTMCs which can be analyzed using the PRISM model checker inside the QuantUM tool. We also illustrate how the information needed to perform probabilistic analysis of dependability properties can be specified at the level of the Simulink Stateflow model. We demonstrate the applicability of our approach using a case study taken from the MathWorks examples library. This paper concerns computational methods for verifying properties of polyhedral invariant hybrid automata (PIHA), which are hybrid automata with discrete transitions governed by polyhedral guards. To verify properties of the state trajectories for PIHA, the planar switching surfaces are partitioned to define a finite set of discrete states in an approximate quotient transition system (AQTS). State transitions in the AQTS are determined by the reachable states, or flow pipes, emitting from the switching surfaces according to the continuous dynamics. This paper presents a method for computing polyhedral approximations to flow pipes. It is shown that the flow-pipe approximation error can be made arbitrarily small for general nonlinear dynamics and that the computations can be made more efficient for affine systems. The paper also describes CheckMate, a MATLAB-based tool for modeling, simulating and verifying properties of hybrid systems based on the computational methods previously described. We report the results obtained during the verification of Autosub6000, an autonomous underwater vehicle used for deep oceanic exploration. Our starting point is the Simulink Matlab engineering model of the submarine, which is discretised by a compiler into a representation suitable for model checking. We assess the ability of the vehicle to function under degraded conditions by injecting faults automatically into the discretised model. The resulting system is analysed by means of the model checker MCMAS, and conclusions are drawn on the system's ability to withstand faults and to perform self-diagnosis and recovery. We present lessons learnt from this and suggest a general method for verifying autonomous vehicles.