Susanne Graf: Selected Publications


For viewing long items click on the publication titles

Knowledge-based Construction of Distributed Constrained Systems

Graf Susanne, Quinton Sophie

Abstract

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

[download]

Bibtex reference

@article{Graf-Quinton-SoSym-15,
   title = {Knowledge-based Construction of Distributed Constrained Systems},
   author = {Graf, Susanne and Quinton, Sophie},
   journal = {Int. Journal on Software and System Modelling},
   volume = {15},
   number = {4},
   pages = {1163--1180},
   team = {DCS},
   month = {September},
   year = {2016},
   0 = {end}
}

Achieving distributed control through model checking

Graf Susanne, Peled Doron, Quinton Sophie

Abstract

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

[download]

Bibtex reference

@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},
   year = {2012},
   0 = {end}
}

Building Distributed Controllers for Systems with Priorities

Hafaiedh Imene Ben, Graf Susanne, Quinton Sophie

Abstract

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

Bibtex reference

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

Meta-models in Europe: Languages, Tools and Applications

Passerone Roberto, Ben-Hafaiedh Imene, Graf Susanne, Benveniste Albert, Cancila Daniela, Cuccuru Arnaud, Gérard Sébastien, Terrier François, Damm Werner, Ferrari Alberto, Mangeruca Leonardo, Josko Bernhard, Peikenkamp Thomas, Sangiovanni-Vincentelli Alberto L.

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Ober Iulian, Graf Susanne, Yushtein Yuri, Ober Ileana

Abstract

This paper presents a case study in UML-based modeling and validation of the intricate timing aspects arising in a small but complex component of the airborne Medium-Altitude Reconnaissance System produced by the Netherlands National Aerospace Laboratory. The purpose is to show how automata-based timing analysis and verification tools can be used by field engineers for solving isolated hard points in a complex real-time design, even if the press-button verification of entire systems remains a remote goal. We claim that the accessibility of such tools is largely improved by the use of an UML profile with intuitive features for modeling timing and related properties. This work has been partially funded by the European OMEGA project (IST-2001-33522). Iulian Ober and Ileana Ober: performed work while at VERIMAG, Grenoble, France. Y. Yushtein: at the moment of writing in National Aerospace Laboratory NLR.

[download]

Bibtex reference

@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},
   0 = {end}
}

OMEGA -- Correct development of Real Time Embedded Systems

Graf Susanne

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},
   0 = {end}
}

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

Graf Susanne, Ober Iulian

Bibtex reference

@article{Graf-Ober-2007,
   title = {Software and architecture modelling with Omega-UML and validation with IF},
   author = {Graf, Susanne and Ober, Iulian},
   address = {http://www.editions-hermes.fr/},
   journal = {Génie Logiciel},
   number = {80},
   pages = {21--26},
   publisher = {Hermes},
   volume = {1},
   team = {DCS},
   year = {2007},
   0 = {end}
}

Time in Abstract State Machines

Graf Susanne, Prinz Andreas

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

A real-time profile for UML

Graf Susanne, Ober Ileana, Ober Iulian

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Validating Timed UML models by simulation and verification

Graf Susanne, Ober Ileana, Ober Iulian

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Ober Ileana, Haugen Oystein, Selic Bran

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Ober Iulian, Graf Susanne, Ober Ileana, Lesens David

[download]

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},
   0 = {end}
}

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

Graf Susanne

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Compositional Minimisation of Finite State Systems using Interface Specifications

Graf Susanne, Lüttgen Gerald, Steffen Bernhard

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Property Preserving Abstractions for the Verification of Concurrent Systems

Loiseaux Claire, Graf Susanne, Sifakis Joseph, Bouajjani Ahmed, Bensalem Saddek

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Sifakis Joseph

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},
   0 = {end}
}

A Modal Characterization of Observational Congruence on Finite Terms of CCS

Graf Susanne, Sifakis Joseph

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Sifakis Joseph

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},
   0 = {end}
}

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

Graf Susanne, Sifakis Joseph

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},
   0 = {end}
}

