Fifth International Conference on Integrated Formal Methods
29 November - 2 December 2005 in Eindhoven, The Netherlands
Abstracts
Title: An Automated Failure Mode and Effect Analysis based on High-Level Design Specification with Behavior Trees
Author(s): Lars Grunske, Peter Lindsay, Nisansala Yatapanage and Kirsten Winter
Abstract: Formal methods have significant benefits for developing safety critical systems, in that they allow for correctness proofs, model checking safety and liveness properties, deadlock checking, etc. However, formal methods do not scale very well and demand specialist skills, when developing real-world systems. For these reasons, development and analysis of large-scale safety critical systems will require effective integration of formal and informal methods. In this paper, we use such an integrative approach to automate Failure Modes and Effects Analysis (FMEA), a widely used system safety analysis technique, using a high-level graphical modelling notation (Behavior Trees) and model checking. We inject component failure modes into the Behavior Trees and translate the resulting Behavior Trees to SAL code. This enables us to model check if the system in the presence of these faults satisfies its safety properties, specified by temporal logic formulas. The benefit of this process is tool support that automates the tedious and error-prone aspects of FMEA.
Keywords: Automated Hazard Analysis, FMEA, High-Level Design Specification, Model Checking, Behavior Trees, SAL
Title: Translating Hardware Process Algebras into Standard Process Algebras -- Illustration with CHP and LOTOS
Author(s): Gwen Salaun and Wendelin Serwe
Abstract: A natural approach for the description of asynchronous hardware designs are hardware process algebras, such as Martin's CHP (Communicating Hardware Processes), TANGRAM, or BALSA, which are extensions of standard process algebras with particular operators exploiting the implementation of synchronisation using handshake protocols. In this paper, we give a structural operational semantics for value-passing CHP. Compared to existing semantics of CHP defined by translation into Petri nets, our semantics handles value-passing CHP with communication channels open to the environment and is independent of any particular (2- or 4-phase) handshake protocol used for circuit implementation. In a second step, we describe the translation of CHP into the standard process algebra LOTOS, in order to allow the application of the CADP verification toolbox to asynchronous hardware designs. A prototype translator from CHP to LOTOS has been successfully used for the compositional verification of the control part of an asynchronous circuit implementing the DES (Data Encryption Standard).
Keywords:
Title: CZT Support for Z Extensions
Author(s): Tim Miller, Leo Freitas, Petra Malik and Mark Utting
Abstract: Community Z Tools (CZT) is an integrated framework for the Z formal specification language. In this paper, we show how it is also designed to support extensions of Z, in a way that minimises the work required to build a new Z extension. The goals of the framework are to maximise extensibility and reuse, and minimise code duplication and maintenance effort. To achieve these goals, CZT uses a variety of different reuse mechanisms, including generation of Java code from a hierarchy of XML schemas, XML templates for shared code, and several design patterns for maximising reuse of Java code. The CZT framework is being used to implement several integrated formal methods, which add object-orientation, real-time features and process algebra extensions to Z. The effort required to implement such extensions of Z has been dramatically reduced by using the CZT framework.
Keywords: Standard Z, Object-Z, TCOZ, \Circus, parsing, typechecking, animation, design patterns, framework, AST.
Title: An Integrated Framework for Scenarios and State Machines
Author(s): Bikram Sengupta and Rance Cleaveland
Abstract: This paper develops a semantic framework for interpreting heterogeneous system specifications consisting of a mixture of scenario-based requirements and state-based design. Such specifications arise naturally in spiral- and refinement-based development methodologies in which parts of a system have detailed designs while others exist in more abstract form as a collection of requirements. More precisely, we consider the scenario-based notation of Triggered Message Sequence Charts (TMSCs) and the state-based notation of Communicating State Machines (CSMs), and show how they may be integrated in a semantic framework that is founded on the mathematical theory of acceptance trees. Our semantic theory is also equipped with a robust notion of refinement, which allows us to relate one heterogeneous specification with another. A case-study serves to illustrate the utility of our framework as a basis for the principled evolution of higher-level requirements to lower-level operational specifications.
Keywords: scenarios, state-machines, heterogeneous specifications, refinement orderings.
Title: Model-based Prototyping of an Interoperability Protocol for Mobile Ad-hoc Networks
Author(s): Lars Kristensen, Michael Westergaard and Peder Christian Nørgaard
Abstract: We present an industrial project conducted at Ericsson Danmark A/S, Telebit where formal methods in the form of Coloured Petri Nets (CP-nets or CPNs) have been used for the specification of an interoperability protocol for routing packets between fixed core networks and mobile ad-hoc networks. The interoperability protocol ensures that a packet flow between a host in a core network and a mobile node in an ad-hoc network is always relayed via one of the closest gateways connecting the core network and the mobile ad-hoc network. This paper shows how integrated use of CP-nets and application-specific visualisation have been applied to build a model-based prototype of the interoperability protocol. The prototype consists of two parts: a CPN model that formally specifies the protocol mechanisms and a graphical user interface for experimenting with the protocol. The project demonstrates that the use of formal modelling combined with the use of application-specific visualisation can be an effective approach to rapidly construct an executable prototype of a communication protocol.
Keywords: Model-driven prototyping; animation; Coloured Petri Nets; mobile ad-hoc network.
Title: Development of Fault Tolerant Grid Applications Using Distributed B
Author(s): Pontus Boström and Marina Waldén
Abstract: Computational grids have become popular for constructing large scale distributed systems. Grid applications typically run in a very heterogeneous environment and fault tolerance is therefore very important for their correctness. Since the construction of correct distributed systems is difficult with traditional development methods we propose the use of formal methods. We use Event B as our formal framework, which we extend with new constructs such as remote procedures and notifications for reasoning about grid systems. The extended language, called Distributed B, ensures that the application can handle both node and network failures. Furthermore, the new constructs in Distributed B enable straightforward implementation of the specifications, as well as automatic generation of the needed proof obligations.
Keywords: Event B, Grid computing, Fault tolerance, Domain specific languages, Language extensions, Stepwise development
Title: Consistency in UML and B multi-view specifications
Author(s): Dieu Donné Okalas Ossami, Jean-Pierre Jacquot and Jeanine Souquières
Abstract: We present the notion of consistency relation in UML and B multi-view specifications. It is defined as a semantic relation between both views. It provides us with a sound basis to define the notion of development operator. An operator models a development step; it separates the design decisions from their expression in the specification formalisms. Operator correctness is defined as a property which guarantees that the application of an operator on a consistent specification state yields a consistent new state. An operator can be proven once and for all to be correct. A classical case-study, the Generalized Railroad Crossing (GRC), demonstrates how the different notions can be put in practice to provide specifiers with a realistic development model.
Keywords: consistency, verification, operator, multi-view, UML, B.
Title: Formal methods meet Domain Specific Languages
Author(s): Jean-Paul Bodeveix, Mamoun Filali, Julia Lawall and Gilles Muller
Abstract: In this paper, we relate an experiment whose aim is to study how to combine two existing approaches for ensuring software correctness: Domain Specific Languages (DSLs) and formal methods. As examples, we consider the Bossa DSL and the B formal method. Bossa is dedicated to the development of process schedulers and has been used in the context of Linux and Chorus. B is a refinement based formal method which has especially been used in the domain of railway systems. In this paper, we use B to express the correctness of a Bossa specification. Furthermore, we show how B can be used as an alternative to the existing Bossa tools for the production of certified schedulers.
Keywords: DSL, scheduling, formal methods, refinements, decision procedure.
Title: Agile Formal Method Engineering
Author(s): Richard Paige and Phil Brooke
Abstract: Software development methods are software products, in the sense that they should be engineered by following a methodology to meet the behavioural and non-behavioural requirements of the intended users of the method. We argue that agile approaches are the most appropriate means for engineering new methods, and particularly for integrating formal methods. We show how agile principles and practices apply to engineering methods, and demonstrate their application by integrating parts of the Eiffel development method with CSP.
Keywords:
Title: A Fixpoint Semantics of Event Systems with and without Fairness Assumptions
Author(s): Hector Ruiz Barradas and Didier Bert
Abstract: We present a fixpoint semantics of event systems. The semantics is presented in a general framework without concerns of fairness. Soundness and completeness of rules for deriving leads-to properties are proved in this general framework. The general framework is instantiated to minimal progress and weak fairness assumptions and similar results are obtained. We show the power of these results by deriving sufficient conditions for leads-to under minimal progress proving soundness of proof obligations without reasoning over state-traces.
Keywords: Liveness properties, event systems, action systems, unity logic, fairness, weak fairness, minimal progress, set transformer, fixpoints.
Title: Exp.Open 2.0: A Flexible tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods
Author(s): Frederic Lang
Abstract: It is desirable to integrate formal verification techniques applicable to different languages. We present Exp.Open 2.0, a new tool of the CADP verification toolbox which combines several features. First, Exp.Open 2.0 allows to describe concurrent systems as a composition of finite state machines, using either synchronization vectors, or parallel composition, hiding, renaming, and cut operators from several process algebras (CCS, CSP, Lotos, E-Lotos, muCRL). Second, together with other tools of CADP, Exp.Open 2.0 allows state space generation and on-the-fly exploration. Third, Exp.Open 2.0 implements on-the-fly partial order reductions to avoid the generation of irrelevant interleavings of independent transitions. Fourth, Exp.Open 2.0 allows to export models towards other tools using interchange formats such as automata networks and Petri nets. Finally, we show some practical applications and measure the efficiency of Exp.Open 2.0 on several benchmarks.
Keywords:
Title: Synthesizing B Specifications from EB3 Attribute Definitions
Author(s): Frédéric Gervais, Marc Frappier and Régine Laleau
Abstract: EB^3 is a trace-based formal language created for the specification of information systems (IS). Attributes, linked to entities and associations of an IS, are computed in EB^3 by recursive functions on the valid traces of the system. On the other hand, B is a state-based formal language also well adapted for the specification of IS. In this paper, we deal with the synthesis of B specifications that correspond to EB^3 attribute definitions, in order to specify and verify safety properties like data integrity constraints. Each action in the EB^3 specification is translated into a B operation. The substitutions are obtained by an analysis of the CAML-like patterns used in the recursive functions that define the attributes in EB^3. Our technique is illustrated by an example of a simple library management system.
Keywords: Information systems, data integrity constraints, attributes, B, EB^3, recursive functions, pattern matching.
Title: Formalising Interactive Voice Services with SDL
Author(s): Kenneth Turner
Abstract: IVR (Interactive Voice Response) services are introduced with reference to VoiceXML (Voice eXtensible Markup Language). It is explained how IVR services can benefit from an underlying formalism and rigorous analysis. IVR services are modelled using Cress (Chisel Representation Employing Systematic Specification) as a high-level graphical notation. Apart from being able to describe services, Cress also introduces the notion of features. The translation of IVR descriptions into SDL is explored, along with how the generated SDL can be formally analysed.
Keywords: Feature, IVR (Interactive Voice Response), SDL (Specification and Description Language), Service, VoiceXML (Voice eXtensible Markup Language).
Title: Embedding the Stable Failures Model of CSP in PVS
Author(s): Kun Wei and James Heather
Abstract: We present an embedding of the stable failures model of CSP in the PVS theorem prover. Our work, extending a previous embedding of the traces model of CSP in [6], provides a platform for the formal verification not only of safety specifications, but also of liveness specifications of concurrent systems in theorem provers. Such a platform is particularly good at analyzing infinite-state systems with an arbitrary number of components. We demonstrate the power of this embedding by using it to construct formal proofs that the asymmetric dining philosophers problem with an arbitrary number of philosophers is deterministic and deadlock-free, and that an industrial-scale example, a `virtual network' [21], with any number of dimensions, is deadlock-free. We have established some generic proof tactics for verification of properties of networks with many components. In addition, our technique of integrating FDR and PVS in our demonstration allows for handling of systems that would be difficult or impossible to analyze using either tool on its own.
Keywords: CSP, theorem prover, liveness, deadlock, determinism.
Title: Chunks: component verification in CSP||B
Author(s): Steve Schneider, Helen Treharne and Neil Evans
Abstract: CSP||B is an approach to combining the process algebra CSP with the formal development method B, enabling the formal description of systems involving both event-oriented and state-oriented aspects of behaviour. The approach provides architectures which enable the application of CSP verification tools and B verification tools to the appropriate parts of the overall description. Previous work has considered how large descriptions can be verified using coarse grained component parts. This paper presents a generalisation of that work so that CSP||B descriptions can be decomposed into finer grained components, chunks, which focus on demonstrating the absence of particular divergent behaviour separately. The theory underpinning chunks is applicable not only to CSP||B specification but to CSP specifications. This makes it an attractive technique to decomposing large systems for analysing with FDR.
Keywords: Component based verification, B-Method, CSP, decomposition.
Title: Consistency Checking of Sequence Diagrams and Statechart Diagrams Using the pi-Calculus
Author(s): Vitus Lam and Julian Padget
Abstract: UML 2.0, like UML 1.x, provides only a set of notations for specifying different aspects of a system. The problem of checking consistency between various types of models in software development is still not fully addressed. In this paper, we suggest the use of an algebraic approach for verifying whether consistency between sequence diagrams and statechart diagrams is preserved. First, statechart diagrams are encoded in the pi-calculus. Then, each object in a sequence diagram is translated into its equivalent pi-calculus definitions and verified against the corresponding statechart diagram represented in the pi-calculus using the Mobility Workbench. The applicability of the proposed approach is illustrated with an agent-based payment protocol.
Keywords:
Title: Enabling Security Testing from Specification to Code
Author(s): Shane Bracher and Padmanabhan Krishnan
Abstract: In this paper, we present the idea of creating an intermediary model which is capable of being derived directly from the high-level, abstract model, but more closely resembles the actual implementation. The focus of our work is on the security properties of protocols. Not only do we show how an intermediary model can be constructed, but also how it can be used to automatically generate test sequences based on the security goals of the protocol being tested. Our aim is to show that by using this approach, we can derive test sequences suitable for a tester to use on a working implementation of the protocol.
Keywords: protocol descriptions, security modelling, model-based testing, concrete test sequences
Title: Adaptive Techniques for Specification Matching in Embedded Systems: A Comparative Study
Author(s): Robi Malik and Partha S. Roop
Abstract: The specification matching problem in embedded systems is to determine whether an existing component may be adapted suitably to match the requirements of a new specification. Recently, a refinement called forced simulation has been introduced to formally address this problem. It has been established that when a forced similarity relation exists between a component and its specification, an adapter process can be constructed so that the composition of the adapter and the component fulfil the specification. This looks very similar to synthesis methods in supervisory control theory, where a controller is constructed to make a plant satisfy a desired specification. However, due to the need for state-based hiding in specification matching, supervisory control theory is not directly applicable. This paper develops a supervisory control based solution to the specification matching problem by modifying the problem representation. Subsequently, a comparison of the forced simulation and supervisory control based specification matching methods is made.
Keywords: Formal verification, specification matching, embedded systems, supervisory control, finite-state machines, bisimulation.
Title: State/Event Software Verification for Branching-Time Specifications
Author(s): Sagar Chaki, Edmund Clarke, Orna Grumberg, Joel Ouaknine, Natasha Sharygina, Tayssir Touili and Helmut Veith
Abstract: In the domain of concurrent software verification, there is an evident need for specification formalisms and efficient algorithms to verify branching-time properties that involve both data and communication. We address this problem by defining a new branching-time temporal logic SE-A\Omega which integrates both state-based and action-based properties. SE-A\Omega is universal, i.e., preserved by the simulation relation, and thus amenable to counterexample-guided abstraction refinement. We provide a model-checking algorithm for this logic, based upon a compositional abstraction-refinement loop which exploits the natural decomposition of the concurrent system into its components. The abstraction and refinement steps are performed over each component separately, and only the model checking step requires an explicit composition of the abstracted components. For experimental evaluation, we have integrated our algorithm within the ComFoRT reasoning framework and used it to verify a piece of industrial robot control software.
Keywords: Concurrent Software Model Checking, State/Event-based Verification, Branching-time Temporal Logic, Automated Abstraction Refinement.
Title: Software Model Checking: Searching for Computations in the Abstract or the Concrete
Author(s): Patrice Godefroid
Abstract: We review and discuss the current approaches to software model checking, including the complementary views of validation versus falsification and those of static versus dynamic analysis. For falsification, also known as bug finding, we advocate the need for blended approaches that combine the strengths of both static and dynamic analysis. We outline possible directions of research in this area.
Keywords:
Title: A Family of Mathematical Methods for Professional Software Documentation
Author(s): David Parnas
Abstract: The movement to integrate mathematically based software development methods is a predictable response to the fact that none of the many methods available seems sufficient to do the whole job (whatever that may be) on its own. This talk argues that integrating separately developed methods is not the most fruitful possible approach. Instead we propose a family of methods, based on a common model, designed to be complementary and mutually supportive. The method family being developed at the Software Quality Research Lab at the University of Limerick is characterised by two major decisions: - Software developers must prepare and maintain a set of documents whose content (not format) is specified by the relational model presented in [3]. - The relations are represented using mathematical expressions in tabular form [5]. This talk will motivate these decisions, describe the model, illustrate the concept of tabular expressions, and discuss the uses of such documents in software development.
Keywords:
Title: Generating Path Conditions for Timed Systems
Author(s): Doron Peled
Abstract: We provide an automatic method for calculating the path condition for programs with real time constraints. This method can be used for the semiautomatic verification of a unit of code in isolation, i.e., without providing the exact values of parameters with which it is called. Our method can also be used for the automatic generation of test cases for unit testing. The current generalization of the calculation of path condition for the timed case turns out to be quite tricky, since not only the selected path contributes to the path condition, but also the timing constraints of alternative choices in the code.
Keywords:
