Susanne Graf

Timing analysis and validation of the embedded MARS bus manager (2008)

(will be inserted by the editor)

Iulian Ober, Susanne Graf, Yuri Yushtein

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

Compositional Minimisation of Finite State Systems Using Interface (2008)

Speci Cations, Susanne Graf, Bernhard Ste En, Gerald Luttgen

State explosion problem Abstract. We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to...

Software Tools for Technology Transfer manuscript No. (2008)

Modeling and Validation of a Software Architecture for the Ariane-5 Launcher ⋆ (2008)

(will be inserted by the editor) A real-time profile for UML ⋆

Iulian Ober, Susanne Graf, David Lesens

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

IOS Press Time in State Machines (2008)

Susanne Graf, Andreas Prinz

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

IF: a validation environment for real-time UML and SDL models (2008)

Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober

IF[5, 6, 8, 10, 14] is an open validation platform for asynchronous timed systems such as telecommunication protocols or distributed applications. The toolbox is built upon a specification language...

Validating (2008)

Software Tools for Technology Transfer manuscript No. (2008)

(will be inserted by the editor)

Iulian Ober, Susanne Graf, David Lesens

(will be inserted by the editor) A case study in UML model-based validation: the Ariane-5 launcher software

Modeling and Analysis of Real-time and Embedded Systems (2008)

Susanne Graf, Øystein Haugen, Iulian Ober, Bran Selic

Abstract: This paper presents an overview of the workshop MARTES on

Comparing Heuristics for Model Based Testsuite Generation (2008)

Modellbasierte Entwicklung, Informatik Bericht, Tu Braunschweig, Jörg Desel, Matthias Gehrke, Petra Nawratil, ...

Michael von der Beek............................................................................................ 1 Einsatz von Modell-basierten Entwicklungstechniken in sicherheitsrelevanten...

SVERTS – Specification and Validation of Real-time and Embedded Systems (2008)

Susanne Graf, Øystein Haugen, Ileana Ober, Bran Selic

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

How useful is the UML profile SPT without Semantics? 1 (2008)

Software Tools for Technology Transfer manuscript No. (2008)

The UML Profile for Scheduling, Performance and Time (SPT) defines a set of concepts useful for modeling real-time systems. Its purpose is to integrate notation used by existing real-time analysis...

Validating timed UML (2008)

(will be inserted by the editor) A real-time profile for UML ⋆

Validating timed UML (2008)

(will be inserted by the editor)

A Framework for Time in FDTs (2008)

(will be inserted by the editor)

Susanne Graf, Andreas Prinz

Abstract. ASM is recognized as a useful formalism for defining the semantics of programming languages and modeling formalisms, but it has not initially been intended for expressing non functional...

Centre Equation (2008)

Saddek Bensalem, Susanne Graf, Yassine Lakhnech

Abstract. We present a methodology for constructing abstractions and re ning them by analyzing counter-examples. We also present a uniform veri cation method that combines abstraction, model-checking...

How useful is the UML profile SPT without Semantics? 1 (2008)

Abstraction as the Key for Invariant Verification (2008)

The UML Profile for Scheduling, Performance and Time (SPT) defines a set of concepts useful for modeling real-time systems. Its purpose is to integrate notation used by existing real-time analysis...

Saddek Bensalem, Susanne Graf, Yassine Lakhnech, Avenue De Vignate

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

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

Närstående till person med bipolär sjukdom - hur tillvaron kan te sig. En fallstudie. (2008)

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

Närstående till person med bipolär sjukdom - hur tillvaron kan te sig. En fallstudie. (2008)

Introduktion. Sjuksköterskan inom psykiatrin möter många närståendetill personer med psykisk ohälsa. I stödet till de närstående börlivsvärldsperspektivet vara centralt....

First international workshop on model based architecting and construction of embedded systems (ACES-MB 2008) (2008)

Introduktion. Sjuksköterskan inom psykiatrin möter många närståendetill personer med psykisk ohälsa. I stödet till de närstående börlivsvärldsperspektivet vara centralt....

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

Construction of state graphs of infinite systems with PVS (2007)

Susanne Graf, Hassen Saidi