On Lamport's comparison between linear and branching time logic

Graf Susanne

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},
   0 = {end}
}

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

Tiziana Margaria, Susanne Graf, Larsen Kim Guldstrand (Eds.)

[download]

Bibtex reference

@proceedings{MargariaGrafLarsen18proc,
   editor = {Tiziana Margaria and Susanne Graf and Larsen, Kim Guldstrand},
   title = {Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday},
   series = {Lecture Notes in Computer Science},
   volume = {11200},
   publisher = {Springer},
   year = {2019},
   doi = {10.1007/978-3-030-22348-9},
   0 = {end}
}

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

Susanne Graf, Mahesh Viswanathan (Eds.)

[download]

Bibtex reference

@proceedings{GrafViswanathan-FORTE2015,
   editor = {Susanne Graf and Mahesh Viswanathan},
   title = {Formal Techniques for Distributed Objects, Components, and Systems - 35th {IFIP} {WG} 6.1 International Conference, {FORTE} 2015, Held as Part of the 10th DisCoTec, Grenoble, France, June 2-4, 2015},
   series = {Lecture Notes in Computer Science},
   volume = {9039},
   publisher = {Springer},
   year = {2015},
   team = {DCS},
   0 = {end}
}

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

Iulia Dragomir, Susanne Graf, Gabor Karsai, Florian Noyrit, Iulian Ober, Damiano Torre, Yvan Labiche, Marcela Genero, Maged Elaasar (Eds.)

Bibtex reference

@proceedings{AcesMB-2015,
   editor = {Iulia Dragomir and Susanne Graf and Gabor Karsai and Florian Noyrit and Iulian Ober and Damiano Torre and Yvan Labiche and Marcela Genero and Maged Elaasar},
   title = {Joint Proceedings of the 8th International Workshop on Model-based Architecting of Cyber-physical and Embedded Systems and 1st International Workshop on {UML} Consistency Rules {(ACES-MB} 2015 {\&} {WUCOR} 2015) co-located with {ACM/IEEE} 18th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2015), Ottawa, Canada, September 28, 2015},
   series = {{CEUR} Workshop Proceedings},
   volume = {1508},
   year = {2015},
   0 = {end}
}

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

Florian Noyrit, Susanne Graf, Iulia Dragomir (Eds.)

[download]

Bibtex reference

@proceedings{ACESmb-2014,
   editor = {Florian Noyrit and Susanne Graf and Iulia Dragomir},
   title = {Proceedings of the 7th International Workshop on Model-based Architecting and Construction of Embedded Systems co-located with {ACM/IEEE} 17th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2014), Valencia, Spain, September 30th, 2014},
   series = {{CEUR} Workshop Proceedings},
   volume = {1250},
   publisher = {CEUR-WS.org},
   year = {2014},
   team = {DCS},
   0 = {end}
}

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

Iulian Ober, Florian Noyrit, Susanne Graf, Gabor Karsai (Eds.)

[download]

Bibtex reference

@proceedings{ACESmb-2013,
   editor = {Iulian Ober and Florian Noyrit and Susanne Graf and Gabor Karsai},
   title = {Proceedings of the 6th International Workshop on Model Based Architecting and Construction of Embedded Systems co-located with {ACM/IEEE} 16th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2013), Miami, Florida, USA, September 29th, 2013},
   series = {{CEUR} Workshop Proceedings},
   volume = {1084},
   publisher = {CEUR-WS.org},
   year = {2013},
   team = {DCS},
   0 = {end}
}

Design and Validation of Concurrent Systems, 30.08. - 04.09.2009

Cormac Flanagan, Susanne Graf, Madhusan Parthasarathy, Shaz Qadeer (Eds.)

[download]

Bibtex reference

@proceedings{Dagstuhl-P961-2009,
   editor = {Cormac Flanagan and Susanne Graf and Madhusan Parthasarathy and Shaz Qadeer},
   title = {Design and Validation of Concurrent Systems, 30.08. - 04.09.2009},
   series = {Dagstuhl Seminar Proceedings},
   volume = {09361},
   publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik, Germany},
   year = {2009},
   team = {DCS},
   0 = {end}
}

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

