Susanne Graf: Selected Publications

• 1. Edited Work
• 2. Journal Papers and Chapters of Books
• 3. Conference and Workshop Papers
• 4. Technical Reports not (yet) published
• 5. Thesis

Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings

Abstract

[download]

Bibtex reference

4th Symposium on Formal Methods for Components and Objects, revised lectures

Abstract

[download]

Bibtex reference

2nd workshop on Modelling and Analysis of Real-Time Embedded Systems (MARTES 2006)

[download]

Bibtex reference

Specification and Validation of Models of Real Time and Embedded Systems in UML

[download]

Bibtex reference

1st workshop on Modelling and Analysis of Real-Time Embedded Systems (MARTES 2005)

[download]

Bibtex reference

Specification and Validation of UML models for Real Time and Embedded Systems: An STTT special section

Abstract

The papers in this special section appeared originally in the proceedings of the first issue of the workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS 2003)

[download]

Bibtex reference

3rd Symposium on Formal Methods for Components and Objects, revised lectures

Abstract

[download]

Bibtex reference

2nd workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS 2004)

Abstract

Topic: Today's applications have often strong constraints with respect to time related aspects. Moreover, overall systems may be huge, and even if the embedded hard real-time components are relatively small, there is some global interdependence and the existence of a global model in a uniform framework is an important issue. The Unified Modeling Language UML can play this role, even if the real-time aspects are not really integrated today. The definition of UML has been motivated by the need for a standard notation for modelling system architectures and behaviours at functional and implementation level. UML aims at providing an integrated modelling framework encompassing architecture descriptions and behaviour descriptions. A first step to the integration of extra functional characteristics into the modelling framework has been achieved by the UML profile for schedulability, Time and Performance; It provides the basic concepts and a first attempt for a common syntax. Nevertheless, in order to be able to exchange models and to build validation tools, it is important to have also a common understanding of the semantics of the given notations. Other important issues in the domain of real-time is methodology and modeling paradigms allowing to break down the complexity, and tools which are able to verify well designed systems. This workshop should bring together researchers to discuss different time related issues in the context of modeling, design and validation of real-time systems, such as

• notations for expressing time and related requirements
• semantic issues and tools
• modeling paradigms for real-time systems

[download]

Bibtex reference

2nd Symposium on Formal Methods for Components and Objects, revised lectures

Abstract

[download]

Bibtex reference

11th International SPIN Workshop on Model Checking of Software, 2004

Abstract

[download]

Bibtex reference

1st workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS 2003)

Abstract

[download]

Bibtex reference

1st Symposium on Formal Methods for Components and Objects, revised lectures

Abstract

[download]

Bibtex reference

Tools and Algorithms for the Construction and Analysis of Systems: An STTT special section

Abstract

The papers in this special section appeared originally in the proceedings of the 2000 edition of the conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2000) hold in Berlin as a constituent event of the European joint conferences on Theory and Practice of Software. All papers present tools relevant in the context of validation of systems. The first three focus on extensions or particular applications of model-checking techniques, whereas the fo urth one is about integration of design tools with validation tools, in particular theorem provers and model-checkers.

[download]

Bibtex reference

Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS2000

Abstract

[download]

Bibtex reference

SDL and MSC Workshop SAM 2000

Abstract

[download]

Bibtex reference

Time in Abstract State Machines

Abstract

State machines are considered a very general means of expressing computations in an implementation-independent way. There are also ways to extend the general state machine framework with distribution aspects. However, there is still no agreement when it comes to handling time in this framework. In this article we take a look at existing ways to enhance state machine frameworks. Based on this we propose a general framework of time extensions for state machines, which we relate to existing approaches. Our work is mainly based on time approaches for ASM, because ASM are considered a very general state machine model. Taking this into account, our approach is valid for state-transition systems in general.

[download]

Bibtex reference

La boîte à outils IF pour la modélisation et la vérification de systèmes temps réel

Bibtex reference

Timed annotations in UML

Abstract