In this paper, we propose a method for the automatic construction of an abstract state graph of an infinite state system using the Pvs theorem prover. Given a system and a partition of the state...

IF Validation Environment Tutorial (2007)

Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober

IF[3, 7] is an open validation platform for asynchronous timed systems developed at Verimag during the last 5 years.

, Jean-Pierre (2007)

Marius Bozga, Jean-claude Fernandez, Lucian Ghirvu, Susanne Graf, Laurent Mounier, Joseph Sifakis

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

2 (2007)

Marius Bozga, Jean-claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-pierre Krimm, Laurent Mounier

2

a (2007)

Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober, Jean-luc Roux, Daniel Vincent

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

2 (2007)

Marius Bozga, Jean-claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-pierre Krimm, Laurent Mounier

VERIMAG, Centre Equation, 2 avenue de Vignate, F-38610 Gi`eres 2 LSR/IMAG, BP 82, F-38402 Saint Martin d'H`eres Cedex

A Real-time Prole for UML and how to adapt it to SDL (2007)

Annex 8. Technical overview of the (2007)

Abstract. This paper presents work of the IST project OMEGA, where we have dened a UML prole for real-time compatible with the Prole for Performance, Scheduling and Real-time accepted recently at...

Time in State Machines (2007)

D2.2.2 Tool set for system verification

Graf, Susanne, Prinz, Andreas

State machines are a very general means to express computations in an implementationindependent way. There are ways to extend the abstract state machine (ASM) framework with distribution aspects, but...

Time in State Machines (2007)

Graf, Susanne, Prinz, Andreas

State machines are a very general means to express computations in an implementationindependent way. There are ways to extend the abstract state machine (ASM) framework with distribution aspects, but...

Logique du temps arborescent pour la spécification et la preuve de programmes (2006)

Verdachts- und ereignisunabhängige Personenkontrollen : polizeirechtliche und verfassungsrechtliche Aspekte der Schleierfahndung / (2006)

Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux...

Graf, Susanne.

Thesis (doctoral) - Albert-Ludwigs-Universität, Freiburg, 2004.

Preface of “Specification and Validation of Real Time (2006)

Susanne Graf, Oystein Haugen, Ileana Ober, Bran Selic

Abstract The ideas of the papers in this special section have originally been presented at the first edition of the workshop on Specification and Validation of Real Time and Embedded Systems (SVERTS)...

SPECIAL SECTION ON SPECIFICATION AND VALIDATION OF MODELS OF REAL TIME AND EMBEDDED SYSTEMS WITH UML (2006)

SPECIAL SECTION ON SPECIFICATION AND VALIDATION OF MODELS OF REAL TIME AND EMBEDDED SYSTEMS WITH UML (2005)

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

3.2 GENERAL TOOL SET ARCHITECTURE AND INTEGRATION........................................................... 9 3.3 WORKFLOW FOR THE CONSIDERED PROFILE AND TOOLS......................................................... 11 3.4 REFERENCES CONCERNING THE GENE (2005)

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

Susanne Graf, Hillel Kugler, Marcel Kyas, David Lesens, Iulian Ober, Angelika Votintseva, ...

4 OMEGA UML PROFILE FOR REAL-TIME AND EMBEDDED SYSTEMS AND ITS...

Tools and Applications II: The IF Toolset (2004)

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

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

Tools and Applications II: The IF Toolset (2004)

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

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

Correct Development of Embedded Systems (2004)

Susanne Graf, Jozef Hooman

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

Validation of UML Models via a Mapping to Communicating Extended Timed Automata (2004)

Validation of UML Models via a Mapping to Communicating Extended Timed Automata (2004)

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

Model checking of UML models via a mapping to communicating extended timed automata (2004)

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

Validation of UML Models via a Mapping to Communicating Extended Timed Automata (2004)

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

A real-time profile for UML and how to adapt it to SDL (2003)

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

Http://www.artist-Embedded.org/ (2003)

Abstract. This paper presents work of the IST project OMEGA, where we have defined a UML profile for real-time that is compatible with the Profile for Performance, Scheduling and Real-time recently...

Geoff Coulson, Ivica Crnkovic, Andy Evans, Sébastien Gérard, Susanne Graf, ...

