Susanne Graf: Selected Publications

• 1. Journal Papers
• 2. Edited Work
• 3. Book Chapters or Collections
• 4. Conference and Workshop Papers
• 5. Technical Reports never or not yet published

Knowledge-based Construction of Distributed Constrained Systems

Abstract

The problem of deriving distributed implementations from global specifications has been extensively studied for a number of application domains. We explore it here from the knowledge perspective: A process may decide to take a local action when it has enough knowledge to do so. Such knowledge may be acquired by communication through primitives available on the platform or by static analysis. In this paper, we want to combine control and distribution, that is, we need to impose some global control constraint on a system executed in a distributed fashion. To reach that goal, we compare two approaches: either build a centralized controlled system, distribute its controller and then implement this controlled system on a distributed platform; or alternatively, directly enforce the control constraint while implementing the distributed system on the platform. We show how to achieve a solution following the second approach and explain why this is a pragmatic and more efficient strategy than the other, previously proposed one.

[download]

Bibtex reference

Achieving distributed control through model checking

Abstract

We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints on concurrent systems. The problem of synthesizing a distributed controller is undecidable in the general case. We thus look at a variant of the synthesis problem that allows adding temporary synchronizations between processes. We calculate when processes can decide autonomously, based on their knowledge, whether to take or block an action so that the global constraint is not violated. The local knowledge of processes may not suffice to control the processes so as to achieve the global constraint without introducing new deadlocks. When individual processes cannot take a decision alone based on their knowledge, one may coordinate several processes to achieve joint knowledge in order to take joint decisions. A fixed coordination among sets of processes may severely degrade concurrency. Therefore, we propose the use of temporary coordinations. Since realizing such coordinations on a distributed platform induces communication overhead, we strive to minimize their number. We show how this framework is applied to the case of synthesizing a distributed controller for enforcing a priority order. Finally, we show that the general undecidability of distributed synthesis without adding synchronization holds even for the particular problem of enforcing a priority order.

[download]

Bibtex reference

Building Distributed Controllers for Systems with Priorities

Abstract

Composition of components by means of multi-party synchronizations and priorities allows specifying properties of systems in a very abstract manner, and are meaningful for many application domains. Such specifications are generally easier to verify than the more concrete ones based on message passing. Synchronizations may introduce deadlocks, whereas priorities do not. In this paper, we propose two algorithms: one which given a specification Sys constructs, if necessary and if possible, a set of priority rules enforcing deadlock freedom. A second algorithm builds a distributed implementation of such a prioritized specification. This second algorithm is presently restricted to binary synchronizations but it differs from comparable algorithms such as alpha-core by the fact that it handles specifications with (global) priorities. We have implemented this algorithm and compared its efficiency with alpha-core in the priorityless case.

Bibtex reference

Meta-models in Europe: Languages, Tools and Applications

Abstract

This article provides an overview of current efforts in Europe for using metamodeling in the integrated development of critical systems such as automotive electronics. It distinguishes between lightweight versus heavyweight approaches, surveys a number of related current European projects, and gives details about the Speeds project to illustrate the role of metamodeling-driven system engineering.

[download]

Bibtex reference

Timing analysis and validation with UML: the case of the embedded MARS bus manager

Abstract

This paper presents a case study in UML-based modeling and validation of the intricate timing aspects arising in a small but complex component of the airborne Medium-Altitude Reconnaissance System produced by the Netherlands National Aerospace Laboratory. 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 an UML profile with intuitive features for modeling timing and related properties. This work has been partially funded by the European OMEGA project (IST-2001-33522). Iulian Ober and Ileana Ober: performed work while at VERIMAG, Grenoble, France. Y. Yushtein: at the moment of writing in National Aerospace Laboratory NLR.

[download]

Bibtex reference

OMEGA -- Correct development of Real Time Embedded Systems

Bibtex reference

Software and architecture modelling with Omega-UML and validation with IF

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

A real-time profile for 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

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

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

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

[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

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

Compositional Minimisation of Finite State Systems using Interface Specifications

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

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

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 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.

[download]

Bibtex reference

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

Bibtex reference

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

Bibtex reference

On Lamport's comparison between linear and branching time logic

Bibtex reference

Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday

[download]

Bibtex reference

Formal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015, Held as Part of the 10th DisCoTec, Grenoble, France, June 2-4, 2015

[download]

Bibtex reference

Joint Proceedings of the 8th International Workshop on Model-based Architecting of Cyber-physical and Embedded Systems and 1st International Workshop on UML Consistency Rules (ACES-MB 2015 \& WUCOR 2015) co-located with ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2015), Ottawa, Canada, September 28, 2015