Van Baelen Stefan, Ober Iulian, Graf Susanne, Filali Mamoun, Weigert Thomas (Eds.)

[download]

Bibtex reference

@proceedings{VaObGrFiWe2008,
   editor = {Van Baelen, Stefan and Ober, Iulian and Graf, Susanne and Filali, Mamoun and Weigert, Thomas},
   title = {ACESMB 2008 First International Workshop on Model Based Architecting and Constructing of Embedded Systems, Toulouse, 29/09/2008 - 29/09/2008},
   team = {DCS},
   year = {2008},
   month = {September},
   publisher = {IRIT Press},
   0 = {end}
}

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

De Boer Frank, Bonsangue Marcello, Graf Susanne, De Roever Willem-Paul (Eds.)

[download]

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},
   0 = {end}
}

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

De Boer Frank, Bonsangue Marcello, Graf Susanne, De Roever Willem-Paul (Eds.)

[download]

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},
   0 = {end}
}

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

Graf Susanne, Zhang Wenhui (Eds.)

[download]

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},
   0 = {end}
}

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

De Boer Frank, Bonsangue Marcello, Graf Susanne, De Roever Willem-Paul (Eds.)

[download]

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},
   0 = {end}
}

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

Gérard Sébastien, Graf Susanne, Haugen Oystein, Ober Iulian, Selic Bran (Eds.)

[download]

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},
   0 = {end}
}

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

Gérard Sébastien, Graf Susanne, Haugen Oystein, Ober Iulian, Selic Bran (Eds.)

[download]

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},
   0 = {end}
}

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

De Boer Frank, Bonsangue Marcello, Graf Susanne, De Roever Willem-Paul (Eds.)

[download]

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},
   0 = {end}
}

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

Graf Susanne, Mounier Laurent (Eds.)

[download]

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},
   0 = {end}
}

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

De Boer Frank, Bonsangue Marcello, Graf Susanne, De Roever Willem-Paul (Eds.)

[download]

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},
   0 = {end}
}

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

Graf Susanne, Haugen Oystein, Ober Ileana, Selic Bran (Eds.)

[download]

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},
   0 = {end}
}

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

De Boer Frank, Bonsangue Marcello, Graf Susanne, De Roever Willem-Paul (Eds.)

[download]

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},
   0 = {end}
}

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

Graf Susanne, Schwartzbach Michael (Eds.)

[download]

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},
   0 = {end}
}

SDL and MSC Workshop SAM 2000

Graf Susanne, Jard Claude (Eds.)

[download]

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},
   0 = {end}
}

Contract-Based Reasoning for Component Systems with Rich Interactions

Graf Susanne, Passerone Roberto, Quinton Sophie

[download]

Bibtex reference

@incollection{GrafPasseroneQuinton-2014,
   title = {Contract-Based Reasoning for Component Systems with Rich Interactions},
   author = {Graf, Susanne and Passerone, Roberto and Quinton, Sophie},
   booktitle = {Embedded Systems Development, From Functional Models to Implementations},
   editor = {Alberto L. Sangiovanni Vincentelli and Haibo Zeng and Marco Di Natale and Peter Marwedel},
   pages = {139--154},
   publisher = {Springer New York},
   team = {DCS},
   year = {2014},
   0 = {end}
}

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

Garavel Hubert, Graf Susanne

Bibtex reference

@book{GrafGaravel-BSI-2013,
   title = {Formal Methods for Safe and Secure Computers Systems - BSI Study 875},
   author = {Garavel, Hubert and Graf, Susanne},
   publisher = {BSI German Federal Office for Information Security},
   team = {DCS},
   year = {2013},
   0 = {end}
}

Modeling and Verification of Real Time Systems Using the IF Toolbox

Bozga Marius, Graf Susanne, Mounier Laurent, Ober Iulian

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},
   0 = {end}
}

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

Bozga Marius, Graf Susanne, Mounier Laurent, Ober Iulian

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},
   0 = {end}
}

