Skip to main content

Über dieses Buch

This book constitutes the proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011, held in Trento, Italy, in August 2011. The 16 papers presented together with 2 invited talks were carefully reviewed and selected from 39 submissions. The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. It also strives to promote research and development for the improvement of formal methods and tools for industrial applications.



Towards Trustworthy Aerospace Systems: An Experience Report

Building modern aerospace systems is highly demanding. They should be extremely dependable. They must offer service without interruption (i.e., without failure) for a very long time — typically years or decades. Whereas “five nines” dependability, i.e., a 99.999 % availability, is satisfactory for most safety-critical systems, for on-board systems it is not. Faults are costly and may severly damage reputations. Dramatic examples are known. Fatal defects in the control software of the Ariane-5 rocket and the Mars Pathfinder have led to headlines in newspapers all over the world. Rigorous design support and analysis techniques are called for. Bugs must be found as early as possible in the design process while performance and reliability guarantees need to be checked whenever possible. The effect of fault diagnosis, isolation and recovery must be quantifiable
Joost-Pieter Katoen

Satisfiability at Microsoft

Constraint satisfaction problems arise in many diverse areas including software and hardware verification, type inference, static program analysis, test-case generation, scheduling, planning and graph problems. These areas share a common trait, they include a core component using logical formulas for describing states and transformations between them. The most well-known constraint satisfaction problem is propositional satisfiability, SAT, where the goal is to decide whether a formula over Boolean variables, formed using logical connectives can be made true by choosing true/false values for its variables. Some problems are more naturally described using richer languages, such as arithmetic. A supporting theory (of arithmetic) is then required to capture the meaning of these formulas. Solvers for such formulations are commonly called Satisfiability Modulo Theories (SMT) solvers.
Modern software analysis and model-based tools are increasingly complex and multi-faceted software systems. However, at their core is invariably a component using logical formulas for describing states and transformations between system states. In a nutshell, symbolic logic is the calculus of computation. The state-of-the art SMT solver, Z3, developed at Microsoft Research, can be used to check the satisfiability of logical formulas over one or more theories. SMT solvers offer a compelling match for software tools, since several common software constructs map directly into supported theories.
SMT solvers have been the focus of increased recent attention thanks to technological advances and an increasing number of applications. The Z3 solver from Microsoft Research is particularly prolific both concerning applications and technological advances. We describe several of the applications of Z3 within Microsoft, some are included as critical components in tools shipped with Windows 7, others are used internally and yet more are available for academic research. Z3 ranks as the premier SMT solver available today.
Leonardo de Moura

Lightweight Verification of a Multi-Task Threaded Server: A Case Study With The Plural Tool

In this case study, we used the Plural tool to verify the design of a commercial multi-task threaded application (MTTS) implemented by Novabase, which has been used for massively parallelising computational tasks. The effort undertaken in this case study has revealed several issues related with the design of the MTTS, with programming practices used in its implementation, and with domain specific properties of the MTTS. This case study has also provided insight on how the analysis done by the Plural tool can be improved. The Plural tool performs lightweight verification of Java programs. Plural specification language combines typestates and access permissions, backed by Linear Logic. The Plural specifications we wrote for the MTTS are based on its code, its informal documentation, sometimes embedded in the code, and our discussions with Novabase’s engineers, who validated our understanding of the MTTS application.
Néstor Cataño, Ijaz Ahmed

Runtime Verification of Typical Requirements for a Space Critical SoC Platform

SystemC TLM (Transaction Level Modeling) enables the description of complex Systems on Chip (SoC) at a high level of abstraction. It offers a number of advantages regarding architecture exploration, simulation performance, and early software development. The tendency is therefore to use TLM-based descriptions of SoC platforms as golden models that, by essence, must be flawless.
In this paper, a SoC critical embedded platform under development by Astrium is used as proof-of-concept demonstrator, to assess the ISIS prototype tool which is devoted to the verification of SystemC TLM designs. Given temporal properties that capture the intended requirements, ISIS automatically instruments the design with ad hoc checkers that inform about the satisfaction of the properties during simulation.
After a description of the target platform design, we show that the PSL language enables the unambiguous expression of the required properties, and that the checkers produced by ISIS verify their satisfaction with a limited simulation time overhead.
Luca Ferro, Laurence Pierre, Zeineb Bel Hadj Amor, Jérôme Lachaize, Vincent Lefftz