Bibtex reference

Proceedings of the 7th International Workshop on Model-based Architecting and Construction of Embedded Systems co-located with ACM/IEEE 17th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2014), Valencia, Spain, September 30th, 2014

[download]

Bibtex reference

Proceedings of the 6th International Workshop on Model Based Architecting and Construction of Embedded Systems co-located with ACM/IEEE 16th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2013), Miami, Florida, USA, September 29th, 2013

[download]

Bibtex reference

Design and Validation of Concurrent Systems, 30.08. - 04.09.2009

[download]

Bibtex reference

ACESMB 2008 First International Workshop on Model Based Architecting and Constructing of Embedded Systems, Toulouse, 29/09/2008 - 29/09/2008

[download]

Bibtex reference

6th Symposium on Formal Methods for Components and Objects, October 24-26, 2007, Revised Lectures

[download]

Bibtex reference

5th Symposium on Formal Methods for Components and Objects, November 7-10, 2006, Revised Lectures

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

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

[download]

Bibtex reference

SDL and MSC Workshop SAM 2000

[download]

Bibtex reference

Contract-Based Reasoning for Component Systems with Rich Interactions

[download]

Bibtex reference

Formal Methods for Safe and Secure Computers Systems - BSI Study 875

Bibtex reference

Modeling and Verification of Real Time Systems Using the IF Toolbox

Abstract

This chapter presents an overview on the IF toolset which is an environment for modeling 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 modeling 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 optimization techniques. The exploration platform gives access to the graph of possible executions. It has been connected to different state-of-the-artmodel-checking and test-case generation tools. A methodology for the use of the toolset is presented using a case study concerning the Ariane 5 flight program for which both an SDL and a UML model have been validated

Bibtex reference

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

Bibtex reference

Roadmap: Component based design and Integration platforms

[download]

Bibtex reference

Verification of systems with time-constraints

[download]

Bibtex reference

MIMOS: A Deterministic Model for the Design and Update of Real-Time Systems

Abstract

Inspired by the pioneering work of Gilles Kahn on concurrent systems, we model real-time systems as a network of software components each of which is specified to compute a collection of functions according to given timing constraints. The components communicate with each other and their environment via two types of channels: (1) FIFO queues for buffering data, and (2) Registers for sampling time-dependent data streams from sensors or output streams of other components executed at different rates. We present a fixed-point semantics for this model which shows that each system function of a network computes for a given set of input (timed) streams, a unique (timed) output stream. Thanks to the deterministic semantics, a model-based approach is enabled for not only building systems but also updating them after deployment, allowing model-in-the-loop simulation to verify the complete behaviour of the resulting system.

[download]

Bibtex reference

Contract-Based Quality-of-Service Assurance in Dynamic Distributed Systems

Abstract

To offer an infrastructure for autonomous systems offloading parts of their functionality, dynamic distributed systems must be able to satisfy non-functional quality-of-service (QoS) requirements. However, providing hard QoS guarantees without complex global verification that are satisfied even under uncertain conditions is very challenging. In this work, we propose a contract-based QoS assurance for centralized, hierarchical systems, which requires local verification only and has the potential to cope with dynamic changes and uncertainties.

[download]

Bibtex reference

Models, Mindsets, Meta: The What, the How, and the Why Not?

Bibtex reference

Building Correct Cyber-Physical Systems: Why We Need a Multiview Contract Theory

Abstract

The design and verification of critical cyber-physical systems is based on a number of models (and corresponding analysis techniques and tools) representing different viewpoints such as function, timing, security and many more. Overall correctness is guaranteed by mostly informal, and therefore basic, arguments about the relationship between these viewpoint-specific models. We believe that a more flexible contract-based approach could lead to easier integration, to relaxed assumptions, and consequently to more cost efficient systems while preserving the current modelling approach and its tools.

[download]

Bibtex reference

A Framework for Evaluating Schedulability Analysis Tools

Abstract

