The Inverse Method E-Book

Etienne André

• Herausgeber: John Wiley & Sons
• Kategorie: Wissenschaft und neue Technologien
• Sprache: Englisch

Seitenzahl: 273

Veröffentlichungsjahr: 2013

Beschreibung

This book introduces state-of-the-art verification techniques for real-time embedded systems, based on the inverse method for parametric timed automata. It reviews popular formalisms for the specification and verification of timed concurrent systems and, in particular, timed automata as well as several extensions such as timed automata equipped with stopwatches, linear hybrid automata and affine hybrid automata.
The inverse method is introduced, and its benefits for guaranteeing robustness in real-time systems are shown. Then, it is shown how an iteration of the inverse method can solve the good parameters problem for parametric timed automata by computing a behavioral cartography of the system. Different extensions are proposed particularly for hybrid systems and applications to scheduling problems using timed automata with stopwatches. Various examples, both from the literature and industry, illustrate the techniques throughout the book.
Various parametric verifications are performed, in particular of abstractions of a memory circuit sold by the chipset manufacturer ST-Microelectronics, as well as of the prospective flight control system of the next generation of spacecraft designed by ASTRIUM Space Transportation.

Contents:

1. Parametric Timed Automata.
2. The Inverse Method for Parametric Timed Automata.
3. The Inverse Method in Practice: Application to Case Studies.
4. Behavioral Cartography of Timed Automata.
5. Parameter Synthesis for Hybrid Automata.
6. Application to the Robustness Analysis of Scheduling Problems.
7. Conclusion and Perspectives.

About the Authors

Étienne André is Associate Professor in the Laboratoire d’Informatique de Paris Nord, in the University of Paris 13 (Sorbonne Paris Cité) in France. His current research interests focus on the verification of real-time systems.
Romain Soulat is currently completing his PhD at the LSV laboratory at ENS-Cachan in France, focusing on the modeling and verification of hybrid temporal systems.

Leseprobe

Contents

Preface

Acknowledgments

Introduction

I.1. Motivation

I.2. The good parameters problem

I.3. Content and organization of the book

Chapter 1. Parametric Timed Automata

1.1. Constraints on clocks and parameters

1.2. Labeled transition systems

1.3. Timed automata

1.4. Parametric timed automata

1.5. Related work

Chapter 2. The Inverse Method for Parametric Timed Automata

2.1. The inverse problem

2.2. The inverse method algorithm

2.3. Variants of the inverse method

2.4. Related work

Chapter 3. The Inverse Method in Practice: Application to Case Studies

3.1. IMITATOR

3.2. Flip-flop

3.3. SR-Latch

3.4. AND–OR

3.5. IEEE 1394 Root Contention Protocol

3.6. Bounded Retransmission Protocol

3.7. CSMA/CD protocol

3.8. The SPSMALL memory

3.9. Networked automation system

3.10. Tools related to IMITATOR

Chapter 4. Behavioral Cartography of Timed Automata

4.1. The behavioral cartography algorithm

4.2. Properties

4.3. Case studies

4.4. Related work

Chapter 5. Parameter Synthesis for Hybrid Automata

5.1. Hybrid automata with parameters

5.2. Algorithms for hybrid automata

5.3. Implementation

5.4. Discussion

5.5. Related work

Chapter 6. Application to the Robustness Analysis of Scheduling Problems

6.1. Preliminaries

6.2. Scheduling analysis using the inverse method

6.3. Application to scheduling problems

6.4. Discussion

6.5. Related work

Chapter 7. Conclusion and Perspectives

7.1. Trace-based inverse method and partial orders

7.2. Preservation of temporal logics

7.3. Application to other formalisms

Bibliography

Index

First published 2013 in Great Britain and the United States by ISTE Ltd and John Wiley & Sons, Inc.

Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form or by any means, with the prior permission in writing of the publishers, or in the case of reprographic reproduction in accordance with the terms and licenses issued by the CLA. Enquiries concerning reproduction outside these terms should be sent to the publishers at the undermentioned address:

ISTE Ltd

27-37 St George’s Road

London SW19 4EU

UK

www.iste.co.uk

John Wiley & Sons, Inc.

111 River Street

Hoboken, NJ 07030

USA

www.wiley.com

© ISTE Ltd 2013

The rights of Étienne André and Romain Soulat to be identified as the author of this work have been asserted by them in accordance with the Copyright, Designs and Patents Act 1988.

Library of Congress Control Number: 2012953075