Roadmap: Component based design and Integration platforms

Jonsson Bengt, Brinksma Ed, Coulson Geoff, Graf Susanne, Crnkovic Ivica, Gérard Sébastien, Hermanns Holger, Jezequel Jean-Marc, Ravn Anders, Schnoebelen Philippe, Terrier François, Votintseva Angelika

[download]

Bibtex reference

@incollection{Artist-comp-roadmap-05,
   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},
   0 = {end}
}

Verification of systems with time-constraints

Graf Susanne, Richier Jean-Luc, Voiron Jacques

[download]

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},
   0 = {end}
}

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

Wang Yi, Morteza Mohaqeqi, Susanne Graf

Abstract

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

[download]

Bibtex reference

@inproceedings{YiMohaqeqiGraf-Coordination22,
   author = {Wang Yi and Morteza Mohaqeqi and Susanne Graf},
   editor = {Maurice H. ter Beek and Marjan Sirjani},
   title = {{MIMOS:} {A} Deterministic Model for the Design and Update of Real-Time Systems},
   booktitle = {Coordination Models and Languages - 24th {IFIP} {WG} 6.1 International Conference, {COORDINATION} 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13-17, 2022, Proceedings},
   series = {Lecture Notes in Computer Science},
   volume = {13271},
   pages = {17--34},
   publisher = {Springer},
   year = {2022},
   doi = {10.1007/978-3-031-08143-9\_2},
   0 = {end}
}

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

Lea Schönberger, Susanne Graf, Selma Saidi, Dirk Ziegenbein, Arne Hamann

Abstract

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

[download]

Bibtex reference

@inproceedings{SchonbergerGrafSaidi*DATE22,
   author = {Lea Sch{ö}nberger and Susanne Graf and Selma Saidi and Dirk Ziegenbein and Arne Hamann},
   editor = {Cristiana Bolchini and Ingrid Verbauwhede and Ioana Vatajelu},
   title = {Contract-Based Quality-of-Service Assurance in Dynamic Distributed Systems},
   booktitle = {2022 Design, Automation {\&} Test in Europe Conference {\&} Exhibition, {DATE} 2022, Antwerp, Belgium, March 14-23, 2022},
   pages = {132--135},
   publisher = {IEEE},
   year = {2022},
   doi = {10.23919/DATE54114.2022.9774529},
   0 = {end}
}

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

Tiziana Margaria, Susanne Graf, Kim Guldstrund Larsen

Bibtex reference

@inproceedings{MargariaGrafLarsen-Isola-18,
   author = {Tiziana Margaria and Susanne Graf and Kim Guldstrund Larsen},
   title = {Models, Mindsets, Meta: The What, the How, and the Why Not?},
   booktitle = {Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday},
   series = {Lecture Notes in Computer Science},
   volume = {11200},
   publisher = {Springer},
   pages = {3--13},
   year = {2018},
   0 = {end}
}

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

Susanne Graf, Sophie Quinton, Alain Girault, Gregor Gö\ssler

Abstract

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

[download]

Bibtex reference

@inproceedings{GrafQuintonGG-FMICS-18,
   author = {Susanne Graf and Sophie Quinton and Alain Girault and Gregor G{ö}{\ss}ler},
   title = {Building Correct Cyber-Physical Systems: Why We Need a Multiview Contract Theory},
   booktitle = {Formal Methods for Industrial Critical Systems - 23rd International Conference, {FMICS} 2018, Maynooth, Ireland, September 3-4, 2018, Proceedings},
   series = {Lecture Notes in Computer Science},
   volume = {11119},
   publisher = {Springer},
   pages = {19--31},
   year = {2018},
   0 = {end}
}

A Framework for Evaluating Schedulability Analysis Tools

Lijun Shan, Susanne Graf, Sophie Quinton, Lo"\ic Fejoz

Abstract

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

[download]

Bibtex reference