This paper describes an approach for real-time modelling in UML, focusing on analysis and verification of time and scheduling related properties. To this aim a concrete UML profile, called the OMEGA profile, is defined. It is dedicated to real-time modelling by identifying a set of relevant concepts for real-time modelling which can be considered as a refinement of the standard SPT profile. The profile is based on a rich concept of event representing an instant of state change, and allows the expression of duration constraints between occurrences of events. These constraints can be provided in the form of OCL-like expressions annotating the specification or by means of state machines, stereotyped as observers. A framework for modelling scheduling issues is obtained by adding a notion of resource and a notion of execution time.
For proving the relevance of these choices, the profile has been implemented in a validation tool and applied to case studies.
It has a formal semantics and is sufficiently general and expressive to define a semantic underpinning for other real-time profiles of UML which in general define more restricted frameworks. In particular, most existing profiles handling real-time issues define a number of attributes representing particular durations or constraints on them and their semantic interpretation can be expressed in the OMEGA profile.

[download]

Bibtex reference

Validating Timed UML models by simulation and verification

Abstract

This paper presents a technique and a tool for model-checking operational (design level) UML models based on a mapping to a model of communicating extended timed automata. The target language of the mapping is the IF format, for which existing model-checking and simulation tools can be used.
Our approach takes into consideration most of the structural and behavioral features of UML, including object-oriented aspects. It handles the combination of operations, state machines, inheritance and polymorphism, with a particular semantic profile for communication and concurrency. We adopt a UML profile that includes extensions for expressing timing. The breadth of concepts covered by our mapping is an important point, as many previous approaches for applying formal validation to UML put stronger limiting conditions on the input models.
For expressing properties about models, a formalism called UML observers is defined in this paper. Observers reuse existing concepts like classes and state machines, and they may express a significant class of linear temporal properties.

[download]

Bibtex reference

Un profil UML et un outil pour la modélisation et la validation de systèmes temps-réel

Abstract

[download]

Bibtex reference

Roadmap: Component based design and Integration platforms

Abstract

[download]

Bibtex reference

Introduction to Tools and Algorithms for the Construction and Analysis of Systems: An STTT special section

Abstract

[download]

Bibtex reference

Compositional Minimisation of Finite State Systems using Interface Specifications

Abstract

[download]

Bibtex reference

Characterization of a sequentially consistent memory and verification of a cache memory by abstraction

Abstract

The contribution of the paper is two-fold. We give a set of properties expressible as temporal logic formulas such that any system satisfying them is a sequentially consistent memory, and which is sufficiently precise such that every reasonnable concrete system implementing a sequentially consistent memory satisfies these properties.
Then, we verify these properties on a particular distributed cache memory systems by means of a verification method, based on the use of abstract interpretation which has been presented in previous papers ([LBBGS95]) and often applied to finite state systems. The motivation of this paper was to show that it can also been applied to systems with infinite state space, and a more recent papers shows that the method can even be automatized ([GS97]).
This paper is a revised and extended version of ([Graf94]).

[download]

Bibtex reference

Property Preserving Abstractions for the Verification of Concurrent Systems

Abstract

We study property preserving transformations for reactive systems. The main idea is the use of simulations parameterized by Galois connections (alpha,gamma), relating the lattices of properties of two systems. We propose and study a notion of preservation of properties expressed by formulas of a logic, by a function alpha mapping sets of states of a system S into sets of states of a system S'. Roughly speaking, alpha preserves f if the satisfaction of f at some state of S implies that f is satisfied by any state in the image of this state by alpha. We give results on the preservation of properties expressed in sublanguages of the branching time mu-calculus when two systems S and S' are related via (alpha,gamma)-simulations. They can be used in particular to verify a property for a system by proving this property on a simpler system which is an abstraction of it. We show also under which conditions abstraction of concurrent systems can be computed from the abstraction of their components. This allows a compositional application of the proposed verification method. This is a revised version of the papers that appeared in CAV'92 [BensalemBouajjaniLoiseauxSifakis92] and in TAPSOFT'93 [GrafLoiseaux92]; the results are fully developed in the thesis of Claire Loiseaux (in french).

[download]

Bibtex reference

Verification of systems with time-constraints

Abstract

Bibtex reference

A Logic for the Description of non Deterministic Programs and their Properties

Abstract

