# 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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{FMCO-07,
title = \{6th Symposium on Formal Methods for Components and Objects, October 24-26, 2007, Revised Lectures},
editor = \{De Boer, Frank and Bonsangue, Marcello and Graf, Susanne and De Roever, Willem-Paul},
series = \{Lecture Notes in Computer Science},
volume = \{5382},
team = \{DCS},
year = \{2008},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{FMCO-06,
title = \{5th Symposium on Formal Methods for Components and Objects, November 7-10, 2006, Revised Lectures},
editor = \{De Boer, Frank and Bonsangue, Marcello and Graf, Susanne and De Roever, Willem-Paul},
series = \{Lecture Notes in Computer Science},
volume = \{4709},
team = \{DCS},
year = \{2007},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{ATVA-2006,
title = \{Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings},
editor = \{Graf, Susanne and Zhang, Wenhui},
series = \{LNCS},
volume = \{4218},
team = \{DCS},
year = \{2006},
isbn = \{3-540-47237-1},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{FMCO-05,
title = \{4th Symposium on Formal Methods for Components and Objects, revised lectures},
editor = \{De Boer, Frank and Bonsangue, Marcello and Graf, Susanne and De Roever, Willem-Paul},
series = \{Lecture Notes in Computer Science},
volume = \{4111},
team = \{DCS},
year = \{2006},
isbn = \{3-540-36749-7},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{MARTES-06,
title = \{2nd workshop on Modelling and Analysis of Real-Time Embedded Systems (MARTES 2006)},
editor = \{Gérard, Sébastien and Graf, Susanne and Haugen, Oystein and Ober, Iulian and Selic, Bran},
series = \{Proceedings appeared as Research Report 343 of the university of Oslo},
team = \{DCS},
year = \{2006},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{MARTES-05,
title = \{1st workshop on Modelling and Analysis of Real-Time Embedded Systems (MARTES 2005)},
editor = \{Gérard, Sébastien and Graf, Susanne and Haugen, Oystein and Ober, Iulian and Selic, Bran},
series = \{Online proceedings available at \url{http://www.martes.org/}},
team = \{DCS},
year = \{2005},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{FMCO-04,
title = \{3rd Symposium on Formal Methods for Components and Objects, revised lectures},
editor = \{De Boer, Frank and Bonsangue, Marcello and Graf, Susanne and De Roever, Willem-Paul},
series = \{LNCS Tutorials},
volume = \{3657},
team = \{DCS},
year = \{2005},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{SPIN-04,
title = \{11th International SPIN Workshop on Model Checking of Software, 2004},
editor = \{Graf, Susanne and Mounier, Laurent},
series = \{Lecture Notes in Computer Science},
volume = \{2989},
team = \{DCS},
year = \{2004},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{FMCO-03,
title = \{2nd Symposium on Formal Methods for Components and Objects, revised lectures},
editor = \{De Boer, Frank and Bonsangue, Marcello and Graf, Susanne and De Roever, Willem-Paul},
series = \{LNCS Tutorials},
volume = \{3188},
team = \{DCS},
year = \{2004},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{SVERTS-03,
title = \{1st workshop on Specification and Validation of UML models for Real Time and Embedded Systems (SVERTS 2003)},
editor = \{Graf, Susanne and Haugen, Oystein and Ober, Ileana and Selic, Bran},
series = \{Verimag technical report 2003/10/22},
team = \{DCS},
year = \{2003},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{FMCO-02,
title = \{1st Symposium on Formal Methods for Components and Objects, revised lectures},
editor = \{De Boer, Frank and Bonsangue, Marcello and Graf, Susanne and De Roever, Willem-Paul},
series = \{LNCS Tutorials},
volume = \{2852},
team = \{DCS},
year = \{2003},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{Tacas00,
title = \{Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS2000},
editor = \{Graf, Susanne and Schwartzbach, Michael},
month = \{March},
series = \{LNCS},
volume = \{1785},
team = \{DCS},
year = \{2000},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## SDL and MSC Workshop SAM 2000

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@proceedings\{SAM00,
title = \{SDL and MSC Workshop SAM 2000},
editor = \{Graf, Susanne and Jard, Claude},
month = \{June},
series = \{IMAG Research report series},
team = \{DCS},
year = \{2000},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Achieving distributed control through model checking

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{Graf-Peled-Quinton-FMSD-12,
title = \{Achieving distributed control through model checking},
author = \{Graf, Susanne and Peled, Doron and Quinton, Sophie},
journal = \{Formal Methods in System Design},
number = \{2},
pages = \{263-281},
volume = \{40},
team = \{DCS},
class = \{web,rap},
year = \{2012}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Building Distributed Controllers for Systems with Priorities

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{BenHafaiedhGrafQuinton11,
title = \{Building Distributed Controllers for Systems with Priorities},
author = \{Ben-Hafaiedh, Imene and Graf, Susanne and Quinton, Sophie},
journal = \{J. Log. Algebr. Program.},
number = \{3},
pages = \{194-218},
volume = \{80},
team = \{DCS},
class = \{web,rap},
year = \{2011}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Meta-models in Europe: Languages, Tools and Applications

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{PasseroneBefhaiedGraf*09,
title = \{Meta-models in Europe: Languages, Tools and Applications},
author = \{Passerone, Roberto and Ben-Hafaiedh, Imene and Graf, Susanne and Benveniste, Albert and Cancila, Daniela and Cuccuru, Arnaud and Gérard, Sébastien and Terrier, François and Damm, Werner and Ferrari, Alberto and Mangeruca, Leonardo and Josko, Bernhard and Peikenkamp, Thomas and Sangiovanni-Vincentelli, Alberto L.},
journal = \{IEEE Design \& Test of Computers},
number = \{3},
pages = \{38--53},
volume = \{26},
team = \{DCS},
year = \{2009},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@article\{Graf-Ober-Yushtein-08,
title = \{Timing analysis and validation with {UML}: the case of the embedded {MARS} bus manager},
author = \{Ober, Iulian and Graf, Susanne and Yushtein, Yuri and Ober, Ileana},
journal = \{Innovations in Systems and Software Engineering},
month = \{September},
note = \{or here: http://www-verimag.imag.fr/~graf/PAPERS/GrafOberYushtein-STTT08.pdf},
number = \{3},
volume = \{4},
team = \{DCS},
year = \{2008},
doi = \{DOI: 10.1007/s11334-008-0066-z, Published online: 23 August 2008},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## OMEGA -- Correct development of Real Time Embedded Systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{Graf2008,
title = \{{OMEGA} -- {C}orrect development of Real Time Embedded Systems},
author = \{Graf, Susanne},
journal = \{SoSyM, int. Journal on Software \& Systems Modelling},
note = \{Special Section introduction},
number = \{2},
volume = \{7},
team = \{DCS},
year = \{2008},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{Graf-Ober-2007,
title = \{{Software and architecture modelling with Omega-UML and validation with IF}},
author = \{Graf, Susanne and Ober, Iulian},
journal = \{Génie Logiciel},
number = \{80},
pages = \{21--26},
publisher = \{Hermes},
volume = \{1},
team = \{DCS},
year = \{2007},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Time in Abstract State Machines

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@article\{Graf-Prinz-ASM07,
title = \{Time in {Abstract State Machines}},
author = \{Graf, Susanne and Prinz, Andreas},
journal = \{Fundamentae Informaticae, Special issue on ASM 2005},
number = \{1},
pages = \{143-174},
volume = \{77},
team = \{DCS},
year = \{2007},
class = \{web,rap,time}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## A real-time profile for UML

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@article\{Graf-Ober-STTT-06,
title = \{A real-time profile for {UML}},
author = \{Graf, Susanne and Ober, Ileana and Ober, Iulian},
journal = \{STTT, Software Tools for Technology Transfer},
month = \{April},
number = \{2},
volume = \{8},
team = \{DCS},
year = \{2006},
doi = \{10.1007/s10009-005-0219-x},
class = \{web,rap,time}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Validating Timed UML models by simulation and verification

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@article\{Graf-Ober-STTT-06b,
title = \{Validating Timed {UML} models by simulation and verification},
author = \{Graf, Susanne and Ober, Ileana and Ober, Iulian},
journal = \{STTT, Software Tools for Technology Transfer},
month = \{April},
number = \{2},
volume = \{8},
team = \{DCS},
year = \{2006},
doi = \{10.1007/s10009-005-0205-x},
class = \{web,rap,time}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### 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)

### Bibtex reference

@article\{Graf-SVERTS-intro05,
title = \{Specification and Validation of Models of Real Time and Embedded Systems in UML},
author = \{Graf, Susanne and Ober, Ileana and Haugen, Oystein and Selic, Bran},
journal = \{STTT, Software Tools for Technology Transfer, a special issue on the SVERTS 2003 workshop},
month = \{April},
note = \{http://www-verimag.imag.fr/~graf/PAPERS/GHOS-Sverts03-05.pdf},
number = \{2},
volume = \{8},
team = \{DCS},
year = \{2006},
doi = \{10.1007/s10009-005-0220-y},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{OberGrafLesens05,
title = \{Un profile {UML} et un outil pour la modélisation et la validation de systèmes temps-réel},
author = \{Ober, Iulian and Graf, Susanne and Ober, Ileana and Lesens, David},
journal = \{Numéro spécial du journal Génie Logiciel consacré à la Journée NEPTUNE 05 : Ingénierie des Modèles - vérification de modèles},
month = \{May},
pages = \{33-38},
volume = \{73},
team = \{DCS},
year = \{2005},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@article\{STTT-Tacas-2000,
title = \{{Tools and Algorithms for the Construction and Analysis of Systems: An STTT special section}},
author = \{Graf, Susanne},
journal = \{STTT, Software Tools for Technology Transfer},
month = \{February},
note = \{Introduction to Special Section for TACAS 2000},
number = \{2},
volume = \{4},
team = \{DCS},
year = \{2003},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### 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]).

### Bibtex reference

@article\{Graf94a,
title = \{Characterization of a sequentially consistent memory and verification of a cache memory by abstraction},
author = \{Graf, Susanne},
journal = \{Distributed Computing},
note = \{accepted for publication without any further revision since 1995},
publisher = \{Springer Verlag},
volume = \{12},
team = \{DCS},
year = \{1999},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Compositional Minimisation of Finite State Systems using Interface Specifications

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@article\{GrafLuttgenSteffen96,
title = \{Compositional Minimisation of Finite State Systems using Interface Specifications},
author = \{Graf, Susanne and Lüttgen, Gerald and Steffen, Bernhard},
journal = \{Formal Aspects of Computation},
note = \{appeared as Passauer Informatik Bericht MIP-9505},
volume = \{8},
team = \{DCS},
year = \{1996},
class = \{web,rap,abs}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Property Preserving Abstractions for the Verification of Concurrent Systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@article\{LoiseauxGrafSifakisBouajjaniBensalem94,
title = \{Property Preserving Abstractions for the Verification of Concurrent Systems},
author = \{Loiseaux, Claire and Graf, Susanne and Sifakis, Joseph and Bouajjani, Ahmed and Bensalem, Saddek},
journal = \{Formal Methods in System Design},
month = \{January},
volume = \{6},
issue = \{1},
team = \{DCS},
year = \{1995},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@article\{GrafSifakis86a,
title = \{A Logic for the Description of non Deterministic Programs and their Properties},
author = \{Graf, Susanne and Sifakis, Joseph},
journal = \{Information and Control},
pages = \{1--3},
volume = \{68},
team = \{DCS},
year = \{1986},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## A Modal Characterization of Observational Congruence on Finite Terms of CCS

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@article\{GrafSifakis86b,
title = \{A Modal Characterization of Observational Congruence on Finite Terms of {CCS}},
author = \{Graf, Susanne and Sifakis, Joseph},
journal = \{Information and Control},
pages = \{1--3},
volume = \{68},
team = \{DCS},
year = \{1986},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{GrafSifakis86c,
title = \{A logic for the specification and proof of regular controllable processes of {CCS}},
author = \{Graf, Susanne and Sifakis, Joseph},
journal = \{Acta Informatica},
pages = \{507--527},
volume = \{23},
team = \{DCS},
year = \{1986},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{GrafSifakis85b,
title = \{A logic for the specification and proof of regular controllable processes of {CCS}},
author = \{Graf, Susanne and Sifakis, Joseph},
booktitle = \{Logics and Models of Concurrent Systems},
journal = \{NATO ASI Series F, Vol. 13, Springer Verlag},
team = \{DCS},
year = \{1985},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## On Lamport's comparison between linear and branching time logic

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@article\{graf84b,
title = \{On {L}amport's comparison between linear and branching time logic},
author = \{Graf, Susanne},
journal = \{RAIRO Informatique Théorique},
number = \{4},
volume = \{18},
team = \{DCS},
year = \{1984},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Modeling and Verification of Real Time Systems Using the IF Toolbox

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@incollection\{Bozga-Graf-Mounier-Ober-07,
title = \{Modeling and Verification of Real Time Systems Using the {IF} Toolbox},
author = \{Bozga, Marius and Graf, Susanne and Mounier, Laurent and Ober, Iulian},
booktitle = \{Real Time Systems 1: Modeling and verification techniques},
editor = \{Navet, Nicolas},
chapter = \{9},
publisher = \{Hermes, Lavoisier},
series = \{Traité IC2, série Informatique et systèmes d'information},
volume = \{1},
team = \{DCS},
year = \{2008},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@incollection\{BozgaGrafMounierOber-Hermes06,
title = \{La boîte à outils {IF} pour la modélisation et la vérification de systèmes temps réel},
author = \{Bozga, Marius and Graf, Susanne and Mounier, Laurent and Ober, Iulian},
editor = \{Navet, Nicolas},
booktitle = \{Systèmes temps réel : techniques de description et de vérification},
chapter = \{9},
publisher = \{Hermes, Lavoisier},
series = \{Traité IC2, série Informatique et systèmes d'information},
volume = \{1},
team = \{DCS},
year = \{2006},
class = \{web, rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Roadmap: Component based design and Integration platforms

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

title = \{Roadmap: Component based design and Integration platforms},
author = \{Jonsson, Bengt and Brinksma, Ed and Coulson, Geoff and Graf, Susanne and Crnkovic, Ivica and Gérard, Sébastien and Hermanns, Holger and Jezequel, Jean-Marc and Ravn, Anders and Schnoebelen, Philippe and Terrier, François and Votintseva, Angelika},
editor = \{Sifakis, Joseph and Bouyssounouse, Bruno},
booktitle = \{Embedded Systems Design: The ARTIST Roadmap for Research and Development},
publisher = \{Springer},
series = \{LNCS},
volume = \{3436},
team = \{DCS},
year = \{2005},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Verification of systems with time-constraints

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@incollection\{GrafRichierVoiron91,
title = \{Verification of systems with time-constraints},
author = \{Graf, Susanne and Richier, Jean-Luc and Voiron, Jacques},
booktitle = \{Delta-4 Architecture Guide'', collection ESPRIT},
publisher = \{Springer Verlag},
team = \{DCS},
year = \{1991},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{BenHafaiedhGrafJaber-ICECS-11,
title = \{Model-based design and distributed implementation of bus arbiter for multiprocessors},
author = \{Ben-Hafaiedh, Imene and Graf, Susanne and Jaber, Mohamad},
booktitle = \{18th IEEE International Conference on Electronics, Circuits and Systems, ICECS 2011, Beirut, Lebanon, December 11-14, 2011},
pages = \{65-68},
publisher = \{IEEE},
team = \{DCS},
class = \{web,rap},
year = \{2011},
isbn = \{978-1-4577-1845-8}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Distributed Implementation of Systems with Multiparty Interactions and Priorities

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{BenHafaiedhGrafMazouz-SEFM-11,
title = \{Distributed Implementation of Systems with Multiparty Interactions and Priorities},
author = \{Ben-Hafaiedh, Imene and Graf, Susanne and Mazouz, Nejla},
editor = \{Barthe, Gilles and Pardo, Alberto and Schneider, Gerardo},
booktitle = \{Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings},
pages = \{38-57},
publisher = \{Springer},
series = \{Lecture Notes in Computer Science},
volume = \{7041},
team = \{DCS},
class = \{web,rap},
year = \{2011},
isbn = \{978-3-642-24689-0}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Contract-Based Reasoning for Component Systems with Complex Interactions

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafPasseroneQuinton11,
title = \{Contract-Based Reasoning for Component Systems with Complex Interactions},
author = \{Graf, Susanne and Passerone, Roberto and Quinton, Sophie},
booktitle = \{TIMOBD'11},
team = \{DCS},
class = \{web,rap},
year = \{2011}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Monitoring Distributed Systems Using Knowledge

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafPeledQuinton11,
title = \{Monitoring Distributed Systems Using Knowledge},
author = \{Graf, Susanne and Peled, Doron and Quinton, Sophie},
editor = \{Bruni, Roberto and Dingel, Jürgen},
booktitle = \{Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference, FORTE 2011, Reykjavik, Iceland, June 6-9, 2011.},
pages = \{183-197},
publisher = \{Springer},
series = \{Lecture Notes in Computer Science},
volume = \{6722},
team = \{DCS},
class = \{web,rap},
year = \{2011},
isbn = \{978-3-642-21460-8}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Implementing Distributed Controllers for Systems with Priorities

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{BenHafaiedhGrafKhairallah-Foclasa10,
title = \{Implementing Distributed Controllers for Systems with Priorities},
author = \{Ben-Hafaiedh, Imene and Graf, Susanne and Khairallah, Hammadi},
booktitle = \{Proceedings Ninth International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA},
pages = \{31-46},
series = \{EPTCS},
volume = \{30},
team = \{DCS},
class = \{web,rap},
year = \{2010},
doi = \{http://dx.doi.org/10.4204/EPTCS.30.3}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Reasoning about Safety and Progress Using Contracts

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{BenHafaiedhGrafQuinton-Ifcem10,
title = \{Reasoning about Safety and Progress Using Contracts},
author = \{Ben-Hafaiedh, Imene and Graf, Susanne and Quinton, Sophie},
editor = \{Dong, Jin Song and Zhu, Huibiao},
booktitle = \{Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings},
pages = \{436-451},
publisher = \{Springer},
series = \{Lecture Notes in Computer Science},
volume = \{6447},
team = \{DCS},
class = \{web,rap},
year = \{2010},
doi = \{http://dx.doi.org/10.1007/978-3-642-16901-4_29}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{BenhfaiedhGrafQuinton-Flacos10,
title = \{Contract-Based Reasoning about Progress: Application to Resource Sharing in a Network},
author = \{Ben-Hafaiedh, Imene and Graf, Susanne and Quinton, Sophie},
booktitle = \{Proc. of FLACOS'10},
team = \{DCS},
class = \{web,rap},
year = \{2010}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Methods for Knowledge Based Controlling of Distributed Systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{BensalemBozgaGraf*ATVA10,
title = \{Methods for Knowledge Based Controlling of Distributed Systems},
author = \{Bensalem, Saddek and Bozga, Marius and Graf, Susanne and Peled, Doron and Quinton, Sophie},
editor = \{Bouajjani, Ahmed and Chin, Wei-Ngan},
booktitle = \{Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings},
pages = \{52-66},
publisher = \{Springer},
series = \{Lecture Notes in Computer Science},
volume = \{6252},
team = \{DCS},
class = \{web,rap},
year = \{2010},
isbn = \{978-3-642-15642-7}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Achieving Distributed Control through Model Checking

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafPeledQuinton-CAV10,
title = \{Achieving Distributed Control through Model Checking},
author = \{Graf, Susanne and Peled, Doron and Quinton, Sophie},
editor = \{Touili, Tayssir and Cook, Byron and Jackson, Paul},
booktitle = \{Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
pages = \{396-409},
publisher = \{Springer},
series = \{Lecture Notes in Computer Science},
volume = \{6174},
team = \{DCS},
class = \{web,rap},
year = \{2010},
doi = \{http://dx.doi.org/10.1007/978-3-642-14295-6_35}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@inproceedings\{BenfhaiedConstantGrafRobbana09,
title = \{A Model-Based Design and Validation Approach with the {OMEGA-UML} Profile and the {IF} Toolset},
author = \{Ben-Hafaiedh, Imene and Constant, Olivier and Graf, Susanne and Robbana, Riadh},
booktitle = \{2nd Mediterranean Conference on Intelligent Systems and Automation, CISA 2009, March 23-25, Zarzis, Tunesia},
publisher = \{American Institut of Physics},
series = \{AIP Conference Proceedings},
volume = \{1107},
team = \{DCS},
year = \{2009},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## From Orchestration to Choreography: Memoryless and Distributed Orchestrators

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{BenhfaiedhGrafQuinton-Flacos09,
title = \{From Orchestration to Choreography: Memoryless and Distributed Orchestrators},
author = \{Quinton, Sophie and Ben-Hafaiedh, Imene and Graf, Susanne},
booktitle = \{Proc. of FLACOS'09},
team = \{DCS},
class = \{web,rap},
year = \{2009}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Model Based Architecting and Construction of Embedded Systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{ObVaGrFiWe2008,
title = \{Model Based Architecting and Construction of Embedded Systems},
author = \{Ober, Iulian and Baelen, Stefan Van and Graf, Susanne and Filali, Mamoun and Weigert, Thomas and Gérard, Sébastien},
editor = \{Chaudron, Michel},
booktitle = \{Models in Software Engineering, Workshops and Symposia at MODELS 2008, Toulouse, France, September 28 - October 3, 2008. Reports and Revised Selected Papers},
pages = \{1--4},
publisher = \{Springer},
series = \{Lecture Notes in Computer Science},
volume = \{5421},
team = \{DCS},
year = \{2009},
isbn = \{978-3-642-01647-9},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## A Model Transformation Tool for Performance Simulation of Complex UML Models

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{ConstantMoninGraf08,
title = \{A Model Transformation Tool for Performance Simulation of Complex {UML} Models},
author = \{Constant, Olivier and Monin, Wei and Graf, Susanne},
booktitle = \{ICSE 2008, tool track},
note = \{complete technical report at http://www-verimag.imag.fr/Rapports-Techniques,28.html&lang=en},
publisher = \{ACM},
volume = \{ICSE Companion},
team = \{DCS},
year = \{2008},
isbn = \{978-1-60558-079-1},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Contract-Based Verification of Hierarchical Systems of Components

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{QuintonGraf08,
title = \{Contract-Based Verification of Hierarchical Systems of Components},
author = \{Quinton, Sophie and Graf, Susanne},
booktitle = \{6th IEEE Int. Conferences on Software Engineering and Formal Methods, SEFM08, Cape Town, South Africa, 10-14 November 2008},
pages = \{377-388},
publisher = \{IEEE Computer Society Press},
team = \{DCS},
year = \{2008},
isbn = \{978-0-7695-3437-4},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## A Framework for Contract-Based Reasoning: Motivation and Application

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@inproceedings\{QuintonGraf08b,
title = \{A Framework for Contract-Based Reasoning: Motivation and Application},
author = \{Quinton, Sophie and Graf, Susanne},
booktitle = \{Second Workshop on Formal Languages and Analysis of Contract-Oriented Software, FLACOS, Malta, november 2008},
team = \{DCS},
year = \{2008},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## An Approach to Modeling and Verification of Component Based Systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GoesslerGrafMila*07,
title = \{An Approach to Modeling and Verification of Component Based Systems},
author = \{Gössler, Gregor and Graf, Susanne and Majster-Cederbaum, Mila and Martens, Moritz and Sifakis, Joseph},
booktitle = \{Current Trends in Theory and Practice of Computer Science, SOFSEM'07},
series = \{LNCS},
volume = \{4362},
team = \{DCS},
year = \{2007},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Contracts for BIP: hierarchical interaction models for compositional verification

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GrafQuinton-07,
title = \{Contracts for {BIP}: hierarchical interaction models for compositional verification},
author = \{Graf, Susanne and Quinton, Sophie},
booktitle = \{FORTE 2007, Talinn},
note = \{invited presentation},
series = \{LNCS},
volume = \{4574},
team = \{DCS},
year = \{2007},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Qualification d'architectures fontionnelles

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BozgaCombesGraf*06,
title = \{Qualification d'architectures fontionnelles},
author = \{Bozga, Marius and Combes, Pierre and Graf, Susanne and Monin, Wei and Moteau, Nicolas},
booktitle = \{Notere'06},
team = \{DCS},
year = \{2006},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GerardGrafHaugenOberSelic-Martes-06,
title = \{{MARTES} - {Modelling and Analysis of Real Time and Embedded Systems Using UML}},
author = \{Graf, Susanne and Gérard, Sébastien and Haugen, Oystein and Ober, Iulian and Selic, Bran},
booktitle = \{MoDELS 2006 International Workshops, Doctoral Symposium, Educators Symposium; Genoa, October 2006, Revised Selected Papers},
series = \{LNCS},
volume = \{4364},
team = \{DCS},
year = \{2006},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Ensuring Properties of Interaction Systems by Construction

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GoesslerGrafMila*06,
title = \{Ensuring Properties of Interaction Systems by Construction},
author = \{Gössler, Gregor and Graf, Susanne and Majster-Cederbaum, Mila and Martens, Moritz and Sifakis, Joseph},
booktitle = \{Program Analysis and Compilation, Theory and Practice},
series = \{LNCS},
volume = \{4444},
team = \{DCS},
year = \{2006},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafOberYushtein06,
title = \{Using an {UML} profile for timing analysis with the {IF} validation tool-set},
author = \{Ober, Iulian and Graf, Susanne and Yushtein, Yuri},
booktitle = \{Proceedings of Model-Based Development of Embedded Systems, MBEES, Dagstuhl, Germany},
month = \{January},
series = \{Technical Report SSE, U. Braunschweig},
volume = \{2006-1},
team = \{DCS},
year = \{2006},
class = \{validation,web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{OberGrafLesens06,
title = \{A case study in {UML} model-based validation: The {Ariane-5} launcher},
author = \{Ober, Iulian and Graf, Susanne and Lesens, David},
booktitle = \{Formal Methods for Open Object-Based Distributed Systems, 8th IFIP WG 6.1 International Conference, FMOODS 2006},
series = \{LNCS},
volume = \{4037},
team = \{DCS},
year = \{2006},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GerardGrafHaugenOberSelic-Martes-05,
title = \{{MARTES} - Specification and Validation of Real-time and Embedded Systems, workshop overview},
author = \{Graf, Susanne and Gérard, Sébastien and Haugen, Oystein and Ober, Iulian and Selic, Bran},
booktitle = \{MoDELS 2005 International Workshops, Doctoral Symposium, Educators Symposium; Montenegro Bay, Jamaica, October 2005, Revised Selected Papers},
series = \{LNCS},
volume = \{3844},
team = \{DCS},
year = \{2005},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Timing analysis and validation of the embedded MARS bus manager

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GrafOberYushtein05,
title = \{Timing analysis and validation of the embedded {MARS} bus manager},
author = \{Ober, Iulian and Graf, Susanne and Yushtein, Yuri},
booktitle = \{Intl Workshop on Modeling and Analysis of Real Time Embedded Systems, MARTES 2005, associated with MoDELS 2005},
month = \{October},
team = \{DCS},
year = \{2005},
class = \{validation,web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## COTS component-Based Embedded Systems - A Dream or Reality?

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{IvicaGraf*05,
title = \{{COTS} component-Based Embedded Systems - {A} Dream or Reality?},
author = \{Crnkovic, Ivica and Axelsson, Jakob and Graf, Susanne and Larsson, Magnus and Ommering, Rob C. van and Wallnau, Kurt C.},
booktitle = \{ICCBSS 2005, Bilbao, January 2005},
series = \{LNCS},
volume = \{3412},
team = \{DCS},
year = \{2005},
class = \{components,rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## IF Tutorial

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@inproceedings\{Bozga-Graf-Mounier-04,
title = \{{IF Tutorial}},
author = \{Bozga, Marius and Graf, Susanne and Mounier, Laurent and Ober, Iulian},
booktitle = \{9th SPIN'04 Workshop on Model-Checking of Software, Barcelona, Spain},
month = \{April},
series = \{Lecture Notes in Computer Science},
volume = \{2989},
team = \{DCS},
year = \{2004},
class = \{time,validation, rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## The IF toolset

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BozgaGrafOberSifakis-SFM-04,
title = \{The {IF} toolset},
author = \{Bozga, Marius and Graf, Susanne and Ober, Iulian and Ober, Ileana and Sifakis, Joseph},
booktitle = \{4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time, SFM-04:RT, Bologna, Sept. 2004},
publisher = \{Springer Verlag},
series = \{LNCS Tutorials},
volume = \{3185},
team = \{DCS},
year = \{2004},
class = \{tools, time, rap, web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Correct Development of Embedded Systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{Graf-Hooman-EWSA-04,
title = \{Correct Development of Embedded Systems},
author = \{Graf, Susanne and Hooman, Jozef},
booktitle = \{European Workshop on Software Architecture: Languages, Styles, Models, Tools, and Applications (EWSA 2004), co-located with ICSE 2004, St Andrews, Scotland},
month = \{May},
series = \{LNCS},
volume = \{3047},
team = \{DCS},
year = \{2004},
class = \{time,web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{Graf-Ober-SIVOES-04,
title = \{How useful is the {UML} real-time profile {SPT} without Semantics?},
author = \{Graf, Susanne and Ober, Ileana},
booktitle = \{Int. workshop SIVOES 2004, associated with RTAS 2004, Toronto Canada},
month = \{April},
note = \{position paper},
team = \{DCS},
year = \{2004},
class = \{time,rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GrafHaugenOberSelic-Sverts-04,
title = \{{SVERTS} - Specification and Validation of Real-time and Embedded Systems, workshop overview},
author = \{Graf, Susanne and Haugen, Oystein and Ober, Ileana and Selic, Bran},
booktitle = \{UML Modeling Languages and Applications, UML 2004 Satellite Activities, Lisbon, Portugal, October 11-15, 2004, Revised Selected Papers},
series = \{LNCS},
volume = \{3297},
team = \{DCS},
year = \{2004},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{OberGraf-04-spin,
title = \{Model Checking of {UML} Models via a Mapping to {Communicating Extended Timed Automata}},
author = \{Ober, Iulian and Graf, Susanne and Ober, Ileana},
booktitle = \{11th International SPIN Workshop on Model Checking of Software, 2004},
series = \{LNCS},
volume = \{2989},
team = \{DCS},
year = \{2004},
class = \{time,validation,rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Abstraction as the Key for Invariant Verification

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BensalemGrafLakhnech03,
title = \{Abstraction as the Key for Invariant Verification},
author = \{Bensalem, Saddek and Graf, Susanne and Lakhnech, Yassine},
editor = \{Dershowitz, Nachum},
booktitle = \{Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday},
pages = \{67-99},
publisher = \{Springer},
series = \{Lecture Notes in Computer Science},
volume = \{2772},
team = \{DCS},
year = \{2003},
isbn = \{3-540-21002-4},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{Graf-Ober-SDL03,
title = \{A Real-time profile for {UML} and how to adapt it to {SDL}},
author = \{Graf, Susanne and Ober, Ileana},
booktitle = \{SDL 2003: System Design, 11th International SDL Forum, Stuttgart, Germany, July 1-4, 2003. Proceedings},
month = \{July},
series = \{LNCS},
volume = \{2708},
team = \{DCS},
year = \{2003},
class = \{web,rap,time}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Validating Timed UML models by simulation and verification

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Abstract

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

### Bibtex reference

@inproceedings\{Graf-Ober-UML03b,
title = \{Validating Timed {UML} models by simulation and verification},
author = \{Ober, Iulian and Graf, Susanne and Ober, Ileana},
booktitle = \{Workshop SVERTS on Specification and Validation of UML models for Real Time and Embedded Systems, a satellite event of UML 2003, San Francisco, October 2003},
month = \{October},
team = \{DCS},
year = \{2003},
class = \{web,rap,time}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BozgaMounierGraf*CAV02,
title = \{{IF-2.0}: A Validation Environment for Component-Based Real-Time Systems},
author = \{Bozga, Marius and Graf, Susanne and Mounier, Laurent},
editor = \{Brinksma, Ed and Larsen, Kim Guldstrand},
booktitle = \{Proceedings of Conference on Computer Aided Verification, CAV'02, Copenhagen},
month = \{June},
pages = \{343 --348},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{2404},
team = \{DCS},
year = \{2002},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Expression of time and duration constraints in SDL

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{Graf-SAM02,
title = \{Expression of time and duration constraints in {SDL}},
author = \{Graf, Susanne},
booktitle = \{3rd SAM Workshop on SDL and MSC, University of Wales Aberystwyth},
month = \{June},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{2599},
team = \{DCS},
year = \{2002},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Automated validation of distributed software using the IF environment

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@inproceedings\{BozgaGrafMounier01,
title = \{Automated validation of distributed software using the {IF} environment},
author = \{Bozga, Marius and Graf, Susanne and Mounier, Laurent},
editor = \{Stoller, Scott D. and Visser, Willem},
booktitle = \{Workshop on Software Model-checking, associated with CAV 2001, Paris},
annote = \{http://www.elsevier.nl/gej-ng/31/29/23/83/34/show/Products/notes/index.htt?-debug=5#007},
month = \{July},
publisher = \{Elsevier Science Publishers},
series = \{Electronic Notes in Theoretical Computer Science},
volume = \{55},
team = \{DCS},
year = \{2001},
issue = \{3},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Automated validation of distributed software using the IF environment

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@inproceedings\{BozgaGrafMounier01b,
title = \{Automated validation of distributed software using the {IF} environment},
author = \{Bozga, Marius and Mounier, Laurent and Graf, Susanne},
booktitle = \{2001 IEEE International Symposium on Network Computing and Applications (NCA 2001)},
month = \{October},
publisher = \{IEEE},
team = \{DCS},
year = \{2001},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Timed Extensions for SDL

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BozgaGrafOber*01,
title = \{Timed Extensions for {SDL}},
author = \{Bozga, Marius and Kerbrat, Alain and Graf, Susanne and Mounier, Laurent and Ober, Iulian and Vincent, Daniel},
booktitle = \{Proceedings of {SDL} {FORUM}'01 (Copenhagen, Denmark)},
month = \{June},
pages = \{223--240},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{2078},
team = \{DCS},
year = \{2001},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Verification Experiments on the Mascara Protocol

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{JiaGraf00a,
title = \{Verification Experiments on the {Mascara} Protocol},
author = \{Graf, Susanne and Jia, Guoping},
booktitle = \{Model Checking Software, 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001, Proceedings},
month = \{May},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{2057},
team = \{DCS},
year = \{2001},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## IF: A Validation Environment for Timed Asynchronous Systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

@inproceedings\{BozgaFernandGhirvu*CAV00,
title = \{{IF}: A Validation Environment for Timed Asynchronous Systems},
author = \{Bozga, Marius and Ghirvu, Lucian and Graf, Susanne and Mounier, Laurent},
editor = \{Emerson, Ernest Allen and Sistla, A. Prasad},
booktitle = \{Proceedings of Conference on Computer Aided Verification, CAV'00, Chicago},
month = \{June},
pages = \{543-547},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{1855},
team = \{DCS},
year = \{2000},
isbn = \{3-540-67770-4},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## SDL for Real Time: What is missing?

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BozgaGrafOber-SAM00,
title = \{{SDL} for {R}eal {T}ime: What is missing?},
author = \{Bozga, Marius and Graf, Susanne and Kerbrat, Alain and Mounier, Laurent and Ober, Iulian and Vincent, Daniel},
booktitle = \{Proceedings of SAM'00: 2nd Workshop on {SDL} and {MSC} (Grenoble, France)},
month = \{June},
pages = \{108 --122},
publisher = \{IMAG},
team = \{DCS},
year = \{2000},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BozgaFernandGhirvu*FM99,
title = \{{IF}: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems},
author = \{Bozga, Marius and Fernandez, Jean-Claude and Ghirvu, Lucian and Graf, Susanne and Krimm, Jean-Pierre and Mounier, Laurent},
booktitle = \{Proceedings of Symposium on Formal Methods 99, Toulouse},
month = \{September},
number = \{1708},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{1708},
team = \{DCS},
year = \{1999},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## IF: An Intermediate Representation for SDL and its Applications

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BozgaFernandGhirvu*SDL99,
title = \{{IF}: An Intermediate Representation for {SDL} and its Applications},
author = \{Bozga, Marius and Fernandez, Jean-Claude and Ghirvu, Lucian and Graf, Susanne and Krimm, Jean-Pierre and Mounier, Laurent and Sifakis, Joseph},
editor = \{Dssouli, Rachida and Bochmann, Gregor and Lahav, Yair},
booktitle = \{Proceedings of SDL Forum 99, Montreal},
month = \{June},
pages = \{138-152},
publisher = \{Elsevier},
team = \{DCS},
year = \{1999},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Construction of abstract state graphs with PVS

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GrafSaidi97,
title = \{Construction of abstract state graphs with {PVS}},
author = \{Graf, Susanne and Saidi, Hassen},
booktitle = \{Conference on Computer Aided Verification CAV'97, Haifa},
month = \{June},
series = \{LNCS},
volume = \{1254},
team = \{DCS},
year = \{1997},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Verifying invariants using theorem proving

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GrafSaidi96,
title = \{Verifying invariants using theorem proving},
author = \{Graf, Susanne and Saidi, Hassen},
booktitle = \{Conference on Computer Aided Verification CAV'96},
month = \{July},
series = \{LNCS},
volume = \{1102},
team = \{DCS},
year = \{1996},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Verification of a distributed Cache memory by using abstractions

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### 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])

### Bibtex reference

@inproceedings\{Graf94,
title = \{Verification of a distributed Cache memory by using abstractions},
author = \{Graf, Susanne},
booktitle = \{Conference on Computer Aided Verification CAV'94, Stanford},
month = \{June},
note = \{a largely improved and extended version appeared in Distributed Computing which is the online version},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{818},
team = \{DCS},
year = \{1994},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Program Verification using compositional Abstraction

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GrafLoiseaux92,
title = \{Program Verification using compositional Abstraction},
author = \{Graf, Susanne and Loiseaux, Claire},
booktitle = \{TAPSOFT 93, joint conference CAAP/FASE},
month = \{April},
publisher = \{LNCS 668, Springer Verlag},
team = \{DCS},
year = \{1993},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## A tool for symbolic program verification and abstraction

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GrafLoiseaux93,
title = \{A tool for symbolic program verification and abstraction},
author = \{Graf, Susanne and Loiseaux, Claire},
booktitle = \{Conference on Computer Aided Verification CAV 93, Heraklion Crete},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{697},
team = \{DCS},
year = \{1993},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Safety for branching Semantics

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BouajjaniFernandezGrafSifakis*90,
title = \{Safety for branching Semantics},
author = \{Bouajjani, Ahmed and Fernandez, Jean-Claude and Graf, Susanne and Sifakis, Joseph and Rodr\'{\i}guez, Carlos},
editor = \{Albert-Leach, Javier and Monien, Burkhard and Rodr\'\iguez-Artalejo, Mario},
booktitle = \{Automata, Languages and Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings},
month = \{July},
pages = \{76-92},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{510},
team = \{DCS},
year = \{1991},
isbn = \{3-540-54233-7},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## An Algebra for Boolean Processes

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{CourcoubetisGrafSifakis91,
title = \{An Algebra for Boolean Processes},
author = \{Courcoubetis, Costas and Graf, Susanne and Sifakis, Joseph},
booktitle = \{Workshop on Computer-Aided Verification CAV'91, Aalborg (Denmark)},
month = \{June},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{575},
team = \{DCS},
year = \{1991},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Delta-4 Architecture Validation

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{KanounArlatBurrillGraf*91,
title = \{Delta-4 Architecture Validation},
author = \{Kanoun, Kamara and Arlat, Jean and Burrill, L. and Crouzet, Yves and Graf, Susanne and Martins, Eliane and MacInness, A. and Powell, David and Richier, Jean-Luc and Voiron, Jacques},
booktitle = \{ESPRIT Conference Week 91},
team = \{DCS},
year = \{1991},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Formal Specification and verification of a Network Independent Atomic Multicast Protocol

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{BaptistaGrafRichier90,
title = \{Formal Specification and verification of a Network Independent Atomic Multicast Protocol},
author = \{Baptista, M. and Graf, Susanne and Richier, Jean-Luc and Rodrigues, Luis and Rodr\'{\i}guez, Carlos and Ver\'{\i}ssimo, Paulo and Voiron, Jacques},
booktitle = \{IFIP Conf. FORTE 90, Madrid},
month = \{November},
publisher = \{North Holland},
team = \{DCS},
year = \{1990},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Compositional Minimisation of Finite State Processes

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

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

### Bibtex reference

@inproceedings\{GrafSteffen90,
title = \{Compositional Minimisation of Finite State Processes},
author = \{Graf, Susanne and Steffen, Bernhard},
booktitle = \{Workshop on Computer-Aided Verification, Rutgers},
month = \{June},
note = \{also as Aachener Informatik Bericht Nr. 91-23 and as ACM proceedings, online version is the extended journal version},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{531},
team = \{DCS},
year = \{1990},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafRichierRodriguezVoiron89a,
title = \{What are the limits of model checking methods for the verification of real life protocols?},
author = \{Graf, Susanne and Richier, Jean-Luc and Rodr\'{\i}guez, Carlos and Voiron, Jacques},
editor = \{Sifakis, Joseph},
booktitle = \{Workshop on Automatic Verification Methods for Finite State Systems (1st CAV), Grenoble},
month = \{June},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{407},
team = \{DCS},
year = \{1989},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{BouajjaniGrafSifakis88a,
title = \{A Logic for the description of Behaviours and Properties of Concurrent Systems},
author = \{Bouajjani, Ahmed and Graf, Susanne and Sifakis, Joseph},
editor = \{de Bakker, J. W. and de Roever, Willem P. and Rozenberg, Grzegorz},
booktitle = \{Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, REX School/Workshop, Noordwijkerhout},
month = \{May},
series = \{LNCS},
volume = \{354},
team = \{DCS},
year = \{1988},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Readiness Semantics for Regular Processes with Silent Actions

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafSifakis87a,
title = \{Readiness Semantics for Regular Processes with Silent Actions},
author = \{Graf, Susanne and Sifakis, Joseph},
editor = \{Ottmann, Thomas},
booktitle = \{Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987},
month = \{July},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{267},
team = \{DCS},
year = \{1987},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## An expressive logic for a process algebra with silent actions

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafSifakis87b,
title = \{An expressive logic for a process algebra with silent actions},
author = \{Graf, Susanne and Sifakis, Joseph},
editor = \{Banieqbal, Behnam and Barringer, Howard and Pnueli, Amir},
booktitle = \{Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{398},
team = \{DCS},
year = \{1987},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## A complete inference system for an algebra of regular acceptance models

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{Graf86d,
title = \{A complete inference system for an algebra of regular acceptance models},
author = \{Graf, Susanne},
editor = \{Gruska, Jozef and Rovan, Branislav and Wiedermann, Juraj},
booktitle = \{Mathematical Foundations of Computer Science MFCS'86, Bratislava, August 25-29, 1996},
pages = \{386--396},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{223},
team = \{DCS},
year = \{1986},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## From synchronization tree logic to acceptance model logic

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafSifakis85a,
title = \{From synchronization tree logic to acceptance model logic},
author = \{Graf, Susanne and Sifakis, Joseph},
editor = \{Parikh, Rohit},
booktitle = \{Logics of Programs, Conference, Brooklyn College, June 17-19, 1985},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{193},
team = \{DCS},
year = \{1985},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## A Modal Characterization of Observational Congruence on Finite Terms of CCS

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@inproceedings\{GrafSifakis84c,
title = \{A Modal Characterization of Observational Congruence on Finite Terms of {CCS}},
author = \{Graf, Susanne and Sifakis, Joseph},
editor = \{Paredaens, Jan},
booktitle = \{ICALP 84, Antwerpen},
annote = \{a full version is published in Information and Control},
publisher = \{Springer Verlag},
series = \{LNCS},
volume = \{172},
team = \{DCS},
year = \{1984},
class = \{web,rap}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## From Complex UML Models to Systematic Performance Simulation

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{ConstantMoninGraf07,
author = \{Olivier Constant and Wei Monin and Susanne Graf},
title = \{From Complex UML Models to Systematic Performance Simulation},
institution = \{Verimag Research Report},
year = \{2007},
month = \{July},
number = \{TR-2007-10},
team = \{DCS},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Omega Final Project Report

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{OmegaFinalReport-05,
author = \{Susanne Graf and Frank de Boer and Pierre Combes and Jozef Hooman and Hillel Kugler and Marcel Kyas and David Lesens and Iulian Ober and Angelika Votintseva and Yuri Yushtein and Meir Zenou},
title = \{Omega Final Project Report},
institution = \{Deliverable of the Omega IST project},
team = \{DCS},
class = \{web,rap},
year = \{2005}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## States and events in the context of timed systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{Graf03,
author = \{Susanne Graf},
title = \{States and events in the context of timed systems},
institution = \{Verimag},
type = \{contribution to the workshop {ST.EVE} on state based versus event based approach, a satellite event of FM 2003},
year = \{2003},
team = \{DCS},
class = \{rap,web},
month = \{September}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Report on the organisations of ETAPS 2002 in Grenoble

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{etaps-report02,
author = \{Susanne Graf},
title = \{Report on the organisations of ETAPS 2002 in Grenoble},
institution = \{Verimag},
team = \{DCS},
class = \{rap,web},
year = \{2002}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Timed Extensions for SDL

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{comITU00,
author = \{Susanne Graf and Laurent Mounier and Iulian Ober},
title = \{Timed Extensions for SDL},
institution = \{Document Temporaire, ITU, secteur de standardisations des Télécommunications, groupe d'étude 10},
month = \{November},
team = \{DCS},
class = \{rap,web},
year = \{2000}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Coping with Process Identities in Networks of Similar Processes

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{GrafLakhnechWolper99,
author = \{Susanne Graf and Yassine Lakhnech and Pierre Wolper},
title = \{Coping with Process Identities in Networks of Similar Processes},
type = \{Technical Report},
institution = \{Verimag},
month = \{January},
team = \{DCS},
class = \{rap,web},
year = \{1999}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Efficient Automata Encoding of Arithmetic expressions

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{Graf95,
author = \{Susanne Graf},
title = \{Efficient Automata Encoding of Arithmetic expressions},
institution = \{VERIMAG, Grenoble},
type = \{Spectre Technical Report},
year = \{1995},
team = \{DCS},
class = \{rap,web},
note = \{jamais publie, dommage, d'autre (e.g. Wolper), l'ont ensuite fait}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## XESAR version 3.1

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{RodriguezRichierGraf*88b,
author = \{Carlos Rodriguez and Jean-Luc Richier and Jacques Voiron and Susanne Graf},
title = \{{XESAR} version 3.1},
type = \{Research Report Spectre C-11},
institution = \{LGI, Grenoble},
month = \{November},
team = \{DCS},
year = \{1988},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Formal Specification of the Turbo-TR/MAC Protocol

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{GrafVoiron88b,
author = \{Susanne Graf and Jacques Voiron},
title = \{Formal Specification of the {Turbo-TR/MAC} Protocol},
type = \{{Deliverable Esprit Delta-4}, Research Report Spectre C-8},
institution = \{LGI, Grenoble},
team = \{DCS},
class = \{},
month = \{April},
year = \{1988}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@techreport\{graf-schmitt-80,
author = \{Susanne Graf and Alfred Schmitt},
title = \{Simulationsmodell für die Studie von Laufzeiten auf Hardware-Ebene},
type = \{Bericht des Instituts für Programmiersysteme},
institution = \{Fakultät für Informatik, Universität Fredericiana Karlsruhe},
team = \{DCS},
class = \{rap,web},
year = \{1980}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

## Models and Methods for the Construction and Verification of Complex Reactive Systems

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@phdthesis\{Graf-Habil-08,
title = \{Models and Methods for the Construction and Verification of Complex Reactive Systems},
author = \{Graf, Susanne},
type = \{Habilitation à Diriger des Recherches},
month = \{April},
school = \{Université Joseph Fourier, Grenoble},
team = \{DCS},
year = \{2008},
class = \{rap,web}
}

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

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

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 54

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 57

Deprecated: Function ereg_replace() is deprecated in /www/verimag/htdocs/PEOPLE/graf/biblio.php on line 61

### Bibtex reference

@phdthesis\{Graf-PhD-84,
title = \{Logiques du temps arborescent pour la spécification et la preuve de programmes},
author = \{Graf, Susanne},
type = \{Thèse 3me cycle},
month = \{February},
school = \{Institut National Polytechnique de Grenoble},
team = \{DCS},
year = \{1984},
class = \{rap,web}
}