O'Reilly logo

The Inverse Method: Parametric Verification of Real-time Embedded Systems by Romain Soulat, Etienne André

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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

Throughout this book, we assume a fixed set X = {x1, … , xH } of clocks. A clock is a variable xi with value in image, which denotes the set of non-negative real numbers. All clocks evolve linearly at the same rate. We define a clock valuation as a function w: X → assigning ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required