We present a logic, called Synchronization tree logic (STL), for the specification and proof of programs described in a simple term language obtained from a constant Nil by using a set A of unary operators, a binary operator + and recursion. The elements of A represent names of actions, + represents non-deterministic choice, and Nil is the program performing no action. The language of formulas of the logic proposed contains the term language used for the description of programs, i.e., programs are formulas of the logic. This provides a uniform frame to deal with programs and their properties as the verification of an assertion t satisfies f (t is a program and f a formula) is reduced to the proof of the validity of the formula t implies f. We propose a sound, and under some conditions complete deductive system for STL and discuss its relation with modal logics used for the specification of programs.

Bibtex reference

A logic for the specification and proof of regular controllable processes of CCS

Abstract

Bibtex reference

A Modal Characterization of Observational Congruence on Finite Terms of CCS

Abstract

We propose a translation method for finite terms of CCS into formulas of a modal language representing their class of observational congruence. For this purpose, we define a modal language and a function associating with any finite term of CCS a formula of the language, satisfied by the term. Furthermore, this function is such that two terms are congruent if and only if the corresponding formulas are equivalent. The translation method consists in associating with operations on terms (that is action and +) operations on the corresponding formulas. This works is a first step towards the definition of a modal language with modalities expressing both possibility and inevitability that is compatible with observational congruence.

Bibtex reference

On Lamport's comparison between linear and branching time logic

Bibtex reference

Contracts for BIP: hierarchical interaction models for compositional verification

Abstract

This paper presents an extension of the BIP component framework to hierarchical components by considering also port sets of atomic components to be structured (ports may be in conflict or ordered, where a larger port represents an interaction set with larger interactions). A composed component consisting of a set of components connected through BIP connectors and a set of ports representing a subset of the internal connectors and ports, has two semantics: one in terms if interactions as defined by the BIP semantics, and one in terms of the actions represented by external ports where the structure of the port set of the component is derived from the internal structure of the component. A second extension consists in the addition of implicit interactions which is done through an explicit distinction of conflicting and concurrent ports: interactions involving only non conflicting ports can be executed concurrently without the existence of an explicit connector. Finally, we define contract-based reasoning for component hierarchies. A component C satisfies a contract (A,G) consisting of an assumption A (constraining the environment) and a guarantee G (constraining C), if its implementation satisfies G in an environment guaranteeing A. The contract (A,G) of a component C dominates a set of inner contracts (Ai,Gi) associated with the components defining it, if the composition -- according to the set of connectors defining C --- of the guarantees Gi in the environment defined by A gurantees G, and, if each of the assumptions Ai is weaker than the one defined by the composition of A with the remaining guarantees. This rule is correct because G expresses a property of C only, and not of the closed system obtained by composing A and C

[download]

Bibtex reference

An Approach to Modeling and Verification of Component Based Systems

Abstract

We propose results ensuring correctness by construction of a system from properties of its interaction model and of its components. We use a modelling framework based on an abstract layered model for components described in a previous paper. A component is the superposition of two models: a behavior model and an interaction model. Interaction models describe architectural constraints induced by connectors between components. We study conditions guaranteeing global or individual deadlock freedom for a system of interacting deadlock-free components depending only on its interaction model. We also provide examples illustrating the application of the results.

[download]

Bibtex reference

Ensuring Properties of Interaction Systems by Construction

Abstract

We propose results ensuring correctness by construction of a system from properties of its interaction model and of its components. The considered properties include deadlock-freedom, local progress of subsystems and robustness of these properties with respect to failure of components. This is done in a framework for component based modelling described in a previous paper. A component is the superposition of two models: a behaviour model and an interaction model. The interaction model describes the way the components may interact by introducing connectors that relate actions from different components. We illustrate our concepts and results with examples.

[download]

Bibtex reference

MARTES - Modelling and Analysis of Real Time and Embedded Systems Using UML

Abstract

This paper presents an overview on the outcomes of the workshop MARTES on Modelling and Analysis of Real Time and Embedded Systems that has taken place for the second time in association with the MoDELS/UML 2006 conference. Important themes discussed at this workshop concerned (1) tools for analysis and model transformation and (2) concepts for modelling quantitative aspects with the perspective of analysis.