@inproceedings{ShanGrafQuintonF-Larsenfest-17,
   author = {Lijun Shan and Susanne Graf and Sophie Quinton and Lo{"\i}c Fejoz},
   title = {A Framework for Evaluating Schedulability Analysis Tools},
   booktitle = {Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday},
   series = {Lecture Notes in Computer Science},
   volume = {10460},
   publisher = {Springer},
   pages = {539--559},
   year = {2017},
   0 = {end}
}

Timing Verification of an Aerial Video Tracking System Using UPPAAL

Lijun Shan, Susanne Graf

[download]

Bibtex reference

@inproceedings{ShaGra-15-Waters,
   author = {Lijun Shan and Susanne Graf},
   title = {Timing Verification of an Aerial Video Tracking System Using UPPAAL},
   booktitle = {Formal Methods for Timing Verification Challenge at WATERS 2015},
   volume = {part of ECRTS 2015, Lund},
   year = {2015},
   0 = {end}
}

Introduction to ACES-MB 2015

Iulia Dragomir, Susanne Graf, Gabor Karsai, Florian Noyrit, Iulian Ober

Bibtex reference

@inproceedings{DBLP:conf/models/DragomirGKNO15,
   author = {Iulia Dragomir and Susanne Graf and Gabor Karsai and Florian Noyrit and Iulian Ober},
   title = {Introduction to {ACES-MB} 2015},
   booktitle = {Joint Proceedings of the 8th International Workshop on Model-based Architecting of Cyber-physical and Embedded Systems and 1st International Workshop on {UML} Consistency Rules {(ACES-MB} 2015 {\&} {WUCOR} 2015) co-located with {ACM/IEEE} 18th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2015), Ottawa, Canada, September 28, 2015.},
   pages = {1--2},
   year = {2015},
   0 = {end}
}

Distributed Implementation of Constrained Systems based on Knowledge

Graf Susanne

Bibtex reference

@inproceedings{Graf-ISPDC-abstr-2014,
   title = {Distributed Implementation of Constrained Systems based on Knowledge},
   author = {Graf, Susanne},
   editor = {Traian Muntean},
   booktitle = {IEEE 13th International Symposium on Parallel and Distributed Computing, ISPDC 2013, Porquerolles Golden Island, France, June 24-27, 2014},
   note = {Two page abstract},
   publisher = {IEEE},
   team = {DCS},
   year = {2014},
   0 = {end}
}

Formal Model Driven Engineering for Space Onboard Software

Conquet Eric, Dormoy Francois-Xavier, Dragomir Iulia, Graf Susanne, Lesens David, Nienaltowski Piotr, Ober Iulian

Abstract

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

Bibtex reference

@inproceedings{Conquet+2012-ERTS2,
   title = {Formal Model Driven Engineering for Space Onboard Software},
   author = {Conquet, Eric and Dormoy, Francois-Xavier and Dragomir, Iulia and Graf, Susanne and Lesens, David and Nienaltowski, Piotr and Ober, Iulian},
   booktitle = {International Congress on Embedded Real Time Software and Systems (ERTS2), Toulouse, February 2012},
   publisher = {French Society for Electricity, Electronics, and Information and Communication Technologies},
   team = {DCS},
   year = {2012},
   0 = {end}
}

Knowledge for the Distributed Implementation of Constrained Systems

Susanne Graf, Sophie Quinton

Bibtex reference

@inproceedings{GrafQinton-iFM13,
   author = {Susanne Graf and Sophie Quinton},
   title = {Knowledge for the Distributed Implementation of Constrained Systems},
   booktitle = {Integrated Formal Methods, 10th International Conference, {IFM} 2013, Turku, Finland, June 10-14, 2013},
   pages = {77--93},
   year = {2013},
   editor = {Einar Broch Johnsen and Luigia Petre},
   series = {Lecture Notes in Computer Science},
   volume = {7940},
   publisher = {Springer},
   team = {DCS},
   xurl = {},
   0 = {end}
}

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

Hafaiedh Imene Ben, Graf Susanne, Jaber Mohamad

Bibtex reference

@inproceedings{BenHafaiedhGrafJaber-ICECS-11,
   title = {Model-based design and distributed implementation of bus arbiter for multiprocessors},
   author = {Hafaiedh, Imene Ben 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},
   year = {2011},
   isbn = {978-1-4577-1845-8},
   0 = {end}
}

Distributed Implementation of Systems with Multiparty Interactions and Priorities

Hafaiedh Imene Ben, Graf Susanne, Mazouz Nejla

Bibtex reference

@inproceedings{BenHafaiedhGrafMazouz-SEFM-11,
   title = {Distributed Implementation of Systems with Multiparty Interactions and Priorities},
   author = {Hafaiedh, Imene Ben 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},
   year = {2011},
   isbn = {978-3-642-24689-0},
   0 = {end}
}

Contract-Based Reasoning for Component Systems with Complex Interactions

Graf Susanne, Passerone Roberto, Quinton Sophie

[download]

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},
   year = {2011},
   0 = {end}
}