Past Time LTL Runtime Verification for Microcontroller Binary Code

This paper presents a method for runtime verification of microcontroller binary code based on past time linear temporal logic (ptLTL). We show how to implement a framework that, owing to a dedicated hardware unit, does not require code instrumentation, thus, allowing the program under scrutiny to remain unchanged. Furthermore, we demonstrate techniques for synthesizing the hardware and software units required to monitor the validity of ptLTL specifications.
Thomas Reinbacher, Jörg Brauer, Martin Horauer, Andreas Steininger, Stefan Kowalewski

A SAT-Based Approach for the Construction of Reusable Control System Components

This paper shows how to take advantage of a SAT-solving approach in the development of safety control software systems for manufacturing plants. In particular, it demonstrates how to construct reusable components which are assembled after instantiation to derive controllers of modular production systems. An experiment has been conducted with Alloy not only to verify properties required by a control theory for complex systems organized hierarchically, but also to synthesize two major parts of a component: observer and supervisor. The former defines its interface while guaranteeing nonblocking hierarchical control. The latter ensures the satisfaction of constraints imposed on its behavior and on the interactions among its subcomponents during system operation. As long as the size of component interfaces is small, SAT-solvers appear useful to build correct reusable components because the formal models that engineers manipulate and analyze are very close to the abstract models of the mathematical theory.
Daniel Côté, Benoît Fraikin, Marc Frappier, Richard St-Denis

Formal Safety Analysis in Industrial Practice

We report on a comparative study on formal verification of two level crossing controllers that were developed using Scade by a rail automation manufacturer. Deductive Cause-Consequence Analysis of Ortmeier et al. is applied for formal safety analysis and in addition, safety requirements are proven. Even with these medium size industrial case studies we observed intense complexity problems that could not be overcome by employing different heuristics like abstraction and compositional verification. In particular, we failed to prove a crucial liveness property within the Scade framework stating that an unsafe state will not be persistent. We finally succeeded to prove this property by combining abstraction and model transformation from Scade to UPPAAL timed automata. In addition, we found that the modeling style has a significant impact on the complexity of the verification task.
Ilyas Daskaya, Michaela Huhn, Stefan Milius

Structural Test Coverage Criteria for Integration Testing of LUSTRE/SCADE Programs

Lustre is a formal synchronous declarative language widely used for modeling and specifying safety-critical applications in the fields of avionics, transportation, and energy production. In such applications, the testing activity to ensure correctness of the system plays a crucial role in the development process. To enable adequacy measurement of test cases over applications specified in Lustre (or SCADE), a hierarchy of structural coverage criteria for Lustre programs has been recently defined. A drawback with the current definition of the criteria is that they can only be applied for unit testing, i.e., to single modules without calls to other modules. The criteria experiences scalability issues when used over large systems with several modules and calls between modules. We propose an extension to the criteria definition to address this scalability issue. We formally define the extension by introducing an operator to abstract calls to other modules. This extension allows coverage metrics to be applied to industrial-sized software without an exponential blowup in the number of activation conditions. We conduct a preliminary evaluation of the extended criteria using an Alarm Management System.
Virginia Papailiopoulou, Ajitha Rajan, Ioannis Parissis

Formal Analysis of a Triplex Sensor Voter in an Industrial Context

For several years, Rockwell Collins has been developing and using a verification framework for MATLAB Simulink© and SCADE SuiteTMmodels that can generate input for different proof engines. Recently, we have used this framework to analyze aerospace domain models containing arithmetic computations. In particular, we investigated the properties of a triplex sensor voter, which is a redundancy management unit implemented using linear arithmetic operations as well as conditional expressions (such as saturation). The objective of this analysis was to analyze functional and non-functional properties, but also to parameterize certain parts of the model based on the analysis results of other parts. In this article, we focus on results about the reachable state space of the voter, which prove the bounded-input bounded-output stability of the system, and the absence of arithmetic overflows. We also consider implementations using floating point arithmetic.
Michael Dierkes

Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost.

