FMICS 2008

Keywords: explicit model checking, evaluation, review, experience report, state space explosion
Abstract:
In order to apply formal methods in practice, the practitioner has to comprehend a vast amount of research literature and realistically evaluate practical merits of different approaches. In this paper we focus on explicit finite state model checking and study this area from practitioner's point of view. We provide a systematic overview of techniques for fighting state space explosion and we analyse trends in the research. We also report on our own experience with practical performance of techniques. Our main conclusion and recommendation for practitioner is the following: be critical to claims of dramatic improvement brought by a single sophisticated technique, rather use many different simple techniques and combine them.

Keywords: program analysis, Datalog, boolean equation system, demand-driven evaluation
Abstract:
This paper describes a powerful, fully automated method to evaluate Datalog queries by using Boolean Equation Systems (BESs), and its application to object-oriented program analysis. Datalog is used as a specification language for expressing complex interprocedural program analyses involving dynamically created objects. In our methodology, Datalog rules encoding a particular analysis, together with a set of constraints (Datalog facts that are automatically extracted from program source code), are dynamically transformed into a BES, whose local resolution corresponds to the demand-driven evaluation of the program analysis. This approach allows us to reuse existing general purpose verification toolboxes, such as CADP, providing local BES resolutions with linear-time complexity. Our evaluation technique has been implemented and successfully tested on several JAVA programs and DATALOG analyses that demonstrate the feasibility of our approach.

Keywords: model-driven development, SCADE, rail automation
Abstract:
In this paper we report about an ongoing pilot project for the model-driven devel-opment of safety-relevant software at Siemens Mobility in the Rail Automation section. In our project models are used to describe the functionality of software as well as for verification. An important focus in the pilot lies on SCADE Version 6, a tool for the model- driven development of safety-relevant software, developed by Esterel Technologies. We briefly describe the most important features of SCADE and discuss the lessons learned during our pilot.

Keywords: Synchronous software, testing, structural coverage, data-flow language, LUSTRE, multi-clock operators
Abstract:
LUSTRE is a formal synchronous declarative language widely used for modeling and specifying safety-critical applications in the fields of avionics, transportation or energy production. Testing this kind of applications is an important and demanding task during the development process. It mainly consists in generating test data and measuring the achieved coverage. An hierarchy of structural coverage criteria for LUSTRE programs have been recently defined to assess the thoroughness of a given test set. They are based on the operator network, which is the graphical representation of a LUSTRE program and depicts the way that input flows are transformed into output flows through their propagation along the program paths. The above criteria definition aimed at demonstrating the opportunity of such a coverage assessment approach but doesn't deal with all the language constructions. In particular, the use of multiple clocks has not been taken into account. In this paper, we extend the criteria to programs that use multiple clocks. Such an extension allows for the application of the existing coverage metrics to industrial software components, which usually operate on multiple clocks, without negatively affecting the complexity of the criteria.

Keywords: test oracle, automation, formal methods, avionics
Abstract:
This paper presents an approach and an associated tool that have been proposed to automate the test oracle procedure of critical systems developed at Airbus. The target tests concern the early validation of the SCADE design and are performed in a simulated environment. The proposed approach and tool have been successfully applied to several Airbus examples.

Keywords: probabilistic systems, model checking, LTL, quantitative analysis, linear programming
Abstract:
Quantitative analysis of probabilistic systems has been studied mainly from the global model-checking point of view. In the global model-checking, the goal of verification is to decide the probability of satisfaction of a given property for all reachable states in the state space of the system under investigation. On the other hand, in local model checking approach the probability of satisfaction is computed only for the set of initial states. In theory, it is possible to solve the local model checking problem using the global model checking approach. However, the global model checking procedure can be significantly outperformed by a dedicated local model-checking one. In this paper we present several particular techniques that if applied to global model checking procedure reduce the runtime needed for a local model checking procedure from days to minutes.

Keywords: State Space Exploration, Matlab Simulink, SPIN, Automotive Software
Abstract:
An increasing number of industrial strength software design tools come along with verification tools that offer some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in state space exploration tool or a general purpose model checking tool arises quite naturally. Using the case study of an AUTOSAR compliant memory management module we compare the Simulink Design Verifier and the SPIN model checking tool in terms of their suitability to verify important correctness properties of this module. The comparison is both functional in that it analyzes the suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools.

