Industry Day is dedicated to sharing experience with using formal methods in industrial environments.
Thursday, August 30th09:00-10:00: Invited talk by Asaf Degani
Formal Methods in the Wild: Trains, Planes, & Automobiles
10:00: Coffee break
10:30-12:30:
Jean-Raymond Abrial, Marseille, France12:30 Lunch
Formalizing hybrid systems with Event-B
Abstract:
In this presentation, we explain how the development of hybrid systems (with discrete as well as continuous transitions) can be done in Event-B and the Rodin Platform. It follows the seminal approach introduced at the turn of the century in Action Systems. Many examples illustrate our approach.
Click to download
Michael Leuschel, Formal Mind, Germany
ProB, ProR and Data Validation with B
Abstract:
We present details about using ProB to validate various aspects of formal railway models. Notably, we describe recent improvements to be able to deal with large sets and relations, as well as various other improvements related to inspecting the truth value of complicated formulas, in order to be used within a SIL-4 development process.
Click to download
14:00-16:00:
Yannick Moy, AdaCore, France16:00: Coffee break
The future of formal software verification in avionics
Abstract:
Avionics software is submitted to a strict certification process (DO-178), that has been quite successful to date: no plane has ever been reported as crashing due to software errors. Until now, this process has been heavily based on testing. The inherent impossibility of doing exhaustive testing led to the definition of coverage criteria, such as MC/DC, to define a limit to testing. Reaching these coverage criteria requires writing a large number of tests manually, which contributes to the very high (and increasing) cost of verification. The avionics industry has recognized this problem, which led to a new version of the certification standard issued in 2011 called DO-178C. This new standard explicitly authorizes the use of formal methods instead of testing to address many verification objectives.
We propose a methodology and tools based on formal methods to address the DO-178C objective of verifying that code correctly implements low-level requirements. Our methodology builds on the years of accumulated experience in applying formal verification based on subprogram contracts in an industrial setting, with the Caveat tool from CEA at Airbus and the SPARK toolset developed between Altran Praxis and AdaCore. Our approach simplifies the adoption of formal verification by using the executable semantics of assertions familiar to engineers, and relying on a combination of automatic proofs and testing instead of manual work by local formal methods experts. We take advantage of the latest version (2012) of the Ada language, which includes many specification features like pre- and post-conditions for subprograms. Static and dynamic verification tools share a common backbone provided by the GNAT compiler, and the proof technology is based on the Why3 and Alt-Ergo tools from INRIA. We will present the current state of the technology developed in the project Hi-Lite, and early experiments on industrial case studies.
Click to download
Viet Yen Nguyen, RWTH Aachen University/ESA, The Netherlands
Formal Modelling & Analysis of an European Satellite
Abstract:
We report on our experience of applying a formal modeling and analysis toolset on one of the satellites under development at the European Space Agency. The satellite's nominal and erroneous behavior was captured using an AADL-like modeling language called SLIM. It includes its discrete, real-time, probabilistic and hybrid behavioral aspects. The nominal state space comprises nearly 50 million states, which multiplies manifold upon the injection of failures. Using the COMPASS toolset developed earlier for the European Space Agency, we automatically derived verification and validation artifacts using (probabilistic) model checking techniques. These artifacts, such as functional verification proofs, fault trees, FMEA tables and probabilistic risk assessments, are typically constructed manually in a space system engineering process. The model's size pushed the computational tractability of the underlying verification algorithms and revealed bottlenecks for future theoretical research. Additionally, as the case study was conducted in parallel with the conventional development of the satellite, we improved our understanding (and issues) of applying formal methods to benefit the space systems engineering process.
Marcel Verhoef, Chess, The Netherlands
Embedding Formal Techniques into Industrial Product Development - Experiences with the DESTECS Approach
Abstract:
Productivity in development of distributed embedded real-time control systems is hampered by the fact that the engineering disciplines involved use distinct methods and techniques that lack a common basis. The impact of early, discipline specific, design choices on the system level requirements is therefore hard -if not impossible- to assess and typically postponed to the integration and test phase. Design errors discovered late in the development life cycle are notoriously expensive to fix, in particularly so for so-called cross-cutting concerns, such as dependability and performance. The DESTECS approach combines established formal techniques to rigorously support discipline specific development, whereby co-simulation is used to assess the cross-discipline impact of integrated early design models. We show, by means of several large scale industrial case studies, that this approach has a significant and positive effect on the designers' ability to evaluate for example fault-resilience.
Click to download
16:30-18:00:
Alessandro Fantechi, Università di Firenze, Italy21:00: Conference Dinner
Trends in formal verification in the railway signalling domain
Abstract:
Railway signaling has been a traditional subject of early application of formal methods in the development and verification of computerized equipment. This talk will attempt to give an up-to-date survey of the current challenges brought by the increasingly complex applications of this domain to formal verification capabilities. Such application will be categorized in two main areas, and the current industrial applicability of formal verification techniques and tools to representatives of the two classes will be discussed.
Weiqiang Kong, Kyushu University, Japan
Garakabu2: formal verification for ZIPC
Abstract:
ZIPC is a table-based modeling method which is widely used in embedded industry. ZIPC describes system behavior by multiple tables. In each table, a column represents a possible state of the system, a raw represents a possible event which would occur in the system, and a cell represents a possible action which takes place. Then, ZIPC can run the simulation and compile the design into C/C++ skeleton. Unfortunately, up to now there is no tool which formally verifies ZIPC models. To fill this gap, Garakabu2 is developed. Garakabu2 is a dedicated model checker for ZIPC. Internally, Garakabu2 converts ZIPC models into formulas of a decidable theory, and checks their satisfiablity by SMT solver such as CVC 3. If a counterexample is found, Garakabu2 can launch ZIPC and show the simulation along the counterexample. Garakabu2 is now commercialize and distributed by CATS, the same company which develops ZIPC. In this talk, we introduce ZIPC and Garakabu2. We also discuss the efforts to improve Garakabu2 further. Finally, we give a demo.
Click to download
Marc Antoni, SNCF, France
Practical formal validation method for interlocking systems
Abstract:
Today, a main question is to answer to the following problematic: have we recognized that for software, the delivery of absolute numerical safety targets is considered to be impossible, and the methods contained in the CENELEC standard produce a probability that certain (unsafe) failure rates will be archived rather than an absolute assurance We know that checks before putting safety signaling facilities into service as well as the results of tests are essential but time consuming without guaranty of exhaustiveness in particular for the case of computerized equipment. In the context of greater economic constraints and increasing complexity of computerized tools, the capacities of the classic approval process are today attained. We see in actual practice a reduction of the validation cover rate and more and more numerous unsafe failures as results. This paper assumes that it is possible in practice to give an exhaustive formal proof that the functional of the signaling application (functional white box) is safe in the context of use (over-system). The presented method makes it possible, after a rigorous and cost effective design, to validate formally the functional software of critical computerized systems. The aim of our project was to provide the SNCF (today for delegated infrastructure manager, and tomorrow for rolling stock departments of railway undertaker) with an operating method for the formal validation of critical computerized systems, especially for the Interlocking and ETCS/ERTMS systems. A formal proof method by assertion, applicable to these critical systems, which covers equally the specification and its real software implementation, is presented in this paper. With the proposed method and its associated tools we completely verify that the system follows all safety properties at all time and does not show superfluous conditions: it replaces the platform checks and is in accordance with the existing SNCF testing procedures. The advantages are a significant reduction of testing time and of the related costs, an increase of the tests cover rate (deterministic safety vs. probabilistic safety), The paper assumes that the formal methods mastery by infrastructure engineers is a main key to prove that, during the life of the system, more safety is not more expensive.
Click to download
