Modeling and Verification of Real-time Systems E-Book

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

Seitenzahl: 655

Veröffentlichungsjahr: 2013

Beschreibung

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.

Leseprobe

Contents

Preface

Stephan MERZ and Nicolas NAVET

Chapter 1. Time Petri Nets - Analysis Methods and Verification with TINA

Bernard BERTHOMIEU, Florent PERES and François VERNADAT

1.1. Introduction

1.2. Time Petri nets

1.3. State class graphs preserving markings and LTL properties

1.4. State class graphs preserving states and LTL properties

1.5. State class graphs preserving states and branching properties

1.6. Computing firing schedules

1.7. An implementation: the Tina environment

1.8. The verification of SE–LTL formulae in Tina

1.9. Some examples of use of selt

1.10. Conclusion

1.11. Bibliography

Chapter 2. Validation of Reactive Systems by Means of Verification and Conformance Testing

Camille CONSTANT, Thierry JÉRON, Hervé MARCHAND and Vlad RUSU

2.1. Introduction

2.2. The IOSTS model

2.3. Basic operations on IOSTS

2.4. Verification and conformance testing with IOSTS

2.5. Test generation

2.6. Test selection

2.7. Conclusion and related work

2.8. Bibliography

Chapter 3. An Introduction to Model Checking

Stephan MERZ

3.1. Introduction

3.2. Example: control of an elevator

3.3. Transition systems and invariant checking

3.4. Temporal logic

3.5. Model checking algorithms

3.6. Some research topics

3.7. Bibliography

Chapter 4. Model Checking Timed Automata

Patricia BOUYER and François LAROUSSINIE

4.1. Introduction

4.2. Timed automata

4.3. Decision procedure for checking reachability

4.4. Other verification problems

4.5. Some extensions of timed automata

4.6. Subclasses of timed automata

4.7. Algorithms for timed verification

4.8. The model-checking tool Uppal

4.9. Bibliography

Chapter 5. Specification and Analysis of Asynchronous Systems using CADP

Radu MATEESCU

5.1. Introduction

5.2. The CADP toolbox

5.3. Specification of a drilling unit

5.4. Analysis of the functioning of the drilling unit

5.5. Conclusion and future work

5.6. Bibliography

Chapter 6. Synchronous Program Verification with Lustre/Lesar

Pascal RAYMOND

6.1. Synchronous approach

6.2. The Lustre language

6.3. Program verification

6.4. Expressing properties

6.5. Algorithms

6.6. Enumerative algorithm

6.7. Symbolic methods and binary decision diagrams

6.8. Forward symbolic exploration

6.9. Backward symbolic exploration

6.10. Conclusion and related works

6.11. Demonstrations

6.12. Bibliography

Chapter 7. Synchronous Functional Programming with Lucid Synchrone

Paul CASPI, Grégoire HAMON and Marc POUZET

7.1. Introduction

7.2. Lucid Synchrone

7.3. Discussion

7.4. Conclusion

7.5. Acknowledgment

7.6. Bibliography

Chapter 8. Verification of Real-Time Probabilistic Systems

Marta KWIATKOWSKA, Gethin NORMAN, David PARKER and Jeremy SPROSTON

8.1. Introduction

8.2. Probabilistic timed automata

8.3. Model checking for probabilistic timed automata

8.4. Case study: the IEEE FireWire root contention protocol

8.5. Conclusion

8.6. Bibliography

Chapter 9. Verification of Probabilistic Systems Methods and Tools

Serge HADDAD and Patrice MOREAUX

9.1. Introduction

9.2. Performance evaluation of Markovian models

9.3. High level stochastic models

9.4. Probabilistic verification of Markov chains

9.5. Markov decision processes

9.6. Bibliography

Chapter 10. Modeling and Verification of Real-Time Systems using the IF Toolset

Marius BOZGA, Susanne GRAF, Laurent MOUNIER and Iulian OBER

10.1. Introduction

10.2. Architecture

10.3. The IF notation

10.4. The IF tools

10.5. An overview on uses of IF in case studies

10.6. Case study: the Ariane 5 flight program

10.7. Conclusion

10.8. Bibliography

Chapter 11. Architecture Description Languages: An Introduction to the SAE AADL

Anne-Marie DÉPLANCHE and Sébastien FAUCOU

11.1. Introduction

11.2. Main characteristics of the architecture description languages

11.3. ADLs and real-time systems

11.4. Outline of related works

11.5. The AADL language

