Modeling and Verification of Real-time Systems

Formalisms and Software Tools

Nicolas Navet, Stephan Merz, Nicolas Navet, Stephan Merz

• Publisher: Wiley-ISTE
• Year: 2013
• Print ISBN: 9781848210134
• eBook ISBN: 9781118623954
• Edition: 1
• Topic: Biological Sciences
• Subtopic: System Theory
• Index: Biological Sciences

This title is devoted to presenting some of the most important concepts and techniques for describing real-time systems and analyzing their behavior in order to enable the designer to achieve guarantees of temporal correctness.

Topics addressed include mathematical models of real-time systems and associated formal verification techniques such as model checking, probabilistic modeling and verification, programming and description languages, and validation approaches based on testing. With contributions from authors who are experts in their respective fields, this will provide the reader with the state of the art in formal verification of real-time systems and an overview of available software tools.

Chapter 1

Time Petri Nets - Analysis Methods and Verification with TINA

1.1. Introduction

Among the techniques proposed to specify and verify systems in which time appears as a parameter, two are prominent: Timed Automata (see Chapter 4) and Time Petri nets, introduced in [MER 74].

Time Petri nets are obtained from Petri nets by associating two dates min(t) and max(t) with each transition t. Assuming t became enabled for the last time at date θ, t cannot fire (cannot be taken) before the date θ + min(t) and must fire no later than date θ + max(t), except if firing another transition disabled t before then. Firing a transition takes no time. Time Petri nets naturally express specifications “in delays”. By making explicit the beginnings and ends of actions, they can also express specifications “in durations”; their applicability is thus broad.

We propose in this chapter a panorama of the analysis methods available for Time Petri nets and discuss their implementation. These methods, based on the technique of state classes, were initiated in [BER 83, BER 91]. State class graphs provide finite abstractions for the behavior of bounded Time Petri nets. Various abstractions have been proposed in [BER 83, BER 01, BER 03b], preserving various classes of properties. In this chapter, we will discuss in addition the practical problem of the verification of formulae (model checking) of certain logics on the graphs of state classes available. Using these techniques requires software tools, both for the construction of the state space abstractions and for the actual verification of the properties. The examples discussed in this chapter are handled with the tools available in the Tina environment [BER 04].

The basic concepts of Time Petri nets are reviewed in section 1.2. Sections 1.3 to 1.5 introduce various state class graph constructions, providing finite abstractions of the infinite state spaces of Time Petri nets. Sections 1.3 and 1.4 present the constructions preserving the properties of linear-time temporal logics such as LTL; in addition to traces, the construction of section 1.3 preserves markings while that exposed in section 1.4 also preserve states (markings and temporal information). Section 1.5 discusses preservation of the properties expressible in branching-time temporal logics. Section 1.6 discusses the analysis of firing schedules and presents a method to characterize exactly the possible firing dates of transitions along any finite sequence. The toolbox Tina, implementing all state space abstractions reviewed and a model checker, is presented in section 1.7. The following sections are devoted to the verification of LTL formulae on the graphs of state classes. Section 1.8 presents the logic selected, SE–LTL , an extension of the LTL logic, and the implementation of a verifier for that logic, the module selt of Tina. Section 1.9 discusses two application examples and their verification.

1.2. Time Petri nets

1.2.1. Definition

Let I⁺ be the set of non-empty real intervals with non-negative rational endpoints. For i ∈ I⁺, ↓ i denotes its left endpoint and ↑ i its right endpoint (if i is bounded) or ∞ (otherwise). For all

denotes the interval

.

DEFINITION 1.1.- A Time Petri net (TPN for short) is a tuple (P, T, Pre, Post, m₀ , I_s ), in which (P, T, Pre, Post, m₀ ) is a Petri net and I_s : T → I⁺ is a function called the Static Interval function.

Application I_s associates a temporal interval I_s (t) with each transition of the net. Therationals Eft_s (t) = ↓ I_s (t) and Lft_s (t) = ↑ I_s (t) are called the static earliest firing time, and static latest firing time of transition t, respectively. A Time Petri net is represented in Figure 1.1.

1.2.2. States and the state reachability relation

DEFINITION 1.2.- A state of a Time Petri net is a pair e = (m, I ) in which m is a marking and I : T → I⁺ a function that associates a temporal interval with each transition enabled at m.

Figure 1.1. A Time Petri net

The initial state is e₀ = (m₀ , i₀ ), where I₀ is the restriction of I_s to the transitions enabled at m₀ . Any transition enabled must fire in the time interval associated with it.

Firing t at date θ from e = (m, I) (or, equivalently, waiting θ units of time then firing t instantly) is thus allowed if and only if:

The state e′ = (m′, I′) reached from e by firing t at θ is determined by:

1) m′ = m - Pre (t) + Post (t) (as in Petri nets).

2) For each transition k enabled at m′ :

Let us note by

the timed reachability relation defined above, and let

stand for

. A firing schedule is a sequence of timed transitions t₁ @θ₁... t_n @θ_n. It is firable from e if the transit...

Table of contents

• Cover
• Title Page
• Copyright Page
• Preface
• Chapter 1: Time Petri Nets - Analysis Methods and Verification with TINA
• Chapter 2: Validation of Reactive Systems by Means of Verification and Conformance Testing
• Chapter 3: An Introduction to Model Checking
• Chapter 4: Model Checking Timed Automata
• Chapter 5: Specification and Analysis of Asynchronous Systems using CADP
• Chapter 6: Synchronous Program Verification with Lustre/Lesar
• Chapter 7: Synchronous Functional Programming with Lucid Synchrone
• Chapter 8: Verification of Real-Time Probabilistic Systems
• Chapter 9: Verification of Probabilistic Systems Methods and Tools
• Chapter 10: Modeling and Verification of Real-Time Systems using the IF Toolset
• Chapter 11: Architecture Description Languages: An Introduction to the SAE AADL
• List of Authors
• Index