this document, we survey the use of component technologies in di#erent industrial sectors. Two important obstacles to wider adoption of component technology for real-time systems are the following

A Real-time Profile for UML and how to adapt it to SDL (2003)

Validating timed uml models by simulation and verification (2003)

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

Timed annotations with UML (2003)

Abstract. We present in this paper a technique and a tool for validating operational UML models by simulation and verification of dynamic properties. With respect to language coverage, our approach...

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

Abstract. In this paper we describe an approach for real-time modeling in UML focusing on analysis and verification of time and scheduling related properties. We show that the use of timed events,...

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

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

IF-2.0: A validation environment for component-based real-time systems (2002)

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

Marius Bozga, Susanne Graf, Laurent Mounier

It is widely recognised that the automated validation of complex systems can hardly be achieved without tool integration. The development of the IF-1.0 toolbox [3] was initiated several years ago, in...

Expression of time and duration constraints in SDL (2002)

Expression of time and duration constraints in SDL (2002)

Abstract. in this paper we give an overview on a set of time related features, useful in the context of real-time system design and classify them into two categories, those needed for modeling of non...

Automated validation of distributed software using the IF environment (2001)

Abstract. in this paper we give an overview on a set of time related features, useful in the context of real-time system design and classify them into two categories, those needed for modelling of...

Marius Bozga, Susanne Graf, Laurent Mounier

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

Verification experiments on the MASCARA protocol (2001)

Guoping Jia, Susanne Graf

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

Automated validation of distributed software using the IF environment (2001)

Automated validation of distributed software using the IF environment (2001)

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

Automated validation of distributed software using the IF environment (2001)

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

Timed Extensions for SDL (2001)

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

Bozga, Marius, Graf, Susanne, Mounier, Laurent, Ober, Iulian, Roux, Jean-Luc, Vincent, Daniel

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

Automated validation of distributed software using the IF environment (2001)

Timed Extensions for SDL (2001)

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

Bozga, Marius, Graf, Susanne, Mounier, Laurent, Ober, Iulian, Roux, Jean-Luc, Vincent, Daniel

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

SDL for Real-Time: What Is Missing? (2000)

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

. In this paper we give an overview on the main weaknesses of SDL for the development of real-time systems, both on the programming and on the specification side. In particular, the SDL semantics...

IF: A Validation Environment for Timed Asynchronous Systems (category B: tool presentation) (2000)

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

Introduction Formal validation of distributed systems relies on several specification formalisms (such as the international standards lotos [16] or sdl [17]), and it requires different kinds of tools...

IF: A Validation Environment for Timed Asynchronous Systems (2000)

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