11.6. Case study

11.7. Conclusion

11.8. Bibliography

List of Authors

Index

First published in Great Britain and the United States in 2008 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 6 Fitzroy Square London W1T 5DX UKwww.iste.co.ukJohn Wiley & Sons, Inc. 111 River Street Hoboken, NJ 07030 USAwww.wiley.com

© ISTE Ltd 2008

The rights of Stephan Merz and Nicolas Navet to be identified as the authors of this work have been asserted by them in accordance with the Copyright, Designs and Patents Act 1988.

Library of Congress Cataloging-in-Publication Data

Modeling and verification of real-time systems : formalisms and software tools / edited by Nicolas Navet, Stephan Merz.

p. cm.

Includes bibliographical references and index.

ISBN-13: 978-1-84821-013-4

1. Real-time data processing. 2. Computer software--Verification. 3. Formal methods (Computer science) I. Navet, Nicolas. II. Merz, Stephan.

QA76.54.M635 2008

004.01'51--dc22

2007045063

British Library Cataloguing-in-Publication Data

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

ISBN: 978-1-84821-013-4

Preface

The study of real-time systems has been recognized over the past 30 years as a discipline of its own whose research community is firmly established in academia as well as in industry. This book aims at presenting some fundamental problems, methods, and techniques of this domain, as well as questions open for research.

The field is mainly concerned with the control and analysis of dynamically evolving systems for which requirements of timeliness are paramount. Typical examples include systems for the production or transport of goods, materials, energy or information. Frequently, controllers for these systems are “embedded” in the sense that they are physically implemented within the environment with which they interact, such as a computerized controller in a plane or a car. This characteristic imposes strong constraints on space, cost, and energy consumption, which limits the computational power and the available memory for these devices, in contrast with traditional applications of computer science where resources usually grow exponentially according to Moore’s law. The design of real-time systems relies on techniques that originate in several disciplines, including control theory, operations research, software engineering, stochastic process analysis and others.

Software supporting real-time systems needs not only to compute the correct value of a given function, but it must also deliver these values at the right moment in order to ensure the safety and the required performance level of the overall system. Usually, this is implemented by imposing constraints (or deadlines) on the termination of certain activities. The verification techniques presented in this volume can help to ensure that deadlines are respected.

The chapters of this book present basic concepts and established techniques for modeling real-time systems and for verifying their properties. They concentrate on functional and timing requirements; the analysis of non-functional properties such as schedulability and Quality of Service guarantees would be a useful complement, but would require a separate volume. Formal methods of system design are based on mathematical principles and abstractions; they are a cornerstone for a “zero-default” discipline. However, their use for the development of real-world systems requires the use of efficient support tools. The chapters therefore emphasize the presentation of verification techniques and tools associated with the different specification methods, as well as the presentation of case studies that illustrate the application of the formalisms and the tools. The focus lies on model checking approaches, which attempt to provide a “push-button” approach to verification and integrate well into standard development processes. The main obstacle for the use of model checking in industrial-sized developments is the state-explosion problem, and several chapters describe techniques based on abstraction, reduction or compression that stretch the limits of the size of systems that can be handled.

Before verification can be applied, the system must be modeled in a formal description language such as (timed) Petri nets, timed automata or process algebra. The properties expected of a system are typically expressed in temporal logic or using automata as observers. Two main classes of properties are safety properties that, intuitively, express that nothing bad ever happens, and liveness properties that assert that something good eventually happens. The third step is the application of the verification algorithm itself to decide whether the properties hold over the model of the system or not; in the latter case, model checking generates a counter-example exhibiting a run of the system that violates the property.

Beyond verification, which compares two formal objects, the model should also be validated to ensure that it faithfully represents the system under development. One approach to validation is to decide healthiness properties of the model (for example, ensure that each component action can occur in a system run), and model checking is again useful here. In general, it is helpful to narrow the gap between the system description and its formal model, for example by writing a model in a high-level executable language or in a notation familiar to designers such as UML. The chapters of this book, written by researchers active in the fields, present different possible approaches to the problems of modeling, verification and validation, as well as open research questions.

Chapter 1, written by Bernard Berthomieu, Florent Peres and François Vernadat, explains the analysis of real-time systems based on timed Petri nets. It illustrates the high expressiveness of that formalism and the different, complementary verification techniques that are implemented in the Tina tool.

Chapter 2, Camille Constant, Thiery Jéron, Hervé Marchand and Vlad Rusu describe an approach that combines verification and conformance testing (on the actual implementation platform) of input/output symbolic transition systems. Disciplined approaches to testing are indeed a very valuable complement to formal verification for ensuring the correctness of an implementation. This is true in particular when the complexity of the models makes exhaustive verification impossible.

Chapters 3 and 4 are devoted to the presentation of model checking techniques. Starting with the canonical example of a lift controller, Stephan Merz presents the basic concepts and techniques of model checking for discrete state transition systems: temporal logics, the principles of model checking algorithms and their complexity, and strategies for mastering the state explosion problem. Patricia Bouyer and François Laroussinie focus on model checking for timed automata, the main semantic formalism for modeling real-time systems. They describe the formalism itself, timed modal and temporal logics, as well as some extensions and subclasses of timed automata. Finally, algorithms and data structures for the representation and verification of timed automata are introduced, and the modeling and verification environment Uppaal is described in some detail.

Using a model of an industrial drilling station as a running example, Radu Mateescu presents in Chapter 5 the functionalities of the CADP toolbox for modeling and verification. CADP is designed to model arbitrary asynchronous systems whose components run in parallel and communicate by message passing. The toolbox accepts models written in different formalisms, including networks of communicating automata or higher-level models written in Lotos. It implements a set of model transformations, simulation and verification algorithms, and offers the possibility to generate conformance tests for the implementation.

Chapter 6, written by Pascal Raymond, is devoted to the verification of programs written in the synchronous language Lustre with the help of the model checker Lesar. Synchronous languages enjoy ever more success for the development of reactive systems, of which real-time systems are a particular instance. Based on mathematical models of concurrency and time, synchronous languages provide a high-level abstraction for the programmer and are well-suited to formal verification.

In Chapter 7, Paul Caspi, Grégoire Hamon and Marc Pouzet go on to describe the language Lucid Synchrone that extends Lustre with constructs borrowed from functional languages, further augmenting expressiveness. The authors start by asking why synchronous languages are relevant for the design of critical systems. They give an account of the development of the Lucid language, and present in detail its primitives and the underlying theoretical concepts, illustrating them by several examples.

One of the most exciting developments over the past 15 years has been the emergence of techniques for the verification of probabilistic systems, intimately coupled with work on stochastic processes carried out in the realm of performance evaluation. Probabilistic models are very useful because they add quantitative information above the non-deterministic representation of the behavior of system components and the environment. They can also be used to determine system parameters such as queue sizes, as a function of the desired failure guarantees. Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston lay the bases in Chapter 8 by defining probabilistic timed automata and extending the model checking algorithms for ordinary timed automata to handle probabilistic models. The case study of the IEEE FireWire Root Contention Protocol illustrates the application of these techniques. In Chapter 9, Serge Haddad and Patrice Moreaux give an overview of verification techniques for probabilistic systems: discrete and continuous-time Markov chains, stochastic Petri nets, Markov decision processes and associated temporal logics. They also cover some of the main tools used in this domain, including GreatSPN, ETMCC and Prism.

Chapter 10, written by Marius Bozga, Susanne Graf, Laurent Mounier and Iulian Ober, presents the IF toolset, a tool environment for modeling and verifying real-time systems centered around a common internal description language based on communicating timed automata. User-level specifications written in languages such as SDL or UML are translated into this internal representation and can be subject to analysis using algorithms of static analysis, reduction and model checking. An extended case study from the aerospace domain based on joint work with EADS concludes the chapter.

Chapter 11, written by Anne-Marie Déplanche and Sébastien Faucou, is dedicated to the architecture description language AADL, originally designed and standardized for the avionic and aerospace domains, but which is an excellent candidate for arbitrary real-time systems. Architectural descriptions can serve as a reference for all actors involved in system design; they contain the information needed for simulation, formal verification and testing. The authors examine the specific requirements for describing real-time systems and then present the AADL and its support tools. Their use is illustrated with the help of a case study of a closed-loop control system.

We would like to express our gratitude to all of the authors for the time and energy they have devoted to presenting their topic. We are also grateful to ISTE Ltd. for having accepted to publish this volume and for their assistance during the editorial phase.

We hope that you, the readers of this volume, will find it an interesting source of inspiration for your own research or applications, and that it will serve as a reliable, complete and well-documented source of information on real-time systems.

Stephan MERZ and Nicolas NAVET

INRIA Nancy Grand Est and LORIA

Nancy, France

Chapter written by Stephan MERZ and Nicolas NAVET.