There exists a large variety of schedulability analysis tools based on different, often incomparable timing models. This variety makes it difficult to choose the best fit for analyzing a given real-time system. To help the research community to better evaluate analysis tools and their underlying methods, we are developing a framework which consists of (1) a simple language called RTSpec for specifying real-time systems, (2) a tool chain which translates a system specification in RTSpec into an input for various analysis tools, and (3) a set of benchmarks. Our goal is to enable users and developers of schedulability analysis tools to compare such tools systematically, automatically and rigorously.

[download]

Bibtex reference

Timing Verification of an Aerial Video Tracking System Using UPPAAL

[download]

Bibtex reference

Introduction to ACES-MB 2015

Bibtex reference

Distributed Implementation of Constrained Systems based on Knowledge

Bibtex reference

Formal Model Driven Engineering for Space Onboard Software

Abstract

One of the major sources of errors in the development of real time critical embedded software is the misinterpretation of system requirements allocated to the software. These misunderstandings between the system team and the software team may have several sources, but are very often due to the following causes: o Use of ambiguous means to describe the system requirements and the software implementation, leading to different interpretations by the system designers, the software developers and the reviewers.

Bibtex reference

Knowledge for the Distributed Implementation of Constrained Systems

Bibtex reference

Model-based design and distributed implementation of bus arbiter for multiprocessors

Bibtex reference

Distributed Implementation of Systems with Multiparty Interactions and Priorities

Bibtex reference

Contract-Based Reasoning for Component Systems with Complex Interactions

[download]

Bibtex reference

Monitoring Distributed Systems Using Knowledge

[download]

Bibtex reference

Implementing Distributed Controllers for Systems with Priorities

Bibtex reference

Reasoning about Safety and Progress Using Contracts

Bibtex reference

Contract-Based Reasoning about Progress: Application to Resource Sharing in a Network

Bibtex reference

Methods for Knowledge Based Controlling of Distributed Systems

[download]

Bibtex reference

Achieving Distributed Control through Model Checking

Abstract

We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints on concurrent systems. We calculate when processes can decide, autonomously, to take or block an action so that the global constraint will not be violated. When the separate processes cannot make this decision alone, it may be possible to temporarily coordinate several processes in order to achieve sufficient knowledge jointly and make combined decisions. Since the overhead induced by such coordinations is important, we strive to minimize their number, again using model checking. We show how this framework is applied to the design of controllers that guarantee a priority policy among transitions.

[download]

Bibtex reference

A Model-Based Design and Validation Approach with the OMEGA-UML Profile and the IF Toolset

Abstract

Intelligent, embedded systems such as autonomous robots and other industrial systems are becoming increasingly more heterogeneous with respect to the platforms on which they are implemented, and thus the software architecture more complex to design and analyse. In this context, it is important to have well-defined design methodologies which should be supported by (1) high level design concepts allowing to master the design complexity, (2) concepts for the expression of non-functional requirements and (3) analysis tools allowing to verify or invalidate that the system under development will be able to conform to its requirements. We illustrate here such an approach for the design of complex embedded systems on hand of a small case study used as a running example for illustration purposes. We briefly present the important concepts of the OMEGA-RT UML profile, we show how we use this profile in a modelling approach, and explain how these concepts are used in the IFx verification toolbox to integrate validation into the design flow and make scalable verification possible.

Bibtex reference

From Orchestration to Choreography: Memoryless and Distributed Orchestrators

Bibtex reference

Model Based Architecting and Construction of Embedded Systems

Bibtex reference

A Model Transformation Tool for Performance Simulation of Complex UML Models

Abstract

The creation and deployment of a service by a telecommunication operator is a complex activity where functional correctness and performance issues are equally critical. We thus promote a methodology that associates rigorous system definition and performance analysis throughout the entire design process, based on the guaranteed availability of analysis models. In this paper, we report how we applied a Model-Driven Engineering approach to build a tool that supports the methodology. The tool provides automatic and systematic transformations of UML 2 design models of a high degree of complexity to performance models for an industrial simulator. We stress in particular how attempting to build a reliable MDE process required careful design decisions and a thorough preliminary study of syntactic and semantic concerns.

[download]

Bibtex reference

Contract-Based Verification of Hierarchical Systems of Components

Abstract

