Integrated Formal Methods

Frontmatter

On Model Checking Techniques for Randomized Distributed Systems

Abstract

The automata-based model checking approach for randomized distributed systems relies on an operational interleaving semantics of the system by means of a Markov decision process and a formalization of the desired event E by an ω-regular linear-time property, e.g., an LTL formula. The task is then to compute the greatest lower bound for the probability for E that can be guaranteed even in worst-case scenarios. Such bounds can be computed by a combination of polynomially time-bounded graph algorithm with methods for solving linear programs. In the classical approach, the “worst-case” is determined when ranging over all schedulers that decide which action to perform next. In particular, all possible interleavings and resolutions of other nondeterministic choices in the system model are taken into account. The worst-case analysis relying on this general notion of schedulers is often too pessimistic and leads to extreme probability values that can be achieved only by schedulers that are unrealistic for parallel systems. This motivates the switch to more realistic classes of schedulers that respect the fact that the individual processes only have partial information about the global system states. Such classes of partial-information schedulers yield more realistic worst-case probabilities, but computationally they are much harder. A wide range of verification problems turns out to be undecidable when the goal is to check that certain probability bounds hold under all partial-information schedulers.

Christel Baier

Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems

Abstract

This paper presents initial results of research aimed at developing methods and tools for multidisciplinary collaborative development of dependable embedded systems. We focus on the construction and analysis by co-simulation of formal models that combine discrete-event specifications of computer-based controllers with continuous-time models of the environment with which they interact. Basic concepts of collaborative modelling and co-simulation are presented. A pragmatic realisation using the VDM and Bond Graph formalisms is described and illustrated by means of an example, which includes the modelling of both normal and faulty behaviour. Consideration of a larger-scale example from the personal transportation domain suggests the forms of support needed to explore the design space of collaborative models. Based on experience so far, challenges for future research in this area are identified.

John Fitzgerald, Peter Gorm Larsen, Ken Pierce, Marcel Verhoef, Sune Wolff

Programming with Miracles

Abstract

In his seminal book, A Discipline of Programming [EWD 76], Dijkstra proposed that all sequential programs satisfy four laws for their weakest preconditions. By far the catchiest name was reserved for the Law of the Excluded Miracle, which captured the intuition that, started in a given state, a program execution must either terminate or loop forever. In the late 1980s, both Nelson [GN 89] and Morgan [CCM 90] noted that the law was unnecessarily restrictive when writing programs to be used as specifications. In the years since,“miracles” have become a standard feature in specification languages (for instance, the assume statement in JML [LLP+00] and BoogiePL [DL 05]).

What is perhaps surprising is that miracles are not as commonly used in programs written as implementations. This is surprising because for many everyday tasks, programming in a language with miracles is often far superior to the popular scripting languages that are used instead. In this talk, we build upon pioneering work by Burrows and Nelson [GN 05] who designed the language LIM (“Language of the Included Miracle”). We describe a language LIMe (“LIM with extensions”), and discuss its application in the context of flight software testing, including the analysis of spacecraft telemetry logs.

Rajeev Joshi

An Event-B Approach to Data Sharing Agreements

Abstract

A Data Sharing Agreement (DSA) is a contract among two or more principals regulating how they share data. Agreements are usually represented as a set of clauses expressed using the deontic notions of obligation, prohibition and permission. In this paper, we present how to model DSAs using the Event-B specification language. Agreement clauses are modelled as temporal-logic formulas that preserve the intuitive meaning of the deontic operators, and constrain the actions that a principal can execute. We have exploited the ProB animator and model checker in order to verify that a system behaves according to its associated DSA and to validate that principals’ actions are in agreement with the DSA clauses.

Alvaro E. Arenas, Benjamin Aziz, Juan Bicarregui, Michael D. Wilson

A Logical Framework to Deal with Variability

Abstract

