Skip to main content

Über dieses Buch

This book constitutes the proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015, Oslo, Norway, in June 2015.

The 12 papers presented in this volume were carefully reviewed and selected from 20 submissions. They are organized in topical sections: applications; protocols; specification and analysis; verification.



Formal Verification of Industrial Critical Software

In this paper, the challenges for using formal verification based on automatic tools, like model-checkers, in the industrial development process of safety critical systems is discussed. This usage must be integrated into an appropriate process and must allow for independent result-checking.
Our approach is illustrated with a case study from the openETCS ITEA2 research project using the Systerel Smart Solver S3, a modern SAT-based model-checker for equivalence checking and safety properties analysis of SCADE, C or Ada programs.
Marielle Petit-Doche, Nicolas Breton, Roméo Courbis, Yoann Fonteneau, Matthias Güdemann



A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C

Cloud hypervisors are critical software whose formal verification can increase our confidence in the reliability and security of the cloud. This work presents a case study on formal verification of the virtual memory system of the cloud hypervisor Anaxagoros, a microkernel designed for resource isolation and protection. The code under verification is specified and proven in the frama-C software verification framework, mostly using automatic theorem proving. The remaining properties are interactively proven with the Coq proof assistant. We describe in detail selected aspects of the case study, including parallel execution and counting references to pages, and discuss some lessons learned, benefits and limitations of our approach.
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéeric Loulergue

Intra-procedural Optimization of the Numerical Accuracy of Programs

Numerical programs performing floating-point computations are very sensitive to the way formulas are written. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their accuracy and, in this article, we go one step further by automatically transforming larger pieces of code containing assignments and control structures. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve the numerical accuracy of the target variable. We use abstract interpretation-based static analysis techniques to over-approximate the roundoff errors in programs and during the transformation of expressions. A prototype has been implemented and experimental results are presented concerning classical numerical algorithm analysis and algorithm for embedded systems.
Nasrine Damouche, Matthieu Martel, Alexandre Chapoutot

Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools

Many safety-concerned standards and regulations for real-time embedded systems, e.g., ISO 26262 for automotive electric/electronic systems, recommends the use of formal techniques to achieve the required safety level. This paper presents a method for formal analysis of real-time embedded systems. The method allows properties to be statistically checked early and quickly with high confidence, and may also produce a formal proof when required. This environment exploits uppaal tools consisting of a symbolic model checker (uppaal MC) and a statistical model checker (uppaal smc), and a model-based testing environment (uppaal Yggdrasil), all of which are based on a formal model in timed automata. We demonstrate our method on an industrial case, an automotive Turn Indicator System, showing how the design of the system at the early phase of system development may be efficiently checked against the defined system requirements.
Jin Hyun Kim, Kim G. Larsen, Brian Nielsen, Marius Mikučionis, Petur Olsen

Successful Use of Incremental BMC in the Automotive Industry

Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and automated test case generation are some of the most common applications of automated verification tools based on Bounded Model Checking (BMC). Existing industrial tools for embedded software use an off-the-shelf Bounded Model Checker and apply it iteratively to verify the program with an increasing number of unwindings. This approach unnecessarily wastes time repeating work that has already been done and fails to exploit the power of incremental SAT solving. This paper reports on the extension of the software model checker Cbmc to support incremental BMC and its successful integration with the industrial embedded software verification tool BTC EmbeddedTester. We present an extensive evaluation over large industrial embedded programs, mainly from automotive industry. We show that incremental BMC cuts runtimes by one order of magnitude in comparison to the standard non-incremental approach, enabling the application of formal verification to large and complex embedded software.
Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller



Colored Petri Net Modeling of the Publish/Subscribe Paradigm in the Context of Web Services Resources

In this paper a Prioritized-Timed Colored Petri Net model for the Publish/Subscribe paradigm in the context of Web services distributed resources is considered. We present a generic CPN model for publishing and managing WS-resources, which includes operations for clients to subscribe to these resources, with the intention of being notified when the resource property values fulfill certain conditions. We use CPN Tools to check and validate the model, and a case study is presented to illustrate how this CPN model works.
Valentin Valero, Hermenegilda Macià, Gregorio Díaz, M. Emilia Cambronero

Model Checking a Server-Side Micro Payment Protocol

Many virtual payment systems are available on the world wide web for micropayment, and as they deal with money, correctness is important. One such payment system is Netpay. This paper examines the server-side version of the Netpay protocol and provides its formalization as a CSP model. The PAT model checker is used to prove three properties essential for correctness: impossibility of double spending, validity of an ecoin during the execution and the absence of deadlock. We prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative. This is a very strong assumption for system built to prevent abuse, but further analysis suggests that without it the protocol does no longer guarantee all correctness properties.
Kaylash Chaudhary, Ansgar Fehnker

Specification and Analysis


Require, Test and Trace IT