We report on the actual industrial use of formal methods during the development of a software bus. At Neopost Inc., we developed the server component of a software bus, called the XBus, using formal methods during the design, validation and testing phase: We modeled our design of the XBus in the process algebra mCRL2, validated the design using the mCRL2-simulator, and fully automatically tested our implementation with the model-based test tool JTorX. This resulted in a well-tested software bus with a maintainable architecture. Writing the model, simulating it, and testing the implementation with JTorX only took 17% of the total development time. Moreover, the errors found with model-based testing would have been hard to find with conventional test methods. Thus, we show that formal engineering can be feasible, beneficial and cost-effective.
Marten Sijtema, Mariëlle I. A. Stoelinga, Axel Belinfante, Lawrence Marinelli

Symbolic Power Analysis of Cell Libraries

Cell libraries are collections of logic cores (cells) used to construct larger chip designs; hence, any reduction in their power consumption may have a major impact in the power consumption of larger designs. The power consumption of a cell is often determined by triggering it with all possible input values in all possible orders at each state. In this paper, we first present a technique to measure the power consumption of a cell more efficiently by reducing the number of input orders that have to be checked. This is based on symbolic techniques and analyzes the number of (weighted) wire chargings taking place. Additionally, we present a technique that computes for a cell all orders that lead to the same state, but differ in their power consumption. Such an analysis is used to select the orders that minimize the required power, without affecting functionality, by inserting sufficient delays. Both techniques have been evaluated on an industrial cell library and were able to efficiently reduce the number of orders needed for power characterization and to efficiently compute orders that consume less power for a given state and input-vector transition.
Matthias Raffelsieper, MohammadReza Mousavi

An Automated Semantic-Based Approach for Creating Tasks from Matlab Simulink Models

The approach proposed in this paper forms the front-end of a framework for the complete design flow from specification models of new automotive functions captured in Matlab Simulink to their distributed execution on hierarchical bus-based electronic architectures hosting the release of already deployed automotive functions. The process starts by deriving a task structure from a given Matlab Simulink model. Because the obtained network is typically unbalanced in the sense of computational node weights, nodes are melted following an optimization metric called cohesion where nodes are attracted by high communication density and repelled by high node weights. This reduces task-switching times by avoiding too lightweight tasks and relieves the bus by keeping inter-task communication low. This so-called Task Creation encloses the translation of the synchronous block diagram model of Simulink into a message-based task network formalism that serves as semantic base.
Matthias Büker, Werner Damm, Günter Ehmen, Ingo Stierand

Performability Measure Specification: Combining CSRL and MSL

An integral part of the performance modeling process is the specification of the performability measures of interest. The notations proposed for this purpose can be grouped into classes that differ from each other in their expressiveness and usability. Two representative notations are the continuous stochastic reward logic CSRL and the measure specification language MSL. The former is a stochastic temporal logic formulating quantitative properties about states and paths, while the latter is a component-oriented specification language relying on a first-order logic for defining reward-based measures. In this paper, we combine CSRL and MSL in order to take advantage of the expressiveness of the former and the usability of the latter. To this aim, we develop a unified notation in which the core logic of MSL is employed to set up the reward structures needed in CSRL, whereas the measure definition mechanism of MSL is exploited to formalize measure and property specification patterns in a component-oriented fashion.
Alessandro Aldini, Marco Bernardo, Jeremy Sproston

Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit Using CADP

The complexity of multiprocessor architectures for mobile multi-media applications renders their validation challenging. In addition, to provide the necessary flexibility, a part of the functionality is realized by software. Thus, a formal model has to take into account both hardware and software. In this paper we report on the use of LOTOS NT and CADP for the formal modeling and analysis of the DTD (Dynamic Task Dispatcher), a complex hardware block of an industrial hardware architecture developed by STMicroelectronics. Using LOTOS NT facilitated exploration of alternative design choices and increased the confidence in the DTD, by, on the one hand, automatic analysis of formal models easily understood by the architect of the DTD, and, on the other hand, co-simulation of the formal model with the implementation used for synthesis.
Etienne Lantreibecq, Wendelin Serwe