Keywords: runtime verification, context-based real-time properties, LARVA, Dynamic Automata with Events and Timers
Abstract:
Given the intractability of exhaustively verifying software, the use of runtime-verification, to verify single execution paths at runtime, is becoming popular. Although the use of runtime verification is increasing in industrial settings, various challenges still are to be faced to enable it to spread further. We present dynamic communicating automata with timers and events to describe properties of systems, implemented in LARVA, an event-based runtime verification tool for monitoring temporal and contextual properties of Java programs. The combination of timers with dynamic automata enables the straightforward expression of various properties, including replication of properties, as illustrated in the use of LARVA for the runtime monitoring of a real life case study --- an online transaction system for credit card. The features of LARVA are also benchmarked and compared to a number of other runtime verification tools, to assess their respective strengths in property expressivity and overheads induced through monitoring.

Keywords: requirements formalization and validation, complex natural language specification, UML, temporal logic, symbolic model checking
Abstract:
Flaws in requirements may have severe impacts on the subsequent phases of the development flow. However, an effective validation of requirements can be considered a largely open problem. In this paper, we propose a new methodology for requirements validation, based on the use of formal methods. The methodology consists of three main phases: first, an informal analysis is carried out, resulting in a structured version of the requirements, where each fragment is classified according to a fixed taxonomy. In the second phase, each fragment is then mapped onto a subset of UML, with a precise semantics, and enriched with static and temporal constraints. The third phase consists of the application of specialized formal analysis techniques, optimized to deal with properties (rather than with models).

Keywords: function block, formal analysis, functional specification checking, coloured Petri nets
Abstract:
Nuclear power plants (NPPs) are highly safety-critical and complex systems, where the correct operation of the safety procedures is of great importance. To cope with the complexity and the high interdependence of the digital control systems (DCS) software, the experts who create the functional specification for the DCS favour graphical models such as Function Block Diagrams (FBDs). The FBD based specifications have a clear structure, a semi-formal, well-defined syntax and semantics, and simulation tools that help to test them during development. Once a specification is completed, a certified automatic code generation process creates an executable code that is compliant to the specification. However, the above approach to FBD based development does not guarantee the correctness and safety of the specification itself. Simulation and testing can uncover a lot of errors; but in complex systems it cannot be exhaustive even if a lot of time and effort is put into testing. Therefore formal analysis is required to prove that the system will not enter into unsafe states, remains operational (no deadlock or livelock), does not trigger the safety actions unnecessarily (no spurious activation), but it always triggers them when required (no activation masking). To reach this goal, in our approach the development process is supplemented with a formal model, based on Coloured Petri Nets. The basic function blocks are described with CPN subnets (by reinterpretation), and constitute a library of formal functional models. The complete formal model of a safety function is obtained by the proper composition of the elementary CPN subnets into a hierarchical CPN, using the structural information from the FDB based specification. This formal model is then analysed using the behavioural properties of the CPN, as well as model checking methods. The state space of the CPN model is reduced by lazy state-space generation.

Keywords: Model Checking, Theorem Proving, Deadlock, Readers-Writers, Uppaal, PVS
Abstract:
The classic readers-writers problem has been extensively studied. This holds to a lesser degree for the reentrant version, where it is allowed to nest locking actions. Such nesting is useful when a library is created with various procedures that each start and end with a lock. Allowing nesting makes it possible for these procedures to call each other. We considered an existing widely used industrial implementation of the reentrant readers-writers problem. We modeled it using a model checker revealing a serious error: a possible deadlock situation. The model was improved and checked satisfactorily for a fixed number of processes. To achieve a correctness result for an arbitrary number of processes the model was converted to a theorem prover with which it was proven.

Keywords: formal methods, CSP||B, compositional modelling, specification, verification, case study
Abstract:
This paper presents an experience report on the specification and the validation of a real case study in the context of the industrial CRISTAL project. The case study concerns a platoon of a new type of urban vehicles with new functionalities and services. It is specified using the combination, named CSP$\|$B, of two well-known formal methods, and validated using the corresponding support tools. This large -- both distributed and embedded -- system typically corresponds to a multi-level composition of components that have to cooperate. We identify some lessons learned, showing how to develop and verify the specification and check some properties in a compositional way using theoretical results and support tools to validate this complex system.