British Library Cataloguing-in-Publication Data

A CIP record for this book is available from the British Library

ISSN: 2051-2481 (Print)

ISSN: 2051-249X (Online)

ISBN: 978-1-84821-447-7

Preface

This book introduces state-of-the-art verification techniques for real-time embedded systems, based on the inverse method for parametric timed automata. It reviews popular formalisms for the specification and verification of timed concurrent systems and, in particular, timed automata as well as several extensions such as timed automata equipped with stopwatches, linear hybrid automata and affine hybrid automata. The inverse method is introduced, and its benefits for guaranteeing robustness in real-time systems are shown. Then, it is shown how an iteration of the inverse method can solve the good parameters problem for parametric timed automata by computing a behavioral cartography of the system. Different extensions are proposed particularly for hybrid systems and applications to scheduling problems using timed automata with stopwatches. Various examples, both from the literature and industry, illustrate the techniques throughout the book. Various parametric verifications are performed, in particular of abstractions of a memory circuit sold by the chipset manufacturer ST-Microelectronics, as well as of the prospective flight control system of the next generation of spacecraft designed by ASTRIUM Space Transportation.

Acknowledgments

The authors wish to thank the numerous colleagues and students who have contributed to the development of the inverse method, its implementation and its practical applications. The authors are very grateful to Laurent Fribourg for his strong support with respect to this book, and for providing valuable feedback on earlier versions of the manuscript. The authors wish to thank Thomas Chatain, Emmanuelle Encrenaz, Ulrich Kühne and Jeremy Sproston for their contributions to the inverse method and its extensions. The authors also wish to acknowledge the contributions of Abdelrezzak Bara, Pirouz Bazargan-Sabet, Remy Chevallier, Dominique Le Dû and Patricia Renault to the VALMEM project presented in section 3.8; the contributions of Olivier De Smet, Bruno Denis and Silvain Ruel to the SIMOP project presented in section 3.9; and the contributions of David Lesens and Pierre Moro to the project presented in section 6.3.

Introduction

The importance of computer systems has dramatically increased in recent decades. Critical systems, involving human lives, need to be perfectly reliable, with a total absence of any inappropriate behavior, such as failures or unexpected sequences of actions.

Let us consider the case of hardware verification. When we analyze synchronous clocked digital circuits, it is possible to separate the functional analysis from the timing analysis: the clock cycle is determined by computing the accumulated delays along the longest path from input to latches, and, assuming that the cycle time is large enough, the functional verification can proceed by ignoring gate and wire delays and by treating the whole circuit at the abstraction level of an untimed finite state automaton. Symbolic methods of model checking relying on efficient and compact representation and manipulation of sets of states are thus very useful for verifying the correctness of hardware circuits.

Such a separation between logic and time is rarely possible when we want to analyze computerized systems that are often made up of dozens of reactive components that are in permanent interaction all together and with the physical environment, with few or no mechanisms of global synchronization. In this context, the delays taken by the individual tasks and their logical interdependency have an immediate impact on the global order in which the actions are taken, and on the functionality of the system. Many counterintuitive phenomena may occur, such as the observation of an increasing global response time to an input when a local delay is decreased. Also, in contrast with what happens in the synchronous world, the delay between two events can no longer be given by a discrete measure, such as the number of clock ticks between them, but could be arbitrarily close to each other.

In this context, the theory of timed automata, which appeared in the early 1990s and makes use of dense time domains, turns out to be a very useful tool for modeling such concurrent asynchronous systems. On the other hand, the determination and tuning of the appropriate timing values and delays for the individual tasks of the various components are achieved by the engineers through an intensive phase of testing and numerical simulation. Once they have determined the reference or nominal values for the individual delays of the tasks and components, they are faced with the challenging question of the robustness of the system in the presence of small variations of the timing delays due to measurement uncertainty or noise perturbations. Another challenging question is to determine if a particular component can be replaced by another component with the same functionality, but possibly with different ranges of timing values. As some even small local timing variation can endanger the global functionality of the system, the engineer is often led to be very conservative in his or her choices, adding extra margins of safety, at the expense of a loss of efficiency and extra cost. He or she also often has to reconduct from scratch a long and tedious phase of empirical testing and simulation, without being able to fully reuse and exploit the simulations done with the previous version of the product.