We present a logical framework that is able to deal with variability in product family descriptions. The temporal logic MHML is based on the classical Hennessy–Milner logic with Until and we interpret it over Modal Transition Systems (MTSs). MTSs extend the classical notion of Labelled Transition Systems by distinguishing possible (may) and required (must) transitions: these two types of transitions are useful to describe variability in behavioural descriptions of product families. This leads to a novel deontic interpretation of the classical modal and temporal operators, which allows the expression of both constraints over the products of a family and constraints over their behaviour in a single logical framework. Finally, we sketch model-checking algorithms to verify MHML formulae as well as a way to derive correct products from a product family description.

Patrizia Asirelli, Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi

Adding Change Impact Analysis to the Formal Verification of C Programs

Abstract

Handling changes to programs and specifications efficiently is a particular challenge in formal software verification. Change impact analysis is an approach to this challenge where the effects of changes made to a document (such as a program or specification) are described in terms of rules on a semantic representation of the document. This allows to describe and delimit the effects of syntactic changes semantically. This paper presents an application of generic change impact analysis to formal software verification, using the GMoC and SAMS tools. We adapt the GMoC tool for generic change impact analysis to the SAMS verification framework for the formal verification of C programs, and show how a few simple rules are sufficient to capture the essence of change management.

Serge Autexier, Christoph Lüth

Creating Sequential Programs from Event-B Models

Abstract

Event-B is an emerging formal method with good tool support for various kinds of system modelling. However, the control flow in Event-B consists only of non-deterministic choice of enabled events. In many applications, notably in sequential program construction, more elaborate control flow mechanisms would be convenient. This paper explores a method, based on a scheduling language, for describing the flow of control. The aim is to be able to express schedules of events; to reason about their correctness; to create and verify patterns for introducing correct control flow. The conclusion is that using patterns, it is feasible to derive efficient sequential programs from event-based specifications in many cases.

Pontus Boström

Symbolic Model-Checking of Optimistic Replication Algorithms

Abstract

The Operational Transformation (OT) approach, used in many collaborative editors, allows a group of users to concurrently update replicas of a shared object and exchange their updates in any order. The basic idea of this approach is to transform any received update operation before its execution on a replica of the object. This transformation aims to ensure the convergence of the different replicas of the object. However, designing transformation algorithms for achieving convergence is a critical and challenging issue. In this paper, we address the verification of OT algorithms with a symbolic model-checking technique. We show how to use the difference bound matrices to explore symbolically infinite state-spaces of such systems and provide symbolic counterexamples for the convergence property.

Hanifa Boucheneb, Abdessamad Imine, Manal Najem

From Operating-System Correctness to Pervasively Verified Applications

Abstract

Though program verification is known and has been used for decades, the verification of a complete computer system still remains a grand challenge. Part of this challenge is the interaction of application programs with the operating system, which is usually entrusted with retrieving input data from and transferring output data to peripheral devices. In this scenario, the correct operation of the applications inherently relies on operating-system correctness. Based on the formal correctness of our real-time operating system Olos, this paper describes an approach to pervasively verify applications running on top of the operating system.

Matthias Daum, Norbert W. Schirmer, Mareike Schmidt

A Compositional Method for Deciding Equivalence and Termination of Nondeterministic Programs

Abstract

In this paper we address the problem of deciding may- and must-equivalence and termination of nondeterministic finite programs from second-order recursion-free Erratic Idealized Algol. We use game semantics to compositionally extract finite models of programs, and the CSP process algebra as a concrete formalism for representation of models and their efficient verification. Observational may- and must-equivalence and liveness properties, such as divergence and termination, are decided by checking traces refinements and divergence-freedom of CSP processes using the FDR tool. The practicality of the approach is evaluated on several examples.

Aleksandar Dimovski

Verification Architectures: Compositional Reasoning for Real-Time Systems

Abstract

We introduce a conceptual approach to decompose real-time systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local real-time assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a real-time logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSP-OZ-DC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification.

Johannes Faber

Automatic Verification of Parametric Specifications with Complex Topologies

Abstract

The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.

Johannes Faber, Carsten Ihlemann, Swen Jacobs, Viorica Sofronie-Stokkermans

Satisfaction Meets Expectations

Computing Expected Values of Probabilistic Hybrid Systems with SMT

Abstract

