EASST Award

Following a tradition established over the past few years, the European Association of Software Science and Technology (EASST) offered an award to the best FMICS paper. This year, the award was given to Bárbara Vieira from Universidade do Minho, Braga, Portugal for the paper Verifying Cryptographic Software Correctness With Respect to Reference Implementations, written together with José Bacelar Almeida, Manuel Barbosa and Jorge Sousa Pinto.

The award was presented by María Alpuente, PC co-chair of FMICS 2009, Christophe Joubert, workshop chair of FMICS 2009, and Alessandro Fantechi, FMICS Working Group coordinator since November 2008 (see photo).

Proceedings

Poster Presentations

Program

Monday 2 November

9:00 FMICS 2009 Opening María Alpuente
9:05 Invited Talk (Chair: María Alpuente)
What's in common between Test, Model checking, and Decision Procedures?
Ken McMillan (Cadence, USA)

10:00 - 10:30 Coffee Break

10:30 Session 1 (Chair: Jaco van de Pol)

Towards an industrial use of FLUCTUAT on safety-critical avionics software.
David Delmas, Eric Goubault, Sylvie Putot, Jean Souyris, Karim Tekkal and Franck Védrine.

Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle
Alwyn Goodloe and César Muñoz.

11:30 Poster Session 1 (Chair: Ken McMillan)

Formal Development for Railway Signaling Using Commercial Tools.
Alessio Ferrari, Alessandro Fantechi, Stefano Bacherini and Niccolò Zingoni.

Integrated Formal Approach for Qualified Critical Embedded Code Generator.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux and Olivier Ssi yan kai.

Developing a decision support tool for Dam management with SPIN.
Laura Panizo, Maria del Mar Gallardo, Pedro Merino and Antonio Linares.

12:30 - 14:30 Lunch

14:30 Invited Talk (Chair: Stefania Gnesi)
Attacking Large Industrial Code with Bi-Abductive Inference.
Dino Distefano (Queen Mary, University of London, UK)

15:30 - 16:00 Coffee Break

16:00 Session 2 (Chair: Dino Distefano)

Correctness with respect to reference implementations.
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto and Bárbara Vieira.

Preemption Abstraction: a Lightweight Approach to Modelling Concurrency.
Erik Schierboom, Alejandro Tamalet, Hendrik Tews, Marko van Eekelen and Sjaak Smetsers.

A Certified Implementation on top of the Java Virtual Machine
Javier de Dios and Ricardo Peña.

19:30 Workshop Dinner and EASST award

Tuesday 3 November

9:00 Invited Talk (Chair: Alessandro Fantechi)
On a Uniform Framework for the Definition of Stochastic Process Languages.
Diego Latella (ISTI-CNR, Italy)

10:00 - 10:30 Coffee Break

10:30 Session 3 (Chair: Santiago Escobar)

Formal Analysis of Non-Determinism in Verilog Cell Library Simulation Models
Matthias Raffelsieper, MohammadReza Mousavi, Jan-Willem Roorda, Chris Strolenberg and Hans Zantema.

Formal Modeling of Concurrent Systems with Shared Resources.
Julio Mariño, Ángel Herranz, Manuel Carro and Juan José Moreno-Navarro.

A Rigorous Methodology for Composing Services.
Kenneth J. Turner and Koon Leai Larry Tan.

12:00 - 14:00 Lunch

14:00 Invited Talk (Chair: Diego Latella)
Applying a Formal Method in Industry: a 15-year trajectory
Thierry Lecomte (ClearSy, France)

15:00 Poster Session 2 (Chair: María del Mar Gallardo)

Visualizing Event-B models with BMotionStudio.
Lukas Ladenberger, Jens Bendisposto and Michael Leuschel.

Model-Based Testing of Electronic Passports.
Wojciech Mostowski, Erik Poll, Julien Schmaltz, Jan Tretmans and Ronny Wichers Schreur.

Behavioural Analysis of an I2C Linux Driver.
Aad Mathijssen, Yaroslav S. Usenko and Dragan Bosnacki.

15:30 - 16:00 Coffee Break

16:00 Session 4 (Chair: Christophe Joubert)

Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs.
Pavel Parizek and Tomas Kalibera.