[download]

Bibtex reference

Qualification d'architectures fontionnelles

Abstract

The scope of this paper is the development of a method supported by tools for the qualification of distributed functional architectures. Architecture qualification is concerned by the analysis of Quality of service criteria, such as performance, and resource dimensioning. This qualification implies the modelling of the functional architecture and its components, in a structured and step-wise view, using different UML2 diagrams. The functional architecture should be validated in terms of dependability and conformity, but also in terms of performance and resource dimensioning. The functional behaviour analysis is based on the use of UML activity diagrams, and this paper proposes some new operators in order to improve the readability and efficiency of activity diagrams. Finally the annotated UML diagrams are translated towards models for performance evaluation.

[download]

Bibtex reference

A case study in UML model-based validation: The Ariane-5 launcher software

Abstract

We present the modeling and validation experiments performed with the IFx validation toolset and with the UML profile developed within the IST Omega project, on a representative space vehicle control system: a model of the Ariane-5 flight software obtained by reverse engineering.
The goal of the study is to verify functional and scheduling-related requirements under different task architecture assumptions.

[download]

Bibtex reference

Using an UML profile for timing analysis with the IF validation tool-set

[download]

Bibtex reference

MARTES - Specification and Validation of Real-time and Embedded Systems, workshop overview

Abstract

This paper presents an overview on the workshop on Modelling and Analysis of Real-TIme Embedded systems that is a follow-up workshop of the previous SVERTS and SIVOES workshops, that took place with the Models/UML 2005 conference. The main themes discussed at this years workshop concerned modelling for validation and profiles for real-time.

[download]

Bibtex reference

Timing analysis and validation of the embedded MARS bus manager

Abstract

This paper presents a case study in UML-based modelling and validation of the intricate timing aspects arising in a small but complex component of the airborne Medium Altitude Reconaissance System produced by NLR. The purpose is to show how automata-based timing analysis and verification tools can be used by field engineers for solving isolated hard points in a complex real-time design, even if the press-button verification of entire systems remains a remote goal. We claim that the accessibility of such tools is largely improved by the use of a UML profile with intuitive features for modeling timing and related properties.

[download]

Bibtex reference

COTS Component-Based Embedded Systems - A Dream or Reality?

Abstract

[download]

Bibtex reference

Time in Abstract State Machines

Abstract

State machines are considered a very general means of expressing computations in an implementation-independent way. There are also ways to extend the general state machine framework with distribution aspects. However, there is still no agreement when it comes to handling time in this framework. In this article we take a look at existing ways to enhance state machine frameworks. Based on this we propose a general framework of time extensions for state machines, which we relate to existing approaches. Our work is mainly based on time approaches for ASM, because ASM are considered a very general state machine model. Taking this into account, our approach is valid for state-transition systems in general.

[download]

Bibtex reference

SVERTS - Specification and Validation of Real-time and Embedded Systems, workshop overview

Abstract

This paper presents an overview on the workshop on Specification and Validation of Real-time and embedded Systems that has taken place for the second time in association with the UML 2004 conference. The main themes discussed at this years workshop concerned modeling of real-time features with the perspective of validation as well as some particular validation issues.

[download]

Bibtex reference

The IF toolset

Abstract

This paper presents an overview on the IF toolset which is an environment for modelling and validation of heterogeneous real-time systems. The toolset is built upon a rich formalism, the IF notation, allowing structured automata-based system representations. Moreover, the IF notation is expressive enough to support real-time primitives and extensions of high-level modelling languages such as SDL and UML by means of structure preserving mappings.
The core part of the IF toolset consists of a syntactic transformation component and an open exploration platform. The syntactic transformation component provides language level access to IF descriptions and has been used to implement static analysis and optimisation techniques. The exploration platform gives access to the graph of possible executions. It has been connected to different state-of-the-art model-checking and test-case generation tools.
A methodology for the use of the toolset is presented at hand of a case study concerning the Ariane-5 Flight Program for which both an SDL and a UML model have been validated.

[download]

Bibtex reference

How useful is the UML real-time profile SPT without Semantics?

Abstract