Stochastic satisfiability modulo theories (SSMT), which is an extension of satisfiability modulo theories with randomized quantification, has successfully been used as a symbolic technique for computing reachability probabilities in probabilistic hybrid systems. Motivated by the fact that several industrial applications call for quantitative measures that go beyond mere reachability probabilities, this paper extends SSMT to compute expected values of probabilistic hybrid systems like, e.g., mean-times to failure. Practical applicability of the proposed approach is demonstrated by a case study from networked automation systems.

Martin Fränzle, Tino Teige, Andreas Eggers

Showing Full Semantics Preservation in Model Transformation - A Comparison of Techniques

Abstract

Model transformation is a prime technique in modern, model-driven software design. One of the most challenging issues is to show that the semantics of the models is not affected by the transformation. So far, there is hardly any research into this issue, in particular in those cases where the source and target languages are different.

In this paper, we are using two different state-of-the-art proof techniques (explicit bisimulation construction versus borrowed contexts) to show bisimilarity preservation of a given model transformation between two simple (self-defined) languages, both of which are equipped with a graph transformation-based operational semantics. The contrast between these proof techniques is interesting because they are based on different model transformation strategies: triple graph grammars versus in situ transformation. We proceed to compare the proofs and discuss scalability to a more realistic setting.

Mathias Hülsbusch, Barbara König, Arend Rensink, Maria Semenyak, Christian Soltenborn, Heike Wehrheim

Specification and Verification of Model Transformations Using UML-RSDS

Abstract

In this paper we describe techniques for the specification and verification of model transformations using a combination of UML and formal methods. The use of UML 2 notations to specify model transformations facilitates the integration of model transformations with other software development processes. Extracts from three large case studies of the specification of model transformations are given, to demonstrate the practical application of the approach.

Kevin Lano, Shekoufeh Kolahdouz-Rahimi

Multiformalism and Transformation Inheritance for Dependability Analysis of Critical Systems

Abstract

Multiformalism approaches and automatic model generation are challenging issues in the context of the analysis of critical systems for which formal verification and validation are mandatory. Reusable model transformations may reduce the skill level required in formal modeling, time and cost of the analysis process, and they may support the integration among different formal languages. This paper investigates how the relationship existing between different classes of formal languages may be exploited to define new model transformations by extending existing definitions. Specifically, the inheritance relationship is considered with the ultimate goal of achieving formalisms integration also by developing proper reusable model transformations. This idea is applied to the integration between Repairable Fault Trees and Generalized Stochastic Petri Nets, where the inheritance relationship between Fault Trees and Repairable Fault Trees is the basis to define inheritable model transformations. The described techniques are demonstrated on the availability model of a modern railway controller.

Stefano Marrone, Camilla Papa, Valeria Vittorini

Translating Pi-Calculus into LOTOS NT

Abstract

Process calculi supporting mobile communication, such as the π-calculus, are often seen as an evolution of classical value-passing calculi, in which communication between processes takes place along a fixed network of static channels. In this paper, we attempt to bring these calculi closer by proposing a translation from the finite control fragment of the π-calculus to Lotos NT, a value-passing concurrent language with classical process algebra flavour. Our translation is succinct in the size of the π-calculus specification and preserves the semantics of the language by ensuring a one-to-one correspondence between the states and transitions of the labeled transition systems corresponding to the input π-calculus and the output Lotos NT specifications. We automated this translation by means of the Pic2Lnt tool, which makes it possible to analyze π-calculus specifications using all the state-of-the-art simulation and verification functionalities provided by the Cadp toolbox.

Radu Mateescu, Gwen Salaün

Systematic Translation Rules from astd to Event-B

Abstract

This article presents a set of translation rules to generate Event-B machines from process-algebra based specification languages such as astd. Illustrated by a case study, it details the rules and the process of the translation. The ultimate goal of this systematic translation is to take advantage of Rodin, the Event-B platform to perform proofs, animation and model-checking over the translated specification.

Jérémy Milhau, Marc Frappier, Frédéric Gervais, Régine Laleau

A CSP Approach to Control in Event-B

Abstract