Dynamic State Space Partitioning for External Memory Model Checking
Sami Evangelista and Lars Michael Kristensen.

17:30 FMICS 2009 Closure and FMICS WG Meeting

Papers' Abstracts

Dino Distefano. Attacking Large Industrial Code with Bi-Abductive Inference.

Abstract: In joint work with Cristiano Calcagno, Peter O'Hearn, and Hongseok Yang, we have introduced bi-abductive inference and its use in reasoning about heap manipulating programs [Calcagno-et-al-POPL-2009]. This extended abstract briefly surveys the key concepts and describes our experience in the application of bi-abduction to real-world applications and systems programs of over one million lines of code.

Rocco De Nicola, Diego Latella, Michele Loreti and Mieke Massink. On a Uniform Framework for the Definition of Stochastic Process Languages.

Abstract: In this paper we show how Rate Transition Systems (RTSs) can be used as a unifying framework for the definition of the semantics of stochastic process algebras. RTSs facilitate the compositional definition of such semantics exploiting operators on the next state functions which are the functional counterpart of classical process algebra operators. We apply this framework to representative fragments of major stochastic process calculi namely TIPP, PEPA and IML and show how they solve the issue of transition multiplicity in a simple and elegant way. We, moreover, show how RTSs help describing different languages, their differences and their similarities. For each calculus, we also show the formal correspondence between the RTSs semantics and the standard SOS one.

Thierry Lecomte. Applying a Formal Method in Industry: a 15-year trajectory

Abstract: This article presents industrial experience of applying the B formal method in the industry, on diverse application fields (railways, automotive, smartcard, etc.). If the added value of such an approach has been demonstrated over the year, using a formal method is not the panacea and requires some precautions when introduced in an industrial development cycle.

Ken McMillan. What's in common between Test, Model checking, and Decision Procedures?

Abstract: The interaction of proof search and counterexample search is at the heart of recent methods in decision procedures model checking. In this talk, we'll consider the relation between these methods and test.

José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto and Bárbara Vieira. Correctness with respect to reference implementations.

Abstract: This paper presents techniques developed to check program equivalences in the context of cryptographic algorithms, which are typically specified by means of reference implementations. The techniques allow for the integration of interactive proof techniques (required given the difficulty and generality of the results sought) in a verification infrastructure that is capable of discharging many verification conditions automatically, in such a way that the difficult results (to be proved interactively) are isolated as a set of lemmas. The fundamental notion of natural invariant is used to link the specification level and the interactive proofs.

David Delmas, Eric Goubault, Sylvie Putot, Jean Souyris, Karim Tekkal and Franck Védrine. Towards an industrial use of FLUCTUAT on safety-critical avionics software.

Abstract: Most modern safety-critical control programs, such as those embedded in fly-by-wire control systems, perform a lot of floating-point computations. The well-known pitfalls of IEEE 754 arithmetic make stability and accuracy analyses a requirement for this type of software. This need is traditionally addressed through a combination of testing and sophisticated intellectual analyses, but such a process is both costly and error-prone. FLUCTUAT is a static analyzer developed by CEA-LIST for studying the propagation of rounding errors in C programs. After a long time research collaboration with CEA-LIST on this tool, Airbus is now willing to use FLUCTUAT industrially, in order to automate part of the accuracy analyses of some control programs. In this paper, we present the IEEE 754 standard, the FLUCTUAT tool, the types of codes to be analyzed and the analysis methodology, together with code examples and analysis results.

Javier de Dios and Ricardo Peña. A Certified Implementation on top of the Java Virtual Machine.

Abstract: Safe is a first-order functional language with unusual memory management features: memory is explicitly and implicitly deallocated at some specific points in the program text, and there is no need for a runtime garbage collector. The final code is bytecode of the Java Virtual Machine (JVM), so the language is useful for programming small devices based on this machine. As an intermediate stage in the compiler's back-end, we have defined the Safe Virtual Machine (SVM), and have implemented this machine on top of the Java Virtual Machine (JVM). As one of the aims of Safe is providing certificates (mathematical proofs) for some program properties, we require this implementation to be certified, i.e.\ the semantics of Safe must be preserved across all the translations. We have used the proof assistant Isabelle/HOL for this purpose. The paper presents the certified implementation of the SVM on top of the JVM. First an introduction to Safe and SVM is done; then the main decisions in order to map the SVM data structures to the JVM are explained. Finally, the Isabelle/HOL formalisations of SVM, JVM, and of the mapping between both are presented, and the main correctness theorem is proved.