To alleviate the burden of repeated test and simulation phases, we propose in this book a method, called the inverse method, that exploits the model of timed automata and the knowledge of a reference point of timing values for which the good behavior of the system is known. The method will synthesize automatically a dense zone of points around the reference point for which the discrete behavior of the system, that is the set of all the admissible sequences of interleaving events, is guaranteed to be the same. By repeatedly applying the method, we will also be able to decompose the parameter space into a covering set of “tiles” that ensure a uniform behavior of the system: it will be sufficient to test only one point of the tile in order to know whether or not the system behaves correctly on the whole tile.

The method has been successfully applied to industrial case studies such as an asynchronous memory circuit built by ST-Microelectronics and a prospective architecture for a next generation space control system designed by ASTRIUM Space Transportation. We hope that it will convince the reader that methods combining numerical simulation and testing with symbolic timed model checking are becoming a promising and attractive field of research.

I.1. Motivation

I.1.1. An example of asynchronous circuit

As an example, consider the asynchronous “D flip-flop” circuit described in [CLA 07] and depicted in Figure I.1(a). It is composed of four elements (G1, G2, G3 and G4) interconnected in a cyclic way. Elements G1 and G3 are made up of an “OR” gate and a “NAND” gate. Element G2 is a single “NAND” gate and element G4 is a single “NOT” gate (or inverter). The environment involves two input signals D and CK. The global output signal is Q. This system is a concurrent real-time system. It is concurrent because each of the elements has its own behavior, which depends on the outputs of the other elements. It is real-time because each change of the output of an element occurs after some time, and events can be arbitrarily close to each other. The time between a change of the input and a change of the output is (usually) a matter of nanoseconds, but has a huge importance when verifying such systems.

Figure I.1.Flip-flop (a) circuit and (b) its environment

I.2. The good parameters problem

We formally state the main problem we are interested in addressing in this book. We are interested in finding correct values for the parameters (unknown constants) of parametric timed automata, an extension of timed automata. This synthesis of good parameters corresponds to the good parameters problem, as defined in [FRE 08a] in the framework of linear hybrid automata. We recall this problem below, with M the parameter dimension (i.e. the number of parameters).

The good parameters problem

Given a concurrent real-time system and a rectangular parameter domain , what is the largest set of parameter values within V0 for which the system is safe?

As in [FRE 08a], we suppose that we are given a bounded rectangular parameter domain within which we want to synthesize good parameters. As a consequence, this problem could be referred to as a “bounded good parameters problem”. However, for the sake of consistency with [FRE 08a], we will stick to the good parameter problems. Note also that, as in [FRE 08a], we do not explicitly mention the property that makes the system “safe”. The only requirement is that this “safety” must be checked using the trace set of the system. The fact that the main problem of this book does not mention the property is important, because we will see that some of the techniques we propose in this book do not actually depend on the property we want to check.

I.3. Content and organization of the book

I.3.1. Content

We present here an approach for solving the good parameters problem, mainly in the framework of timed automata [ALU 94]. Timed automata are an extension of the class of standard finite-state automata, making use of clocks, which are real-valued variables evolving linearly at the same rate. Those clocks are compared with the delays of the system in constraints that must be verified in order to stay in a state of the automaton, or in order to take a transition. We can also reset some clocks when firing transitions. The model of timed automata has been widely used in order to study and verify hardware devices, communication protocols and scheduling problems. However, timed automata can verify the correctness of a system only for one given set of values for the timing parameters. When addressing the problem of synthesis of parameters ensuring the correctness of the system, we need to consider parametric timed automata [ALU 93c]. Parametric timed automata are an extension of timed automata to the parametric case, allowing in the constraints the use of parameters (or unknown constants) in place of real-valued constants.

The approach we present here relies on the following inverse method: given a reference valuation of the parameters, it synthesizes a set of parameter valuations (more precisely, a constraint on the delays viewed as parameters), guaranteeing the same time-abstract behavior as for the reference valuation. Roughly speaking, this time-abstract behavior only relies on actions, and not on the time elapsing between actions. This method has two main advantages. First, it gives a criterion of robustness by ensuring the correctness of the system for other values for the parameters around the reference valuation. This is of interest when implementing a system: indeed, the exact model with (for example) integer values for timing delays that has been formally verified will necessarily be implemented using values that will not be exactly the values that have been verified. Second, it allows the system designer to optimize some delays without changing the overall functional behavior of the system.

