The Inverse Method: Parametric Verification of Real-time Embedded Systems

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 = {x₁, … , x_H } of clocks. A clock is a variable x_i with value in , 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 ...