Event-B has emerged as one of the dominant state-based formal techniques used for modelling control-intensive applications. Due to the blocking semantics of events, their ordering is controlled by their guards. In this paper we explore how process algebra descriptions can be defined alongside an Event-B model. We will use CSP to provide explicit control flow for an Event-B model and alternatively to provide a way of separating out requirements which are dependent on control flow information. We propose and verify new conditions on combined specifications which establish deadlock freedom. We discuss how combined specifications can be refined and the challenges arising from this. The paper uses Abrial’s Bridge example as the basis of a running example to illustrate the framework.

Steve Schneider, Helen Treharne, Heike Wehrheim

Towards Probabilistic Modelling in Event-B

Abstract

Event-B provides us with a powerful framework for correct-by-construction system development. However, while developing dependable systems we should not only guarantee their functional correctness but also quantitatively assess their dependability attributes. In this paper we investigate how to conduct probabilistic assessment of reliability of control systems modeled in Event-B. We show how to transform an Event-B model into a Markov model amendable for probabilistic reliability analysis. Our approach enables integration of reasoning about correctness with quantitative analysis of reliability.

Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis

Safe Commits for Transactional Featherweight Java

Abstract

Transactions are a high-level alternative for low-level concurrency-control mechanisms such as locks, semaphores, monitors. A recent proposal for integrating transactional features into programming languages is Transactional Featherweight Java (TFJ), extending Featherweight Java by adding transactions. With support for nested and multi-threaded transactions, its transactional model is rather expressive. In particular, the constructs governing transactions —to start and to commit a transaction— can be used freely with a non-lexical scope. On the downside, this flexibility also allows for an incorrect use of these constructs, e.g., trying to perform a commit outside any transaction. To catch those kinds of errors, we introduce a static type and effect system for the safe use of transactions for TFJ. We prove the soundness of our type system by subject reduction.

Thi Mai Thuong Tran, Martin Steffen

Certified Absence of Dangling Pointers in a Language with Explicit Deallocation

Abstract

Safe is a first-order eager functional language with facilities for programmer controlled destruction of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures, so that the runtime system does not need a garbage collector. A region is a collection of cells, each one big enough to allocate a data constructor. Deallocating cells or regions may create dangling pointers. The language is aimed at inferring and certifying memory safety properties in a Proof Carrying Code like environment. Some of its analyses have been presented elsewhere. The one relevant to this paper is a type system and a type inference algorithm guaranteeing that well-typed programs will be free of dangling pointers at runtime.

Here we present how to generate formal certificates about the absence of dangling pointers property inferred by the compiler. The certificates are Isabelle/HOL proof scripts which can be proof-checked by this tool when loaded with a database of previously proved theorems. The key idea is proving an Isabelle/HOL theorem for each syntactic construction of the language, relating the static types inferred by the compiler to the dynamic properties about the heap that will be satisfied at runtime.

Javier de Dios, Manuel Montenegro, Ricardo Peña

Integrating Implicit Induction Proofs into Certified Proof Environments

Abstract

We give evidence of the direct integration and automated checking of implicit induction-based proofs inside certified reasoning environments, as that provided by the Coq proof assistant. This is the first step of a long term project focused on 1) mechanically certifying implicit induction proofs generated by automated provers like Spike, and 2) narrowing the gap between automated and interactive proof techniques inside proof assistants such that multiple induction steps can be executed completely automatically and mutual induction can be treated more conveniently. Contrary to the current approaches of reconstructing implicit induction proofs into scripts based on explicit induction tactics that integrate the usual proof assistants, our checking methodology is simpler and fits better for automation. The underlying implicit induction principles are separated and validated independently from the proof scripts that consist in a bunch of one-to-one translations of implicit induction proof steps. The translated steps can be checked independently, too, so the validation process fits well for parallelisation and for the management of large proof scripts. Moreover, our approach is more general; any kind of implicit induction proof can be considered because the limitations imposed by the proof reconstruction techniques no longer exist. An implementation that integrates automatic translators for generating fully checkable Coq scripts from Spike proofs is reported.

Sorin Stratulat

Backmatter