Keywords: Model Checking, Process Algebras, Symbolic Method, Partial Order Reduction
Abstract:
Different approaches have been developed to mitigate the state space explosion of model checking techniques. Among them, symbolic verification techniques use efficient representations such as BDDs to reason over sets of states rather than over individual states. Unfortunately, past experience has shown that these techniques do not work well for loosely-synchronized models. This paper presents a new algorithm and a new tool that combine BDD-based model checking with partial order reduction (POR) to allow the verification of models featuring asynchronous processes, with significant performance improvements over currently available tools. We start from the ImProviso algorithm (Lerda et al) for computing reachable states, which combines POR and symbolic verification. We merge it with the FwdUntil method (Iwashita et al) that supports verification of a subset of CTL. Our algorithm has been implemented in a prototype that is applicable to action-based models and logics such as process algebras and ACTL. Experimental results on a model of an industrial application show that our method can verify properties of a large industrial model which cannot be handled by conventional model checkers.

Keywords: LTL, model checking, I/O efficient, flash memory, SSD
Abstract:
As flash media become common and their capacities and speed grow, they are becoming a practical alternative for standard mechanical drives. So far, external memory model checking algorithms have been optimized for mechanical hard disks corresponding to the model of Aggarwal and Vitter. Since flash memories are essentially different, the model of Aggarwal and Vitter no longer describes their typical behavior. On such a different device, algorithms can have different complexity, which may lead to the design of completely new flash-memory-efficient algorithms. We provide a model for computation of I/O complexity on the model of Aggarwal and Vitter modified for flash memories. We discuss verification algorithms optimized for this model and compare the performance of these algorithms with approaches known from I/O-efficient model checking on mechanical hard disks. We also give an answer, when the usage of flash devices pays off and whether their further evolution in speed and capacity could broaden a range, where new algorithms outperform the old ones.

Keywords: function block, formal analysis, functional specification checking, coloured Petri nets
Abstract:
Nuclear power plants (NPPs) are highly safety-critical and complex systems, where the correct operation of the safety procedures is of great importance. To cope with the complexity and the high interdependence of the digital control systems (DCS) software, the experts who create the functional specification for the DCS favour graphical models such as Function Block Diagrams (FBDs). The FBD based specifications have a clear structure, a semi-formal, well-defined syntax and semantics, and simulation tools that help to test them during development. Once a specification is completed, a certified automatic code generation process creates an executable code that is compliant to the specification. However, the above approach to FBD based development does not guarantee the correctness and safety of the specification itself. Simulation and testing can uncover a lot of errors; but in complex systems it cannot be exhaustive even if a lot of time and effort is put into testing. Therefore formal analysis is required to prove that the system will not enter into unsafe states, remains operational (no deadlock or livelock), does not trigger the safety actions unnecessarily (no spurious activation), but it always triggers them when required (no activation masking). To reach this goal, in our approach the development process is supplemented with a formal model, based on Coloured Petri Nets. The basic function blocks are described with CPN subnets (by reinterpretation), and constitute a library of formal functional models. The complete formal model of a safety function is obtained by the proper composition of the elementary CPN subnets into a hierarchical CPN, using the structural information from the FDB based specification. This formal model is then analysed using the behavioural properties of the CPN, as well as model checking methods. The state space of the CPN model is reduced by lazy state-space generation.

Keywords: Proof Carrying Code, Program Non-interference, Rewriting Logic, Abstract Interpretation
Abstract:
In this paper we propose a certification technique for non-interference of Java programs based on rewriting logic, a very general logical and semantic framework efficiently implemented in the high-level programming language Maude. Non–interference is a semantic program property that prevents illicit information flow to happen. Starting from a basic specification of the semantics of Java written in Maude, we develop an information–flow extension of this operational Java semantics which allows us to observe non-interference of Java programs. Then we develop in Maude an abstract, finite-state version of the information-flow operational semantics which supports finite program verification. As a by–product of the verification, a certificate of non-interference is delivered which consists of a set of (abstract) rewriting proofs that can be easily checked by the code consumer using a standard rewriting logic engine.