Monitoring Distributed Systems Using Knowledge

Graf Susanne, Peled Doron, Quinton Sophie

[download]

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},
   year = {2011},
   isbn = {978-3-642-21460-8},
   0 = {end}
}

Implementing Distributed Controllers for Systems with Priorities

Ben-Hafaiedh Imene, Graf Susanne, Khairallah Hammadi

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},
   year = {2010},
   doi = {http://dx.doi.org/10.4204/EPTCS.30.3},
   0 = {end}
}

Reasoning about Safety and Progress Using Contracts

Ben-Hafaiedh Imene, Graf Susanne, Quinton Sophie

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},
   year = {2010},
   doi = {http://dx.doi.org/10.1007/978-3-642-16901-4_29},
   0 = {end}
}

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

Ben-Hafaiedh Imene, Graf Susanne, Quinton Sophie

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},
   year = {2010},
   0 = {end}
}

Methods for Knowledge Based Controlling of Distributed Systems

Bensalem Saddek, Bozga Marius, Graf Susanne, Peled Doron, Quinton Sophie

[download]

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},
   year = {2010},
   isbn = {978-3-642-15642-7},
   0 = {end}
}

Achieving Distributed Control through Model Checking

Graf Susanne, Peled Doron, Quinton Sophie

Abstract

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

[download]

Bibtex reference

@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},
   year = {2010},
   doi = {http://dx.doi.org/10.1007/978-3-642-14295-6_35},
   0 = {end}
}

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

Ben-Hafaiedh Imene, Constant Olivier, Graf Susanne, Robbana Riadh

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},
   0 = {end}
}

From Orchestration to Choreography: Memoryless and Distributed Orchestrators

Quinton Sophie, Ben-Hafaiedh Imene, Graf Susanne

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},
   year = {2009},
   0 = {end}
}

Model Based Architecting and Construction of Embedded Systems

Ober Iulian, Baelen Stefan Van, Graf Susanne, Filali Mamoun, Weigert Thomas, Gérard Sébastien

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},
   0 = {end}
}

A Model Transformation Tool for Performance Simulation of Complex UML Models

Constant Olivier, Monin Wei, Graf Susanne

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Contract-Based Verification of Hierarchical Systems of Components

Quinton Sophie, Graf Susanne

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

A Framework for Contract-Based Reasoning: Motivation and Application

Quinton Sophie, Graf Susanne

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},
   xurl = {http://www-verimag.imag.fr/~graf/PAPERS/GQ-FLACOS08.pdf},
   team = {DCS},
   year = {2008},
   0 = {end}
}

An Approach to Modeling and Verification of Component Based Systems

Gössler Gregor, Graf Susanne, Majster-Cederbaum Mila, Martens Moritz, Sifakis Joseph

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Contracts for BIP: hierarchical interaction models for compositional verification

Graf Susanne, Quinton Sophie

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Qualification d'architectures fontionnelles

Bozga Marius, Combes Pierre, Graf Susanne, Monin Wei, Moteau Nicolas

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Gérard Sébastien, Haugen Oystein, Ober Iulian, Selic Bran

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Ensuring Properties of Interaction Systems by Construction