Formal validation of distributed systems relies on several specification formalisms (such as the international standards LOTOS or SDL, and it requires different kinds of tools to cover the whole...

IF: A Validation Environment for Timed Asynchronous Systems (2000)

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

Formal validation of distributed systems relies on several specification formalisms (such as the international standards LOTOS or SDL, and it requires different kinds of tools to cover the whole...

SDL for Real-Time: What Is Missing? (2000)

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

In this paper we review the needs of a real-time systems developer that are not covered, for various reasons, by SDL. The issues that we examine are heterogeneous, ranging from pure programming...

SDL for Real-Time: What Is Missing? (2000)

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

In this paper we review the needs of a real-time systems developer that are not covered, for various reasons, by SDL. The issues that we examine are heterogeneous, ranging from pure programming...

IF: An Intermediate Representation for SDL and its Applications (1999)

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

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

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

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

. Formal Description Techniques (fdt), such as lotos or sdl are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of...

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

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

. Formal Description Techniques (fdt), such as lotos or sdl are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of...

IF: An intermediate Representation and Validation Environment for Timed Asynchronous Systems (1999)

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

Formal Description Techniques (FDT), such as LOTOS or SDL are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of commercial...

IF: An intermediate Representation and Validation Environment for Timed Asynchronous Systems (1999)

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

Formal Description Techniques (FDT), such as LOTOS or SDL are at the base of a technology for the specification and the validation of telecommunication systems. Due to the availability of commercial...

Characterization of a sequentially consistent memory and verification of a cache memory by abstraction (1999)

IF: An Intermediate Representation for SDL and its Applications (1999)

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

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

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

IF: An Intermediate Representation for SDL and its Applications (1999)

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

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

Construction of state graphs with PVS (1997)

Susanne Graf, Hassen Saidi

. 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. Given a parallel composition of sequential...

Construction of abstract state graphs with PVS (1997)

Susanne Graf, Hassen Saidi

: We describe in this paper a method based on abstract interpretation which, from a theoretical point of view, is similar to the splitting methods proposed in [DGG93, Dam96] but the weaker abstract...

Compositional Minimisation of Finite State Systems Using Interface Specifications (1996)

Susanne Graf, Bernhard Steffen, Gerald Lüttgen

We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused...

Compositional Minimisation of Finite State Systems Using Interface Specifications (1996)

Susanne Graf, Bernhard Steffen, Gerald Lüttgen

. We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused...

Verifying Invariants Using Theorem Proving (1996)

Susanne Graf, Hassen Saidi, Then P

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

Compositional Minimisation of Finite State Systems Using Interface Specifications (1996)

Speci Cations, Bernhard Steffen, Susanne Graf, Bernhard Ste En, Gerald Lüttgen

We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused...

Compositional Minimisation of Finite State Systems Using Interface Specifications (1996)

Susanne Graf, Bernhard Steffen, Gerald Lüttgern

Semantics) For a 2 A consider the functions E I a : 2 L(I) ! 2 L(I) with E I a (L) = df ae L a if a 2 A I L otherwise Then the local abstract semantic functions for (q; a; q 0 ) 2\Gamma! p with...

Compositional minimization of finite state systems using interface specifications (1995)

Graf, Susanne, Steffen, Bernhard, Lüttgen, Gerald

Compositional Minimization of Finite State Systems Using Interface Specifications (1995)

Susanne Graf, Bernhard Steffen, Bernhard Ste En, Gerald Lüttgen

In this paper we present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state...

Property Preserving Abstractions for the Verification of Concurrent Systems * (1995)

Claire Loiseaux, Susanne Graf

ions for the Verification of Concurrent Systems * CLAIRE LOISEAUX claire.loiseaux@imag.fr SUSANNE GRAF susanne.graf@imag.fr JOSEPH SIFAKIS joseph.sifakis@imag.fr AHMED BOUAJJANI...

Characterization of a Sequentially Consistent Memory and Verification of a Cache Memory by Abstraction (1995)

Compositional Minimisation of Finite State Systems Using Interface Specifications (1995)

ion ? Susanne Graf VERIMAG ?? , Avenue de la Vignate, F-38610 Gi`eres ? ? ? Abstract. The contribution of the paper is two-fold. We give a set of properties expressible as temporal logic formulas...

Susanne Graf, Bernhard Steffen, Gerald Lüttgen

In this paper we present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state...

Characterization of a Sequentially Consistent Memory and Verification of a Cache Memory by Abstraction (1995)

Characterization of a Sequentially Consistent Memory and Verification of a Cache Memory by Abstraction (1995)

ion ? Susanne Graf VERIMAG ?? , Rue Lavoisier, F-38330 Monbonnot, e-mail: graf@imag.fr Abstract. The contribution of the paper is two-fold. We give a set of properties expressible as temporal logic...

A Tool for Symbolic Program Verification and Abstraction (1993)

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

Susanne Graf, Claire Loiseaux

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

Program Verification Using Abstraction Compositionally (1993)

Susanne Graf, Claire Loiseaux

We study property preserving transformations for reactive systems. A key idea is the use of %- simulations which are simulations parametrized by a relation %, relating the domains of two systems. We...

Compositional minimization of finite state systems (1990)

Susanne Graf, Bernhard Steffen, Aachener Informatikberichte

In this paper we develop a compositional method for the construction of the minimal transition system that represents the semantics of a given reactive system. The point of this method is that it...

Logique du temps arborescent pour la spécification et la preuve de programmes (1984)

Logique du temps arborescent pour la spécification et la preuve de programmes (1984)

Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux...

Logique du temps arborescent pour la spécification et la preuve de programmes (1984)

Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux...

Logique du temps arborescent pour la spécification et la preuve de programmes (1984)

Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux...

Logique du temps arborescent pour la spécification et la preuve de programmes (1984)

Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux...