Modeling and Verification of Real-Time Systems

Formalisms and Software Tools
1. Auflage 2008
ISBN: 978-1-84821-013-4
Verlag: Wiley

Buch, Englisch, 448 Seiten, Format (B × H): 163 mm x 234 mm, Gewicht: 717 g

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.

Autoren/Hrsg.

Navet, Nicolas

Merz, Stephan

Inhaltsverzeichnis

Preface 15
Stephan MERZ and Nicolas NAVET

Chapter 1. Time Petri Nets – Analysis Methods and Verification with TINA 19
Bernard BERTHOMIEU, Florent PERES and Francois VERNADAT

1.1. Introduction 19

1.2. Time Petri nets 20

1.2.1. Definition 20

1.2.2. States and the state reachability relation 20

1.2.3. Illustration 22

1.2.4. Some general theorems 23

1.3. State class graphs preserving markings and LTL properties 24

1.3.1. State classes 24

1.3.2. Illustration 25

1.3.3. Checking the boundedness property on-the-fly 26

1.3.4. Variations 27

1.4. State class graphs preserving states and LTL properties 28

1.4.1. Clock domain 28

1.4.2. Construction of the SSCG 29

1.4.3. Variants 30

1.5. State class graphs preserving states and branching properties 32

1.6. Computing firing schedules 33

1.6.1. Schedule systems 33

1.6.2. Delays (relative dates) versus dates (absolute) 34

1.6.3. Illustration 35

1.7. An implementation: the Tina environment 35

1.8. The verification of SE-LTL formulae in Tina 37

1.8.1. The temporal logic SE-LTL 37

1.8.2. Preservation of LTL properties by tina constructions 39

1.8.3. selt: the SE-LTL checker of Tina 39

1.9. Some examples of use of selt 42

1.9.1. John and Fred 42

1.9.2. The alternating bit protocol 44

1.10. Conclusion 47

1.11. Bibliography 48

Chapter 2. Validation of Reactive Systems by Means of Verification and Conformance Testing 51
Camille CONSTANT, Thierry JERON, Herve MARCHAND and Vlad RUSU

2.1. Introduction 51

2.2. The IOSTS model 54

2.2.1. Syntax of IOSTS 54

2.2.2. Semantics of IOSTS 56

2.3. Basic operations on IOSTS 57

2.3.1. Parallel product 57

2.3.2. Suspension 58

2.3.3. Deterministic IOSTS and determinization 60

2.4. Verification and conformance testing wit

Über Autor(innen)

Stephan Merz is a researcher at INRIA Lorraine (Nancy, France). He is interested in formal methods for the analysis and construction of reliable software systems, in particular temporal logic, refinement, and the automated and interactive verification of distributed systems.

Nicolas Navet is a researcher in Real-Time Systems at INRIA Lorraine (Nancy, France). His research interests include real-time scheduling, probalistic modeling and computational intelligence, with applications to automotive embedded systems and financial engineering.