Sami Evangelista and Lars Michael Kristensen. Dynamic State Space Partitioning for External Memory Model Checking.

Abstract: We describe a dynamic partitioning scheme usable by model checking techniques that divide the state space into partitions, such as most external memory and distributed model checking algorithms. The goal of the scheme is to reduce the number of transitions that link states belonging to different partitions, and thereby limit the amount of disk access and network communication. We report on several experiments made with our verification platform ASAP that implements the dynamic partitioning scheme proposed in this paper.

Alwyn Goodloe and César Muñoz. Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle.

Abstract: We present the specification and verification, in PVS, of a protocol intended to facilitate communication in an experimental remotely operated vehicle used by NASA researchers. The protocol is defined as the stack-layered composition of simpler protocols. It can seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process satisfies a distinct requirement.  We formally prove that the protocol components satisfy certain delivery guarantees.  Then, we demonstrate compositional techniques that allow us to prove that these guarantees also hold in the composed system.  Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the routine, but usually cumbersome, part of the proof, thereby making an industrial iterative design process feasible.

Julio Mariño, Ángel Herranz, Manuel Carro and Juan José Moreno-Navarro. Formal Modeling of Concurrent Systems with Shared Resources.

Abstract: Testing is the more extended approach to system validation in industry. The introduction of concurrency makes exhaustive testing extremely costly or directly impossible. Validation of concurrent systems demands formal verification techniques. We propose a methodology for designing and verifying a concurrent system that splits the verification problem in two independent tasks: internal verification of shared resources, where some concurrency aspects like mutual exclusion and conditional synchronisation are isolated, and external verification of processes, where synchronisation mechanisms are not relevant. Our method is language independent, is not a deterrent for developers, helps in the  verification process and improves the portability of the resulting system. We demonstrate the method with several examples.

Pavel Parizek and Tomas Kalibera. Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs.

Abstract: The main limitation of software model checking is that, due to state explosion, it does not scale to real-world multi-threaded programs. One of the reasons is that current software model checkers adhere to full semantics of programming languages, which are based on very permissive models of concurrency. Current runtime platforms for programs, however, restrict concurrency in various ways - it is visible especially in the case of critical embedded systems, which typically involve only a single processor and use threading model based on limited preemption. In this paper, we present a technique for addressing state explosion in model checking of Java programs for embedded systems, which exploits restrictions of concurrency common to current Java platforms for such systems. We have implemented the technique in Java PathFinder and performed a number of experiments on Purdue Collision Detector, which is a non-trivial multi-threaded Java program. Results of experiments show that use of the restrictions of concurrency in model checking with Java PathFinder reduces the state space size by an order of magnitude and also reduces time needed to discover errors in Java programs.

Matthias Raffelsieper, MohammadReza Mousavi, Jan-Willem Roorda, Chris Strolenberg and Hans Zantema. Formal Analysis of Non-Determinism in Verilog Cell Library Simulation Models.

Abstract: Cell libraries often contain a simulation model in a system design language, such as Verilog. These languages usually involve non-determinism, which in turn, poses a challenge to their validation. Simulators often resolve such problems by using certain rules to make the specification deterministic. This however is not justified by the behavior of the hardware that is to be modeled. Hence, simulation might not be able to detect certain errors. In this paper we develop a technique to prove whether non-determinism does not affect the behavior of the simulation model, or whether there exists a situation in which the simulation model might produce different results. To make our technique efficient, we show that the global property of equal behavior for all possible evaluations is equivalent to checking only a certain local property.

Erik Schierboom, Alejandro Tamalet, Hendrik Tews, Marko van Eekelen and Sjaak Smetsers. Preemption Abstraction: a Lightweight Approach to Modelling Concurrency.