In this position paper we argue that the present practise in UML, consisting in standardising notations only at the level of abstract syntax (meta-model) is in particular in the context of real-time embedded systems, and thus the SPT profile, hindering the usefulness of the standard. A standard should make possible exchange of (parts of) models, and this is clearly not the case today. We argue that the real-time profile that we have defined in the context of the OMEGA project, can provide a basis for the semantic definition of any real-time profile. Also, the translation of the operational part of UML into IF, based on the use of priorities, can be mimicked for providing a means to define any particular execution semantics in UML.

[download]

Bibtex reference

A Framework for Time in FDTs

Abstract

An improved version is available at [GP05].

Bibtex reference

Correct Development of Embedded Systems

Abstract

This paper provides an overview on the approach of the IST OMEGA project for the development of correct software for embedded systems based on the use of UML as modelling language. The main contributions of the project are the definition of a useful subset of UML and some extensions, a formal dynamic semantics integrating all notations and a tool set for the validation of models based on this semantics

[download]

Bibtex reference

IF Tutorial

Abstract

This provided a tutorial on the IF language and on the detailed architecture of the IF verification toolset, as well as detailed descriptions of the translators and verification algorithms.

Bibtex reference

Model Checking of UML Models via a Mapping to Communicating Extended Timed Automata

Abstract

We present a technique and a tool for model-checking operational UML models based on a mapping of object oriented UML models into a framework of communicating extended timed automata - in the IF format - and the use of the existing model-checking and simulation tools for this format. We take into account most of the structural and behavioural characteristics of classes and their interplay and tackle issues like the combination of operations, state machines, inheritance and polymorphism, with a particular semantic profile for communication and concurrency. The UML dialect considered here, also includes a set of extensions for expressing timing. Our approach is implemented by a tool importing UML models via an XMI repository, and thus supporting several commercial and non-commercial UML editors. For user friendly interactive simulation, an interface has been built, presenting feedback to the user in terms of the original UML model. Model-checking and model exploration can be done by reusing the existing IF state-of-the-art validation environment.

[download]

Bibtex reference

Validating Timed UML models by simulation and verification

Abstract

A more recent and complete version of this paper is [OGO05].

Bibtex reference

Timed annotations in UML

Abstract

A more recent and complete version of this paper is [GOO05].

Bibtex reference

Abstraction as the Key for Invariant Verification

Abstract

We present a methodology for constructing abstractions and refining them by analyzing counter-examples. We also present a uniform verification method that combines abstraction, model-checking and deductive verification. In particular, we show how to use the abstract system in a deductive proof even when the abstract model does not satisfy the specification but simulates the concrete system with respect to a weaker notion of simulation than Milner's.

[download]

Bibtex reference

A Real-time profile for UML and how to adapt it to SDL

Abstract

This paper presents work of the IST project OMEGA, where we have defined a UML profile for real-time compatible with the Profile for Performance, Scheduling and Real-time accepted recently at OMG. In contrast to this OMG profile, we put emphasis on semantics and on its use in the context of timed analysis of real-time embedded systems. The defined profile is compatible with the time concepts existing in SDL, and we show how we can adapt also those notations to SDL and MSC which do not yet exist in these ITU languages. We analyze also the possibilities of validation of systems using the profile which is used as guide for the definition of subsets allowing different validation approaches.

[download]

Bibtex reference

Expression of time and duration constraints in SDL

Abstract

In this paper, we give an overview on time related features, useful in the context of real-time system design using the SDL design language. We classify them into two categories, those needed for modelling of non-functional aspects and analysis, and those needed for functional design.
We are careful to allow a clear distinction between functional and non functional parts of specifications. We show how these features are represented at the semantic level with a minimal number of primitives. We discusses a possible semantic framework for time annotaded SDL designs, compatible with the ASM semantics of SDL 2000.

[download]

Bibtex reference

IF-2.0: A Validation Environment for Component-Based Real-Time Systems

Abstract