Transforming SOS Specifications to Linear Processes

This paper describes an approach to transform Structural Operational Semantics, given as a set of deduction rules, to a Linear Process Specification. The transformation is provided for deduction rules in De Simone format, including predicates. The Linear Process Specifications are specified in the syntax of the mCRL2 language, that, with help of the underlying (higher-order) re-writer/tool-set, can be used for simulation, labeled transition system generation and verification of behavioral properties. We illustrate the technique by showing the effect of the transformation from the Structural Operational Semantics specification of a simple process algebra to a Linear Process Specification.
Frank P. M. Stappers, Michel A. Reniers, Sven Weber

Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study

We describe a collaborative effort in which the HOL4 theorem prover is being used to formally verify properties of a structure within the Large Hadron Collider (LHC) machine protection system at the European Organization for Nuclear Research (CERN). This structure, known as Successive Running Sums (SRS), generates the primary input to the decision logic that must initiate a critical action by the LHC machine protection system in response to the detection of a dangerous level of beam particle loss. The use of mechanized logical deduction complements an intensive study of the SRS structure using simulation. We are especially interested in using logical deduction to obtain a generic result that will be applicable to variants of the SRS structure. This collaborative effort has individuals with diverse backgrounds ranging from theoretical physics to system safety. The use of a formal method has compelled the stakeholders to clarify intricate details of the SRS structure and behaviour.
Naghmeh Ghafari, Ramana Kumar, Jeff Joyce, Bernd Dehning, Christos Zamantzas

Hierarchical Modeling and Formal Verification. An Industrial Case Study Using Reo and Vereofy

In traditional approaches to software development, modeling precedes programming activities. Hence, models represent the intended structure and behavior of the system-to-be. The reverse case, however, is often found in practice: using models to gain insight into an existing software system, enabling the evolution and refactoring of the system to new needs. We report on a case study with the ASK communication platform, an existing distributed software system with multithreaded components. For the modeling of the ASK system we followed a hierarchical top-down approach that allows a high-level description of the system behavior on different levels of abstraction by applying an iterative refinement procedure. The system model is refined by decomposing the components into sub-components together with the “glue code” that orchestrates their interactions. Our model of the ASK system is based on the exogenous coordination language Reo for specifying the glue code and an automata-based formalism for specifying the component interfaces. This approach is supported by the modeling framework of the tool-set Vereofy which is used to establish several properties of the components and the coordination mechanism of the ASK system. Besides demonstrating how modeling and verification can be used in combination to gain insight into legacy software, this case study also illustrates the applicability of exogenous coordination languages such as Reo for modeling and tool-sets such as Vereofy for the formal analysis of industrial systems.
Joachim Klein, Sascha Klüppelholz, Andries Stam, Christel Baier

Modeling and Verifying Timed Compensable Workflows and an Application to Health Care

Over the years, researchers have investigated how to provide better support for hospital administration, therapy and laboratory workflows. Among these efforts, as with any other safety critical system, reliability of the workflows is a key issue. In this paper, we provide a method to enhance the reliability of real world workflows by incorporating timed compensable tasks into the workflows, and by using formal verification methods (e.g., model checking). We extend our previous work [1] with the notion of time by providing the formal semantics of Timed Compensable WorkFlow nets (CWF T -nets). We extend the graphical modeling language of Nova WorkFlow (a workflow management system currently under development) to model CWF T -nets and enhance Nova WorkFlow’s automatic translator to translate a CWF T -net into DVE, the modeling language of the distributed LTL model checker DiVinE. These enhancements provide a method for rapid (re)design and verification of timed compensable workflows. We present a real world case study for Seniors’ Care, developed through collaboration with the local health authority.
Ahmed Shah Mashiyat, Fazle Rabbi, Wendy MacCaull


Weitere Informationen

Premium Partner