Abstract: This paper presents the preemption abstraction, an abstraction technique for the lightweight verification of one sequential component of a concurrent system. Thereby, different components of the concurrent system are permitted to interfere with each other. The preemption abstraction yields a sequential abstract system, that can easily be described in the higher-order logic of a theorem prover. One can therefore avoid the cumbersome and costly reasoning about all possible interleavings of state changes of each system component. The preemption abstraction is best suited for components that use preemption points, that is, where the concurrently running environment can only interfere at a limited number of points. The preemption abstraction has been used to model an abstract version of the IPC subsystem of the Fiasco microkernel. We proved two practically relevant properties on the model. On the attempt to prove a third property, namely that the assertions in the code are always valid, we discovered a bug that could potentially crash the whole system.

Kenneth J. Turner and Koon Leai Larry Tan. A Rigorous Methodology for Composing Services.

Abstract: Creating new services through composition of existing ones is an attractive option. However, composition can be complex and service compatibility needs to be checked. A rigorous and industrially-usable methodology is therefore desirable required for creating, verifying, implementing and validating composed services. An explanation is given of the approach taken by Cress (Communication Representation Employing Systematic Specification). Formal verification and validation are performed through automated translation to Lotos (Language Of Temporal Ordering Specification). Implementation and validation are performed through automated translation to Bpel (Business Process Execution Logic) and WSDL (Web Services Description Language). The approach is illustrated with an application to grid service composition in e-Social Science.

Posters' Abstracts

Alessio Ferrari, Alessandro Fantechi, Stefano Bacherini and Niccolò Zingoni. Formal Development for Railway Signaling Using Commercial Tools.

Abstract: This report presents the approach experimented by a railway signaling manufacturer for the development of applications through Simulink/Stateflow in a standard–regulated industrial framework.

Nassima Izerrouken, Marc Pantel, Xavier Thirioux and Olivier Ssi yan kai. Integrated Formal Approach for Qualified Critical Embedded Code Generator.

Abstract: This paper sums up the integration of a correct-by-construction components for the qualifiable GeneAuto automatic code generator from Simulink models to C code for safety critical systems. Our approach which combines classical development process and formal specification and verification using proof-assistants, led to preliminary fruitful exchanges with French certification authorities. The resulting tool has been applied successfully to real-size industrial use case from various transportation domain partners and led to requirement errors detection.

Lukas Ladenberger, Jens Bendisposto and Michael Leuschel. Visualizing Event-B models with BMotionStudio.

Abstract: The communication between a developer and a domain expert (or manager) is a very important for successful deployment of formal methods. On the one hand it is crucial for the developer to get feedback from the domain expert for further development. On the other hand the domain expert needs to check whether his expectations are met. An animation tool allows to check the presence of desired functionality and to inspect the behaviour of a speciification, but requires knowledge about the mathematical notation. To avoid this problem, it is useful to create domain specific visualizations.

Aad Mathijssen, Yaroslav S. Usenko and Dragan Bosnacki. Behavioural Analysis of an I2C Linux Driver.

Abstract: We present an analysis of the behaviour of an I2C Linux driver, by means of model checking with the mCRL2 toolset and static analysis with UNO. We have reverse engineered the source code to obtain the structure and interactions of the driver. Based on these results, we have semi-automatically created an mCRL2 model of the behaviour of the driver, on which we have checked mutual exclusion properties. This revealed non-trivial potential errors, like unprotected usage of shared memory variables due to inconsistent locking and disabling/enabling of interrupts. We also applied UNO on the instrumented source code and were able to find the same errors. These defects were confirmed by the developers.

Wojciech Mostowski, Erik Poll, Julien Schmaltz, Jan Tretmans and Ronny Wichers Schreur. Model-Based Testing of Electronic Passports.

Abstract: Electronic passports, or e-passports for short, contain a contactless smartcard which stores digitally signed data. To rigorously test e-passports, we developed formal models of the e-passport protocols that enable model-based testing using the TorXakis framework.

Laura Panizo, Maria del Mar Gallardo, Pedro Merino and Antonio Linares. Developing a decision support tool for Dam management with SPIN.

Abstract: Analysis of critical systems is mainly based on the simulation of numerical models. This solution is suitable for analyzing systems with continuous and deterministic behaviors. However, real critical systems are more complex and can exhibit non-deterministic behavior due to unexpected events. Furthermore, critical systems present both discrete and continuous behaviors, which interact regularly. Both features can be modeled with hybrid formal methods, taking advantage of exploration techniques like model checking.