By iterating this inverse method on various points of a bounded parameter domain, it is then possible to separate the parametric space into tiles, that is subspaces for which the time-abstract behavior of the system is uniform. This gives a behavioral cartography of the system. We can then partition those tiles into good tiles and bad tiles, with respect to a given property we want to verify. The main interest is that this cartography does not depend on the property we want to verify: only the partition into good and bad tiles actually does. As a result when verifying other properties, it is sufficient to check the property for only one point (i.e. one parameter valuation) in each tile in order to get the new partition into good and bad tiles.

Both the inverse method and the behavioral cartography algorithm naturally extend to hybrid automata, an extension of timed automata. A particular application is timed automata equipped with stopwatches, which are interesting to verify scheduling problems with pre-emption.

The tool IMITATOR implements the inverse method, and its behavioral cartography algorithm, in the framework of timed automata. This tool was used to solve many case studies such as communication protocols and hardware circuits. In particular, it synthesized values for the parameters of abstractions of a memory circuit sold by the chipset manufacturer ST-Microelectronics, as well as for a prospective architecture of the flight control system of the next generation of spacecrafts designed by ASTRIUM Space Transportation. An extension of this tool, HyMITATOR, implements these algorithms in the hybrid case.

I.3.2. Organization of the book

This book is structured as follows. In Chapter 1, we recall the major formalisms used in this book. We first recall the notion of clocks, parameters and constraints. We then recall timed automata, and their extension to parametric timed automata. In Chapter 2, we introduce the inverse method, which generalizes the behavior of a timed automaton by synthesizing a constraint on the parameters guaranteeing the same time-abstract behavior. In Chapter 3, we present the tool IMITATOR that implements the inverse method, and we apply the method to various case studies of asynchronous hardware circuits and communication protocols. In Chapter 4, we show how an iteration of the inverse method can solve the good parameters problem for parametric timed automata, by computing a behavioral cartography of the system. We also apply this algorithm to various case studies using IMITATOR. In Chapter 5, we show how the inverse method and the behavioral cartography can be extended to hybrid automata. Several case studies are presented. In Chapter 6, we apply both the inverse method and the behavioral cartography to scheduling problems; this gives a measure of the robustness of solutions computed for scheduling problems. We finally conclude and present directions of future research in Chapter 7. Related work is mentioned at the end of each chapter.

This book tries as much as possible to avoid results that are too theoretical focusing instead on the practical aspects of parameter synthesis for real-time systems. In particular, proofs of the results are usually omitted; only a pointer is given. An exception is section 2.2.4, where we do detail the correctness of the inverse method. Any reader who is not particularly interested in theory can skip Chapter 1 and start directly with Chapter 2, and possibly go back to Chapter 1 later if needed.

I.3.3. Acknowledgements

Most of this work was produced with the support and aid of Laurent Fribourg. Emmanuelle Encrenaz contributed to Chapters 2–4 and Thomas Chatain worked with the authors on the inverse method for parametric timed automata (Chapter 2). The fixpoint of the inverse method benefited from discussions with Laurent Doyen. The counterexample showing the non-CTL (computation tree logic) equivalence of the inverse method was proposed by Jeremy Sproston. Chapter 5 has been taken from work by Laurent Fribourg and Ulrich Kühne [FRI 12a], with their kind agreement.

The analysis of the SPSMALL memory (section 3.8) has been performed in the framework of the ANR VALMEM project involving Étienne André, Emmanuelle Encrenaz, Laurent Fribourg (from LSV), Remy Chevallier (from ST-Microelectronics), Abdelrezzak Bara, Pirouz Bazargan-Sabet, Dominique Le Dû and Patricia Renault (from LIP 6). The analysis of the SIMOP networked automation system (section 3.9) was produced in the framework of the SIMOP project by Institut Farman (Fédération de Recherche CNRS, FR3311), with the contribution of Étienne André, Emmanuelle Encrenaz, Laurent Fribourg (from LSV), Olivier De Smet, Bruno Denis and Silvain Ruel (LURPA, École Normale Supérieure de Cachan). David Lesens and Pierre Moro provided the cases studies used in section 6.3.3 and our implementation benefited from their expertise.

When coming to the design and implementation of the tool IMITATOR (Chapter 3), Étienne André designed the first version of the tool; Ulrich Kühne implemented several algorithmic optimizations allowing us to decrease the computation time, and implemented the hybrid version HyMITATOR. Romain Soulat has been a great contributor of IMITATOR by applying the tool to various case studies; in particular, he applied the cartography algorithm implemented in IMITATOR to the SPSMALL memory, and designed very helpful optimizations. Finally, Daphné Dussaud implemented the graphical output of the cartography in IMITATOR.