Gössler Gregor, Graf Susanne, Majster-Cederbaum Mila, Martens Moritz, Sifakis Joseph

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Ober Iulian, Graf Susanne, Yushtein Yuri

[download]

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},
   0 = {end}
}

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

Ober Iulian, Graf Susanne, Lesens David

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Gérard Sébastien, Haugen Oystein, Ober Iulian, Selic Bran

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Timing analysis and validation of the embedded MARS bus manager

Ober Iulian, Graf Susanne, Yushtein Yuri

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Crnkovic Ivica, Axelsson Jakob, Graf Susanne, Larsson Magnus, Ommering Rob C. van, Wallnau Kurt C.

[download]

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},
   0 = {end}
}

IF Tutorial

Bozga Marius, Graf Susanne, Mounier Laurent, Ober Iulian

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},
   0 = {end}
}

The IF toolset

Bozga Marius, Graf Susanne, Ober Iulian, Ober Ileana, Sifakis Joseph

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Correct Development of Embedded Systems

Graf Susanne, Hooman Jozef

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Ober Ileana

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Haugen Oystein, Ober Ileana, Selic Bran

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Ober Iulian, Graf Susanne, Ober Ileana

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Abstraction as the Key for Invariant Verification

Bensalem Saddek, Graf Susanne, Lakhnech Yassine

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Ober Ileana

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Validating Timed UML models by simulation and verification

Ober Iulian, Graf Susanne, Ober Ileana

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},
   0 = {end}
}

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

Bozga Marius, Graf Susanne, Mounier Laurent

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Expression of time and duration constraints in SDL

Graf Susanne

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Automated validation of distributed software using the IF environment

Bozga Marius, Graf Susanne, Mounier Laurent

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Automated validation of distributed software using the IF environment

Bozga Marius, Mounier Laurent, Graf Susanne

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},
   0 = {end}
}

Timed Extensions for SDL

Bozga Marius, Kerbrat Alain, Graf Susanne, Mounier Laurent, Ober Iulian, Vincent Daniel

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Verification Experiments on the Mascara Protocol

Graf Susanne, Jia Guoping

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

IF: A Validation Environment for Timed Asynchronous Systems

Bozga Marius, Ghirvu Lucian, Graf Susanne, Mounier Laurent

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

SDL for Real Time: What is missing?

Bozga Marius, Graf Susanne, Kerbrat Alain, Mounier Laurent, Ober Iulian, Vincent Daniel

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Bozga Marius, Fernandez Jean-Claude, Ghirvu Lucian, Graf Susanne, Krimm Jean-Pierre, Mounier Laurent

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

IF: An Intermediate Representation for SDL and its Applications

Bozga Marius, Fernandez Jean-Claude, Ghirvu Lucian, Graf Susanne, Krimm Jean-Pierre, Mounier Laurent, Sifakis Joseph

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Construction of abstract state graphs with PVS

Graf Susanne, Saidi Hassen

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Verifying invariants using theorem proving

Graf Susanne, Saidi Hassen

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Verification of a distributed Cache memory by using abstractions

Graf Susanne

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Program Verification using compositional Abstraction

Graf Susanne, Loiseaux Claire

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

A tool for symbolic program verification and abstraction

Graf Susanne, Loiseaux Claire

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Safety for branching Semantics

Bouajjani Ahmed, Fernandez Jean-Claude, Graf Susanne, Sifakis Joseph, Rodriguez Carlos

Abstract

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

[download]

Bibtex reference

@inproceedings{BouajjaniFernandezGrafSifakis*90,
   title = {Safety for branching Semantics},
   author = {Bouajjani, Ahmed and Fernandez, Jean-Claude and Graf, Susanne and Sifakis, Joseph and Rodriguez, Carlos},
   editor = {Albert-Leach, Javier and Monien, Burkhard and Rodriguez-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},
   0 = {end}
}

An Algebra for Boolean Processes

Courcoubetis Costas, Graf Susanne, Sifakis Joseph

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

Delta-4 Architecture Validation

