Communicating Embedded Systems E-Book

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

Seitenzahl: 479

Veröffentlichungsjahr: 2013

Beschreibung

The increased complexity of embedded systems coupled with quick design cycles to accommodate faster time-to-market requires increased system design productivity that involves both model-based design and tool-supported methodologies. Formal methods are mathematically-based techniques and provide a clean framework in which to express requirements and models of the systems, taking into account discrete, stochastic and continuous (timed or hybrid) parameters with increasingly efficient tools. This book deals with these formal methods applied to communicating embedded systems by presenting the related industrial challenges and the issues of modeling, model-checking, diagnosis and control synthesis, and by describing the main associated automated tools.

Leseprobe

Contents

Preface

Chapter 1. Models for Real-Time Embedded Systems

1.1. Introduction

1.2. Notations, languages and timed transition systems

1.3. Timed models

1.4. Models with stopwatches

1.5. Conclusion

1.6. Bibliography

Chapter 2. Timed Model-Checking

2.1. Introduction

2.2. Timed models

2.3. Timed logics

2.4. Timed model-checking

2.5. Conclusion

2.6. Bibliography

Chapter 3. Control of Timed Systems

3.1. Introduction

3.2. Timed games

3.3. Computation of winning states and strategies

3.4. Zeno strategies

3.5. Implementability

3.6. Specification of control objectives

3.7. Optimal control

3.8. Efficient algorithms for controller synthesis

3.9. Partial observation

3.10. Changing game rules

3.11. Bibliography

Chapter 4. Fault Diagnosis of Timed Systems

4.1. Introduction

4.2. Notations

4.3. Fault diagnosis problems

4.4. Fault diagnosis for discrete event systems

4.5. Fault diagnosis for timed systems

4.6. Other results and open problems

4.7. Bibliography

Chapter 5. Quantitative Verification of Markov Chains

5.1. Introduction

5.2. Performance evaluation of Markov models

5.3. Verification of discrete time Markov chain

5.4. Verification of continuous time Markov chain

5.5. State of the art in the quantitative evaluation of Markov chains

5.6. Bibliography

Chapter 6. Tools for Model-Checking Timed Systems

6.1. Introduction

6.2. Uppaal

6.3. Uppaal-CORA

6.4. Uppaal-TIGA

6.5. TAPAAL

6.6. Roméo: a tool for the analysis of timed extensions of Petri nets

6.7. Bibliography

Chapter 7. Tools for the Analysis of Hybrid Models

7.1. Introduction

7.2. Hybrid automata and reachability

7.3. Linear hybrid automata

7.4. Piecewise affine hybrid systems

7.5. Hybridization techniques for reachability computations

7.6. Bibliography

List of Authors

Index

First published 2008 in France by Hermes Science/Lavoisier entitled: Approches formelles des systèmes embarqués communicants © LAVOISIER 2008

First published 2010 in Great Britain and the United States 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 Ltd27-37 St George’s RoadLondon SW19 4EUUK

John Wiley & Sons, Inc.111 River Street Hoboken, NJ 07030USA

www.iste.co.uk

www.wiley.com

© ISTE Ltd 2010

The rights of Claude Jard and Olivier H. Roux 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

Approches formelles des systèmes embarqués communicants. English

Communicating embedded systems : software and design : formal methods / edited by Claude Jard, Olivier H. Roux. p. cm.

Includes bibliographical references and index.

ISBN 978-1-84821-143-8

1. Embedded computer systems--Programming. 2. Embedded computer systems--Design and construction. 3. Computer software--Development. 4. Formal methods (Computer science) I. Jard, Claude. II. Roux, Olivier H. III. Title.

TK7895.E42A387 2009

621.39’2--dc22

2009026282

British Library Cataloguing-in-Publication Data

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

ISBN 978-1-84821-143-8

Edited and formatted by Aptara Corporation, New Delhi, India

Preface1

This book stems from the global scientific priority put on the development of the research on communicating embedded systems. A worldwide scientific community is motivated by this theme and taking care of the development and promotion of formal approaches based on mathematical models and implemented by computer-automated tools. The main objective is to rise to the ever-growing challenge of mastering the quality of upcoming computer systems.

The computer systems concerned are:

– critical: a strong demand for quality comes from their handling of critical functions or a large-scale deployment;

– complex: their correct functioning depends on the careful use of resources that are mutually dependent over time. So their analysis on the basis of a formal model appears to be the most solid scientific approach.