The paper presents the new version of the IF language and validation environment.
The main new features of the language concern the ability to describe dynamic architures by means of concepts for dynamic creation and distruction of processes and communication channels, hierarchical states and a simplification of the action structure, allowing in particular the inclusion of external code.
The main changes in the toolset concern the exploration engine, generating the semantic model: each process or signalroute is represented as an object with an internal state and a set of fireable(local) transitions, depending on its current state (where Time is a specialised process dealing with the management of all (running) clocks). Coordination is realised by a process manager which scans the set of local transitions, chooses the fireable one(s) with respect to global (system) constraints, askd the corresponding processes to execute these transitions and updated the global state accordingly.

[download]

Bibtex reference

Automated validation of distributed software using the IF environment

Abstract

Bibtex reference

Automated validation of distributed software using the IF environment

Abstract

This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools can cover by itself the whole validation process. The IF environment was built upon an expressive intermediate language and allows to connect several validation tools, providing most of the advanced techniques currently available. The results obtained on several large case-studies, including telecommunication protocols and embedded software systems, confirm the practical interest of this approach.

[download]

Bibtex reference

Timed Extensions for SDL

Abstract

In this paper we propose some extensions necessary to enable the specification and description language SDL to become an appropriate formalism for the design of real-time and embedded systems. The extensions we envisage concern both roles of SDL: First, in order to make SDL a real-time specification language, allowing to correctly simulate and verify real-time specifications, we propose a set of annotations to express in a flexible way assumptions and assertions on timing issues such as execution durations, communication delays, or periodicity of external inputs. Second, in order to make SDL a real-time design language, several useful real-time programming concepts are missing. In particular we propose to extend the basic SDL timer mechanism by introducing new primitives such as cyclic timers, interruptive timers, and access to timer value. All these extensions relies on a clear and powerful time semantics for SDL, which extends the current one, and which is based on timed automata with urgencies.

[download]

Bibtex reference

Verification Experiments on the Mascara Protocol

Abstract

In this paper, we describe a case study on the verification of a real industrial protocol for wireless ATM, called MASCARA. Several tools have been used: SDL has been chosen as the specification language and the commercial tool ObjectGeode has been used for creating and maintaining SDL descriptions. The IF tool-set has been used for generation, minimization and comparison of system models and verification of expected properties. All specification and verification tools are connected via the IF language, which has been defined as an intermediate representation for timed asynchronous systems as well as an open validation environment. Due to the complexity of the protocol, static analysis techniques, such as live variable analysis and program slicing, were the key to the success of this case study. The results obtained give some hints concerning a methodology for the formal verification of real systems.

[download]

Bibtex reference

IF: A Validation Environment for Timed Asynchronous Systems

Abstract

This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools can cover by itself the whole validation process. The IF environment was built upon an expressive intermediate language and allows to connect several validation tools, providing most of the advanced techniques currently available. The results obtained on several large case-studies, including telecommunication protocols and embedded software systems, confirm the practical interest of this approach.

[download]

Bibtex reference

SDL for Real Time: What is missing?

Abstract

This paper provides an overview on the main weaknesses of SDL for the development of real-time sysstems, both on the programming and on the specification side. In particular the fact that according to the standard time progress is totally external and forbids control over time progress is a real hindernis for verification. For this reason, we propose to introduce in SDL the time concepts of timed automata with urgency. We illustrate our proposal by means of a small but realistic example, and show the relationships to several other proposals.

[download]

Bibtex reference

IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems

Abstract

We present work of a project for the improvement of a specification/validation toolbox integrating a commercial toolset ObjectGeode and different validation tools such as the verification tool CADP and the test sequence generator TGV. The intrinsic complexity of most protocol specifications lead us to study combination of other techniques such as static analysis and abstraction together with the classical model-checking techniques. Experimentation and validation of our results in this context motivated the development of an intermediate representation for SDL called IF. In this intermediate representation, a system is represented as a set of timed automata communicating asynchronously through a set of buffers or by rendez-vous through a set of synchronization gates. The advantage of the use of such a program level intermediate representation is that it is easier to interface with various existing tools, such as static analysis, abstraction and compositional state space generation. Moreover, it allows to define for SDL different, but mathematically sound, notions of time.
The purpose of this paper is to show that the intermediate representation IF can serve as a basis for the interconnections of various tools with different input languages into a unified validation framework.

[download]

Bibtex reference