1

Parametric Timed Automata

In this chapter, we present the formalisms used throughout this book. In particular, we present timed automata [ALU 94], a powerful modeling formalism for real-time systems. Since this book focuses on synthesizing values for timing parameters of a system, guaranteeing a good behavior, we will also use a parametric extension of timed automata, namely parametric timed automata [ALU 93c]. This chapter presents their syntax and semantics, and more generally all the necessary formalisms to understand the rest of this book. Any reader who is not particularly interested in theory can skip directly to Chapter 2, and return to Chapter 1 when needed.

Outline of the chapter

We describe clocks, parameters and constraints on the clocks and parameters in section 1.1 and labeled transition system in section 1.2. We then introduce the syntax and semantics of timed automata in section 1.3, and parametric timed automata in section 1.4. Related works, including representation of time, and formalisms related to timed automata, are discussed in section 1.5.

1.1. Constraints on clocks and parameters

1.1.1. Clocks

1.1.2. Parameters

1.1.3. Constraints

We define constraints here as a set of linear inequalities.

1.1.3.1. Syntax of constraints

wherevi ∈ V , αi ∈ , for 1 ≤ i ≤ Nand d ∈ .

Note that we define the coefficients of the linear inequalities as positive reals. It would be equivalent to define them as positive rationals, since we consider only linear inequalities. Both definitions are found in the literature; we suppose here that, since we are addressing the problem of the verification of real-time systems, we consider real valued constants.

We assume in the following that all inequalities are linear, and we will simply refer to linear inequalities as inequalities.

We assume in the following that all constraints are both convex and linear, and we will simply refer to convex linear constraints as constraints.

DEFINITION 1.4.– An inequality on the clocks is an inequality on the set of clocks X. A constraint on the clocks is a constraint on the set of clocks X.

DEFINITION 1.5.– An inequality on the parameters is an inequality on the set of parameters P. A constraint on the parameters is a constraint on the set of parameters P.

DEFINITION 1.6.– An inequality on the clocks and the parameters is an inequality on X ∪ P. A constraint on the clocks and the parameters is a constraint on X ∪ P.

Throughout this book, we denote by the set of all constraints on the clocks, by the set of all constraints on the parameters and by the set of all constraints on the clocks and the parameters.

In the following, the letter J will denote an inequality on the parameters, the letter D will denote a constraint on the clocks, the letter K will denote a constraint on the parameters, and the letter C will denote a constraint on the clocks and the parameters.

1.1.3.2. Semantics of constraints

Given a constraint D on the clocks and a clock valuation w, D[w] denotes the expression obtained by replacing each clock x in D with w(x). A clock valuation w satisfies constraint D (denoted by ) if D[w] evaluates to true.

Given a parameter valuation π and a constraint C on the clocks and the parameters, C[π] denotes the constraint on the clocks obtained by replacing each parameter p in C with π(p). Likewise, given a clock valuation w, C[π][w] denotes the expression obtained by replacing each clock x in C[π] with w(x). We say that a parameter valuation πsatisfies a constraint C, denoted by , if the set of clock valuations that satisfy C[π] is non-empty. We use the notation to indicate that C[π][w] evaluates to true.

A convex linear constraint on the clocks and the parameters can also be interpreted as a set of points in the space , more precisely as a convex polyhedron. We will use these notions synonymously. In this geometric context, a valuation w satisfying a constraint C is equivalent to the polyhedron C containing the corresponding point w, written as w ∈ C. For a partial valuation w (i.e. a point of a subspace of C), we write w ∈ C if and only if w is contained in the projection of C on the variables of w.

Given a constraint C on the clocks and the parameters, we denote by C↓P the constraint on the parameters obtained by projecting C onto the set of parameters, that is after elimination of the clock variables. Formally:

Sometimes we will refer to a variable domain X′, which is obtained by renaming the variables in X. Explicit renaming of variables is denoted by the substitution operation. Given a constraint C on the clocks and the parameters, we denote by C[X←X′] the constraint obtained by replacing in C the variables of X by the variables of X′.

We define the time elapsing of C, denoted by C↑, as the constraint over X and P obtained from C by delaying an arbitrary amount of time. Note that, of course, only clocks can evolve; parameters are unknown constants and therefore remain constant. Formally:

where d is a new parameter with values in and X′ is a renamed set of clocks. The inner part of the expression adds a delay d to all clocks; the projection onto X′ ∪ P eliminates the original set of clocks X, as well as the variable d; the outer part of the expression renames clocks X′ with X.