We investigate contract-based verification of systems composed hierarchically from components by using glue operators from the BIP (Behavior, Interaction, Priority) framework. BIP builds on a clear separation between behavior of components and interaction between them. We extend the BIP framework by representing behaviors of atomic components as modal transition systems (MTSs) rather than LTSs. We introduce a notion of {\it contract} including a {\it structural} part and a {\it behavioral} part. The structural part of a contract $ for an interface $ describes the BIP interaction model $\gamma$ between $ and the environment {Env}$ in which a component $ may be used. The behavioral part of $ consists of two MTSs: an {\it assumption} $ conforming to the interface $, and a {\it guarantee} $ conforming to the interface $. Intuitively, $ -- defined by $(\gamma,B)$, $ a behaviour conforming to $ -- satisfies $ if as long as $ behaves like $, $ behaves like $, where ``behaves like'' is defined with respect to $\gamma$. We explore a framework for compositional verification which decomposes verification of a global contract for a system made of $ components into $ verification problems of local contracts for the components, and refines the local contracts until either satisfaction or violation of the global contract can be proven. We provide several sufficient conditions for dominance between contracts (that is, satisfaction of a set of contracts implies satisfaction of another contract) based on circular reasoning. We also provide a satisfiability condition and an algorithm based on assumption generation to generate or refine contracts.

[download]

Bibtex reference

A Framework for Contract-Based Reasoning: Motivation and Application

Abstract

In addition to the paper in SEFM'2008, we show here several examples of compositional reasoning frameworks presented in the literature, that they can be considered as particular instances of our framework. We consider a contract-based reasoning framework for I/O automata and for modal I/O automata introduced recently by Kim Larsen et al.

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

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 K satisfies a contract (A,G) consisting of an assumption A (constraining the environment) and a guarantee G (constraining K), if its implementation satisfies G in an environment guaranteeing A. The contract (A,G) of a component K dominates a set of inner contracts (Ai,Gi) associated with the components defining it, if the composition -- according to the set of connectors defining K --- 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 consistent because G expresses a safety property of K only, and not of the closed system obtained by composing A and K

[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

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

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

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

[download]

Bibtex reference

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

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

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?

[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

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

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

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

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

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

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

Validating Timed UML models by simulation and verification

Abstract

A more recent and complete version of this paper is published in STTT (see [OGO05]).

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

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

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

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.

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

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

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

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

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

Delta-4 Architecture Validation

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?

Bibtex reference

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

Bibtex reference

Readiness Semantics for Regular Processes with Silent Actions

Bibtex reference

An expressive logic for a process algebra with silent actions

Bibtex reference

A complete inference system for an algebra of regular acceptance models

Bibtex reference

From synchronization tree logic to acceptance model logic

Bibtex reference

A Modal Characterization of Observational Congruence on Finite Terms of CCS

Bibtex reference

MIMOS: A Deterministic Model for the Design and Update of Real-Time Systems

Abstract

Inspired by the pioneering work of Gilles Kahn on concurrent systems, we propose to model timed systems as a network of software components (implemented as real-time processes or tasks), each of which is specified to compute a collection of functions according to given timing constraints. We present a fixed-point semantics for this model which shows that each system function of such a network computes for a given set of (timed) input streams, a deterministic (timed) output stream. As a desired feature, such a network model can be modified by integrating new components for adding new system functions without changing the existing ones. Additionally, existing components may be replaced also by new ones fulfilling given requirements. Thanks to the deterministic semantics, a model-based approach is enabled for not only building systems but also updating them after deployment, allowing for efficient analysis techniques such as model-in-the-loop simulation to verify the complete behaviour of the updated system.

[download]

Bibtex reference

RTLib: A Library of Timed Automata for Modeling Real-Time Systems

Abstract

[download]

Bibtex reference

From Complex UML Models to Systematic Performance Simulation

Abstract

[download]

Bibtex reference

Omega Final Project Report

[download]

Bibtex reference

States and events in the context of timed systems

Bibtex reference

Report on the organisations of ETAPS 2002 in Grenoble

Bibtex reference

Timed Extensions for SDL

Bibtex reference

Coping with Process Identities in Networks of Similar Processes

Bibtex reference

Efficient Automata Encoding of Arithmetic expressions

Bibtex reference

Simulationsmodell für die Studie von Laufzeiten auf Hardware-Ebene

Bibtex reference