IF: An Intermediate Representation for SDL and its Applications

Abstract

We present work of a project for the improvement of a specification/validation toolbox integrating a commercial toolset ObjectGeode and different validation tools such as the verification tool CADP and the test sequence generator TGV. The intrinsic complexity of most protocol specifications lead us to study combination of other techniques such as static analysis and abstraction together with the classical model-checking techniques. Experimentation and validation of our results in this context motivated the development of an intermediate representation for SDL called IF. In this intermediate representation, a system is represented as a set of timed automata communicating asynchronously through a set of buffers or by rendez-vous through a set of synchronization gates. The advantage of the use of such a program level intermediate representation is that it is easier to interface with various existing tools, such as static analysis, abstraction and compositional state space generation. Moreover, it allows to define for SDL different, but mathematically sound, notions of time.
The purpose of this paper is to show that the intermediate representation IF can serve as a basis for studying semantics of time extensions of SDL.

[download]

Bibtex reference

Construction of abstract state graphs with PVS

Abstract

In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the PVS theorem prover, called predicate abstraction. Given a parallel composition of sequential processes and predicates P1 ... Pn on the program variables defining an abstract domain, we construct an abstract state graph, starting in the state defined by the values of the predicates P1 ... Pn in the initial state. The possible successors of a state are computed using the PVS theorem prover by verifying for each i if Pi or not Pi is a postcondition of it. This allows an abstract state space exploration for arbitrary programs. Using this method, we have automatically verified a bounded retransmission protocol which cannot be proved using backward analysis without providing strong auxiliary invariants.

[download]

Bibtex reference

Verifying invariants using theorem proving

Abstract

Our goal is to use a theorem prover in order to verify invariance properties of distributed systems in a model checking like manner. A system S is described by a set of sequential components, each one given by a transition relation and a predicate Init defining the set of initial states. In order to verify that P is an invariant of S, we try to compute, in a model checking like manner, the weakest predicate P' stronger than P and weaker than Init which is an inductive invariant, that is, whenever P' is true in some state, then P' remains true after the execution of any possible transition. The fact that P is an invariant can be expressed by a set of predicates (having no more quantifiers than P) on the set of program variables, one for every possible transition of the system. In order to prove these predicates, we use either automatic or assisted theorem proving depending on their nature.
We show in this paper how this can be done in an efficient way using the Prototype Verification System PVS. A tool implementing this verification method is presented.

[download]

Bibtex reference

Verification of a distributed Cache memory by using abstractions

Abstract

The contribution of the paper is two-fold. We give a set of properties expressible as temporal logic formulas such that any system satisfying them is a sequentially consistent memory, and which is sufficiently precise such that every reasonnable concrete system implementing a sequentially consistent memory satisfies these properties.
Then, we verify these properties on a particular distributed cache memory systems by means of a verification method, based on the use of abstract interpretation which has been presented in previous papers ([LBBGS95]) and often applied to finite state systems. The motivation of this paper was to show that it can also been applied to systems with infinite state space, and a more recent papers shows that the method can even be automatized ([GS97])

[download]

Bibtex reference

A tool for symbolic program verification and abstraction

Abstract

We give the description of a verification tool taking boolean programs of guarded commands as input; internal representation of programs are sets of Binary Decision Diagrams (BDD) (one for each guarded command). It allows to construct an abstract program of the same form obtained using an abstraction relation given by a boolean expression on ``concrete'' and ``abstract'' variables. The tool allows the verification of CTL formulas on programs. We illustrate its possibilities on an example.

[download]

Bibtex reference

Program Verification using compositional Abstraction

Abstract

In this paper we describe a method for the obtention of the minimal transition system, representing a communicating system given by a set of parallel processes, avoiding the complexity of the non minimal transition system. We consider minimization with respect to observational equivalence, but the method may be adapted to any other equivalence. An interesting method to achieve this goal is to proceed by stepwise composition and minimization of the components of the system. However, if no precautions are taken, the intermediate state graphs generated by this method may contain a lot of transitions which are impossible in the whole context. We give here a variant of this method which allows to avoid these impossible transitions by taking into account at each composition step a guess of the interface behaviour of the context. This ``interface specification'' must be provided by the user. The method is based on a reduction operator for the composition of a subsystem with its interface specification, which is similar to the parallel operator but introduces undefinedness predicates whereever the interface ``cuts off'' a transition. The parallel operator is defined in a way that these undefinedness predicates disappear again in the full context if and only if the corresponding transition is in fact impossible in the whole system. The efficiency of the method depends in fact on the accuracy with which the designer is able to approximate the possible sequences of the context, but its correctness does not. The proof of the correctness of the method is based on a preorder relation similar to the one defined by Walker.

[download]

Bibtex reference

Delta-4 Architecture Validation

Abstract

Bibtex reference

An Algebra for Boolean Processes

Abstract

This work has been motivated by the study of the S/R-models which allow to represent systems as a set of communicating state machines cooperating through a shared memory. We show that S/R-models can be expressed in terms of a process algebra called Boolean SCCS which is a special case of Milner's SCCS, in the sense that the actions are elements of some boolean algebra. We define for BSSCS an operational and a symbolic semantics modulo strong bisimulation equivalence. A complete axiomatisation of bisimulation and simulation equivalences on this algebra is proposed. Furthermore, we propose a very general renaming operator, and show by means of examples that it allows the definition of abstractions.

[download]

Bibtex reference

Safety for branching Semantics

Abstract

We study in a first part of this paper safety and liveness properties for any given program semantics. We give a topological definition of these properties using a safety preorder. Then, we consider the case of branching time semantics where a program is modeled by a set of infinite computation trees modulo bisimulation. We propose and study a safety preorder for this semantics based on simulation and dealing with silent actions. We focus on regular safety properties and characterize them by both tree-automata and formulas of a branching time logic. We show that verifying safety properties on trees reduces to simulation testing.

[download]

Bibtex reference

Formal Specification and verification of a Network Independent Atomic Multicast Protocol

Abstract

Research on formal description techniques during the last years has revealed new trends on the description of distributed systems. Nevertheless, the application of these techniques to real and complex systems is not straightforward and there are not many case studies in this area. This paper presents an experience in protocol building area, by involving a close interaction between protocol design and formal verification, and shows off its application in the design of a real distributed system: a network independent atomic multicast protocol.

[download]

Bibtex reference

Compositional Minimisation of Finite State Processes

Abstract

In this paper we describe a method for the obtention of the minimal transition system, representing a communicating system given by a set of parallel processes, avoiding the complexity of the non minimal transition system. We consider minimization with respect to observational equivalence, but the method may be adapted to any other equivalence. An interesting method to achieve this goal is to proceed by stepwise composition and minimization of the components of the system. However, if no precautions are taken, the intermediate state graphs generated by this method may contain a lot of transitions which are impossible in the whole context. We give here a variant of this method which allows to avoid these impossible transitions by taking into account at each composition step a guess of the interface behaviour of the context. This interface specification must be provided by the user. The method is based on a reduction operator for the composition of a subsystem with its interface specification, which is similar to the parallel operator but introduces undefinedness predicates whereever the interface cuts off a transition. The parallel operator is defined in a way that these undefinedness predicates disappear again in the full context if and only if the corresponding transition is in fact impossible in the whole system. The efficiency of the method depends in fact on the accuracy with which the designer is able to approximate the possible sequences of the context, but its correctness does not. The proof of the correctness of the method is based on a preorder relation similar to the one defined by Walker.

[download]

Bibtex reference

What are the limits of model checking methods for the verification of real life protocols?

Abstract

Bibtex reference

A Logic for the description of Behaviours and Properties of Concurrent Systems

Abstract

Bibtex reference

An expressive logic for a process algebra with silent actions

Abstract

Bibtex reference

Readiness Semantics for Regular Processes with Silent Actions

Abstract

Bibtex reference

A complete inference system for an algebra of regular acceptance models

Bibtex reference

From synchronization tree logic to acceptance model logic

Abstract

Bibtex reference

A Modal Characterization of Observational Congruence on Finite Terms of CCS

Bibtex reference

Omega Final Project Report

[download]

Bibtex reference

Logiques du temps arborescent pour la spécification et la preuve de programmes

Bibtex reference