Kanoun Kamara, Arlat Jean, Burrill L., Crouzet Yves, Graf Susanne, Martins Eliane, MacInness A., Powell David, Richier Jean-Luc, Voiron Jacques

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},
   0 = {end}
}

Formal Specification and verification of a Network Independent Atomic Multicast Protocol

Baptista M., Graf Susanne, Richier Jean-Luc, Rodrigues Luis, Rodr\'\iguez Carlos, Ver\'\issimo Paulo, Voiron Jacques

Abstract

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

[download]

Bibtex reference

@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},
   address = {Madrid},
   month = {November},
   publisher = {North Holland},
   team = {DCS},
   year = {1990},
   0 = {end}
}

Compositional Minimisation of Finite State Processes

Graf Susanne, Steffen Bernhard

Abstract

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

[download]

Bibtex reference

@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},
   0 = {end}
}

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

Graf Susanne, Richier Jean-Luc, Rodr\'\iguez Carlos, Voiron Jacques

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},
   0 = {end}
}

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

Bouajjani Ahmed, Graf Susanne, Sifakis Joseph

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},
   0 = {end}
}

Readiness Semantics for Regular Processes with Silent Actions

Graf Susanne, Sifakis Joseph

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},
   0 = {end}
}

An expressive logic for a process algebra with silent actions

Graf Susanne, Sifakis Joseph

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},
   0 = {end}
}

A complete inference system for an algebra of regular acceptance models

Graf Susanne

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},
   0 = {end}
}

From synchronization tree logic to acceptance model logic

Graf Susanne, Sifakis Joseph

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},
   0 = {end}
}

A Modal Characterization of Observational Congruence on Finite Terms of CCS

Graf Susanne, Sifakis Joseph

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},
   0 = {end}
}

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

Wang Yi, Morteza Mohaqeqi, Susanne Graf

Abstract

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

[download]

Bibtex reference

@techreport{YMG-MIMOS-Arxiv-2020,
   author = {Wang Yi and Morteza Mohaqeqi and Susanne Graf},
   title = {{MIMOS:} {A} Deterministic Model for the Design and Update of Real-Time Systems},
   institution = {CoRR},
   volume = {abs/2011.13234},
   year = {2020},
   eprinttype = {arXiv},
   eprint = {2011.13234},
   0 = {end}
}

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

Lijun Shan, Susanne Graf, Sophie Quinton

Abstract

[download]

Bibtex reference

@techreport{ShanGrafQuinton-HAL-16,
   author = {Lijun Shan and Susanne Graf and Sophie Quinton},
   title = {RTLib: A Library of Timed Automata for Modeling Real-Time Systems},
   institution = {Research Report Univ Grenoble Alpes - INRIA Grenoble-Rhone-Alpes},
   year = {2016},
   0 = {end}
}

From Complex UML Models to Systematic Performance Simulation

Olivier Constant, Wei Monin, Susanne Graf

Abstract

[download]

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},
   0 = {end}
}

Omega Final Project Report

Susanne Graf, Frank de Boer, Pierre Combes, Jozef Hooman, Hillel Kugler, Marcel Kyas, David Lesens, Iulian Ober, Angelika Votintseva, Yuri Yushtein, Meir Zenou

[download]

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},
   year = {2005},
   0 = {end}
}

States and events in the context of timed systems

Susanne Graf

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},
   month = {September},
   0 = {end}
}

Report on the organisations of ETAPS 2002 in Grenoble

Susanne Graf

Bibtex reference

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

Timed Extensions for SDL

Susanne Graf, Laurent Mounier, Iulian Ober

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},
   year = {2000},
   0 = {end}
}

Coping with Process Identities in Networks of Similar Processes

Susanne Graf, Yassine Lakhnech, Pierre Wolper

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},
   year = {1999},
   0 = {end}
}

Efficient Automata Encoding of Arithmetic expressions

Susanne Graf

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},
   note = {jamais publie, dommage, d'autres l'ont ensuite fait ... mais je voulais un truc comme SMT ...},
   0 = {end}
}

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

Susanne Graf, Alfred Schmitt

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},
   year = {1980},
   0 = {end}
}