We propose a framework for requirement-driven test generation that combines contract-based interface theories with model-based testing. We design a specification language, requirement interfaces, for formalizing different views (aspects) of synchronous data-flow systems from informal requirements. Multiple views of a system, modeled as requirement interfaces, are naturally combined by conjunction.
We develop an incremental test generation procedure with several advantages. The test generation is driven by a single requirement interface at a time. It follows that each test assesses a specific aspect or feature of the system, specified by its associated requirement interface. Since we do not explicitly compute the conjunction of all requirement interfaces of the system, we avoid state space explosion while generating tests. However, we incrementally complete a test for a specific feature with the constraints defined by other requirement interfaces. This allows catching violations of any other requirement during test execution, and not only of the one used to generate the test. Finally, this framework defines a natural association between informal requirements, their formal specifications and the generated tests, thus facilitating traceability. We implemented a prototype test generation tool and we demonstrate its applicability on an industrial use case.
Bernhard K. Aichernig, Klaus Hörmaier, Florian Lorber, Dejan Ničković, Stefan Tiran

Applying Finite State Process Algebra to Formally Specify a Computational Model of Security Requirements in the Key2phone-Mobile Access Solution

Key2phone is a mobile access solution which turns mobile phone into a key for electronic locks, doors and gates. In this paper, we elicit and analyse the essential and necessary safety and security requirements that need to be considered for the Key2phone interaction system. The paper elaborates on suggestions/solutions for the realisation of safety and security concerns considering the Internet of Things (IoT) infrastructure. The authors structure these requirements and illustrate particular computational solutions by deploying the Labelled Transition System Analyser (LTSA), a modelling tool that supports a process algebra notation called Finite State Process (FSP). While determining an integrated solution for this research study, the authors point to key quality factors for successful system functionality.
Sunil Chaudhary, Linfeng Li, Eleni Berki, Marko Helenius, Juha Kela, Markku Turunen

Timed Mobility and Timed Communication for Critical Systems

We present a simple but elegant prototyping language for describing real-time systems including specific features as timeouts, explicit locations, timed migration and timed communication. The parallel execution of a step is provided by multiset labelled transitions. In order to illustrate its features, we describe a railway control system. Moreover, we define some behavioural equivalences matching multisets of actions that could happen in a given range of time (up to a timeout). We define the strong time-bounded bisimulation and the strong open time-bounded bisimulation, and prove that the latter one is a congruence. By using various bisimulations over the behaviours of real-time systems, we can check which behaviours are closer to an optimal and safe behaviour.
Bogdan Aman, Gabriel Ciobanu

On the Formal Analysis of Photonic Signal Processing Systems

Photonic signal processing is an emerging area of research, which provides unique prospects to build high-speed communication systems. Recent advancements in fabrication technology allow on-chip manufacturing of signal processing devices. This fact has lead to the widespread use of photonics in industrial critical applications such as telecommunication, biophotonics and aerospace. One the most challenging aspects in the photonics industry is the accurate modeling and analysis of photonic devices due to the complex nature of light and optical components. In this paper, we propose to use higher-order-logic theorem proving to improve the analysis accuracy by overcoming the known limitations of incompleteness and soundness of existing approaches (e.g., paper-and-pencil based proofs and simulation). In particular, we formalize the notion of transfer function using the signal-flow-graph theory which is the most fundamental step to model photonic circuits. Consequently, we formalize and verify the important properties of the stability and the resonance of photonic systems. In order to demonstrate the effectiveness of the proposed infrastructure, we present the formal analysis of a widely used double-coupler double-ring (DCDR) photonic processor.
Umair Siddique, Sidi Mohamed Beillahi, Sofiène Tahar



Automated Verification of Nested DFS

In this paper we demonstrate the automated verification of the Nested Depth-First Search (NDFS) algorithm for detecting accepting cycles. The starting point is a recursive formulation of the NDFS algorithm. We use Dafny to annotate the algorithm with invariants and a global specification. The global specification requires that NDFS indeed solves the accepting cycle problem. The invariants are proved automatically by the SMT solver Z3 underlying Dafny. The global specifications, however, need some inductive reasoning on paths in a graph. To prove these properties, some auxiliary lemmas had to be provided. The full specification is contained in this paper. It fits on 4 pages, is verified by Dafny in about 2 minutes, and was developed in a couple of weeks.
Jaco C. van de Pol

On the Formal Verification of Optical Quantum Gates in HOL

Quantum computers are expected to handle hard computational problems and provide unbreakable security protocols. Among different quantum computer implementations, those based on quantum optics and nuclear magnetic resonance show good advancement in building large scale machines. However, the involvement of optical and nuclear techniques makes their development very critical. This motivates us to apply formal techniques, in particular theorem proving, in quantum circuits analysis. In this work, we present the formalization of multi-inputs/multi-outputs quantum gates (technically called multi-modes optical circuits). This requires the implementation of tensor product over complex-valued functions. Firstly, we build a formal model of single optical beams and then extend it to cover circuits of multi optical beams, with the help of the developed tensor product algebra. As an application, we formally verify the behavior of the optical quantum CNOT gate and Mach-Zehnder interferometer.
Mohamed Yousri Mahmoud, Prakash Panangaden, Sofiène Tahar


Weitere Informationen

Premium Partner