This motivation is not new as the formal methods community has already produced a great number of results, mainly dedicated to the tasks of formal specification, verification and proof, and test synthesis. Several studies have been conducted with industrial partners, and a few of them have finally initiated some industrial software development processes. However, it remains mostly insufficient with respect to the increasing computer-related risks. Some progress is expected on the development and promotion of formal methods used in concrete computer-related problems and objects, as well as in the systematic research of new application fields and methods. Beyond the “traditional” application of formal methods to the conception of safe software, a significant impact can already be observed on areas of compiling and synthesis of controllers, diagnosis and supervision, system engineering, or security and safety engineering.

Considering the widely acknowledged importance of the human and economic interests at stake with the future embedded systems (encompassing many economic sectors that have yet to be discovered), it is necessary to take particular interest in widely diffusing the technical advances of the domain. This is precisely the aim of this book arranged in an unified manner, such as the elements related to the current problems of embedded systems, the presentation of the achievements of new research directions on models and their use, and the presentation of available software tools. The contributing authors are renowned specialists in their respective fields. We have taken care of the coordination of the whole book, as leaders of the French national action AFSEC (“Formal Approaches for Communicating Embedded Systems”), supported by the CNRS.

1 Chapter written by Claude JARD and Olivier H. ROUX.

Chapter 1

Models for Real-Time Embedded Systems1

1.1. Introduction

The class of real-time embedded systems contains software components that control an application by reacting to stimuli received from a changing environment. Therefore, they are often referred to as reactive systems. The reaction time of these systems must be small enough to cope with the internal dynamics of the controlled or monitored application. They must thus obey the strong timing requirements, and it is crucial to ensure their correctness from both the functional and temporal points of view.

Real-time applications are often regarded as safety critical because their failures may either involve substantial financial losses or endanger human lives. It is also important to detect any error at an early stage to minimize the costs involved in its correction. This issue can be addressed by several approaches. Let us consider the following two approaches: in the first approach, from the application requirements, a model for the application and its expected properties are derived. Then a controller is proposed, using expert knowledge, to restrict the application behavior in order to satisfy the given properties. The next step is to validate the proposed controller using different techniques such as testing, theorem proving, formal verification, etc. If the controller is not acceptable, then it has to be reworked on the basis of the knowledge gained from the reported failures or counter-examples. In the second approach, the controller will be synthesized automatically from the formal model of the application. If such a controller exists, which may not be the case, for example, if the requirements are incoherent, then a method to implement should be derived. Alternatively, if the controller model cannot be implemented, the problem has to be reworked from the beginning.

In this chapter, we will address the formal methods relating to these two approaches and those based on state-transition models. The models presented here deal with instantaneous actions and real-valued variables. The former approach usually models relevant events in the systems such as those relative to the command of the actuators or to the measures of sensors and the latter approach models durations of processes. These models thus describe subclasses of real-time embedded systems.

1.1.1. Model-checking and control problems

The requirements of a computer application are usually given as a natural language document. Therefore, they are subject to the interpretation of the persons who will derive the specification from them, which may result in many errors. Moreover, it is impossible for a conceptor to understand all possible interactions of the components of any reasonably sized application.

Formal methods aim at providing a mathematical framework for a clear, non-ambiguous and precise description of the systems and programs we want to develop. In this framework, the system is described by a labeled transition system or any model abstracting such a systems, e.g. automata, Petri nets, process algebra, etc. The specification may be either described in the same manner or as a property expressed in a suitable logic, such as linear temporal logics (LTL) or tree-based temporal logics (CTL), or even their timed extensions. A classical example of a real-time property is the bounded response property which requires that for the execution of the system, whenever some predicate P0 on the states of the system becomes true, then some other predicate P1 will become true, within n time units.

Among formal methods, model-checking is an automatic procedure that verifies whether a system satisfies a given temporal logic property. It usually works by exploring parts of the set of possible states of the system.

Controller synthesis consists of automatically synthesizing a program (the controller) that leads the interaction mechanisms with the environment (the application) and guarantees a safe and correct behavior of the coupled system. The set of actions of the system is partitioned into two disjoint subsets: a set of controllable actions and a set of uncontrollable actions. They usually correspond to the commands to actuators and the measures of sensors, respectively. The controller of the application may act on the controllable actions (and only on them) and the resulting system is said to be (as opposed to the system without the controller, which is said to be ).