1.2. Labeled transition systems

We now introduce labeled transition systems, which will be used later in this section to represent the semantics of timed automata.

1.3. Timed automata

Timed automata are an extension of standard finite-state automata allowing the use of clocks, that is real-valued variables increasing linearly at the same rate. Such clocks can be compared with constants in constraints that allow us (or not) to stay in a location (“invariants”) or to take a transition (“guards”). At each transition, it is possible to reset some of the clocks of the system. This formalism allows the parallel composition of several timed automata, which behave like a single one, and thus provides the designer with a powerful and intuitive way to represent timed systems. It is important to note that the formalism of timed automata is very sensitive to the size of the automata and the number of automata in parallel, thus often leading to the state-space explosion problem. However, powerful tools, such as the UPPAAL [LAR 97] model checker, have been implemented, allowing designers to model and verify very efficiently timed systems modeled by timed automata.

1.3.1. Syntax

Σ

is a

finite set of

actions,

Q is a finite set of

locations,

q

0

∈

Q is the

initial location,

X is a set of

clocks,

I

:

is the

invariant,

assigning to every q

∈

Q

a constraint I

(

q

)

on the clocks and

→

is a transition relation consisting of elements of the form

(

q

,

g

,

a

,

ρ

,

q

′),

also denoted by

,

where q

,

q

′ ∈

Q

,

a

∈ Σ,

ρ

⊆

X

is a set of clock variables to be

reset

by the transition, and

is the

guard

of the transition

.

Note that we use a more permissive definition of the constraints used in guards and invariants than in the original definition of timed automata (see [ALU 94]). Indeed, we allow the use of conjunctions of any linear inequalities on the clocks, whereas the original definition usually considers conjunctions of comparisons of a single clock with a constant. This more permissive definition usually has an impact on the decidability (the addition of clock values within a constraint leads to undecidability [ALU 94]), but this has no impact in this book, mainly because of the use of parametric timed automata, where the parameters bring themselves undecidability in the general case. Furthermore, many tools for (parametric) timed automata allow more permissive definitions than the original one.

Timed automata are often extended in practice with discrete variables, which can be used in guards and transitions, updated within the transitions, and sometimes even used as a factor for clocks. However, in most cases, they represent only syntactic sugar for the discrete space (i.e. locations). As a result, we will not use them in any theoretical part of this book. Note, nevertheless, that many tools for (parametric) timed automata allow the use of such discrete variables, and some of the case studies contained here also use them.

The graphical representation of a timed automaton is an oriented graph where vertices correspond to locations, and edges correspond to actions of . We follow the following conventions for the graphical representation of timed automata: locations are represented by nodes, above of which the invariant of the location is written; transitions are represented by arcs from one location to another location, labeled by the associated guard, the action name and the set of clocks to be reset (guards and invariants equal to true are omitted). The initial location is represented here using a double circle.

EXAMPLE 1.1.– We give in Figure 1.1 an example of a timed automaton containing four locations (viz. q0, q1, q2 and q3), three actions (viz. a, b and c) and two clocks (viz. x1 and x2). The initial location is q0.

Figure 1.1. An example of a timed automaton

In this timed automaton, q0 has invariant x1 ≤ 5, q1 has invariant true and both q2 and q3 have invariant x2 ≤ 5. The transition from q0 to q1 has guard x1 ≥ 4 through action a; no clock is reset. The transition from q0 to q2 has guard x1 ≥ 2 ∧ x2 ≥ 3 through action b, and resets clock x2. The transitions between q2 and q3 can be explained similarly.

1.3.2. Semantics

The semantics of timed automata is given under the form of a labeled transition system, where states are pairs made by a location and a valuation for each clock.

and the transition predicate ⇒ is specified by the following three rules. For all (q, w), (q′, w′) ∈ S, d ≥ 0 and a ∈ Σ,

We consider with the definition of S0 that all clocks are initially set to 0, or have evolved linearly in the bounds given by I(q0). A state (respectively, run) in the concrete semantics will be referred to as a concrete state (respectively, concrete run).

A concrete run is represented under the form of a branch where states are shown within nodes containing the name of the location and the value of each of the clocks, and transitions are shown using edges labeled with the name of the action.

EXAMPLE 1.2.– Consider again the timed automaton of example 1.1. Then, Figure 1.2 shows an example of a concrete run for .

Figure 1.2.Example of a concrete run for a timed automaton