REAL-TIME SYSTEMS Formal Specification and Automatic Verificatio....pdf

发布时间：2022-05-30 发布人：admin 分类：说明书资料大小：1.73M 资料格式：pdf 举报版权申诉

garbird-1604057-4744302543462527858.pdf-第1页.png

第1页 / 共338页

garbird-1604057-4744302543462527858.pdf-第2页.png

第2页 / 共338页

garbird-1604057-4744302543462527858.pdf-第3页.png

第3页 / 共338页

garbird-1604057-4744302543462527858.pdf-第4页.png

第4页 / 共338页

garbird-1604057-4744302543462527858.pdf-第5页.png

第5页 / 共338页

garbird-1604057-4744302543462527858.pdf-第6页.png

第6页 / 共338页

garbird-1604057-4744302543462527858.pdf-第7页.png

第7页 / 共338页

garbird-1604057-4744302543462527858.pdf-第8页.png

第8页 / 共338页

Cover

Half-title

Title

Contents

Preface

Structure of this book

How to read this book

Intended audience

Courses based on this book

Acknowledgements

List of symbols

1 Introduction

1.1 What is a real-time system?

1.2 System properties

1.3 Generalised railroad crossing

1.3.1 The problem

1.3.2 Formalisation

1.4 Gas burner

1.4.1 The problem

1.4.2 Formalisation

1.4.3 Design

1.5 Aims of this book

1.5.1 Duration Calculus

1.5.2 Timed automata

1.5.3 PLC-Automata

1.5.4 Tying it all together

1.6 Exercises

1.7 Bibliographic remarks

2 Duration Calculus

2.1 Preview

2.2 Syntax and semantics

2.2.1 Symbols

2.2.2 State assertions

2.2.3 Terms

2.2.4 Formulas

2.2.5 Validity, satisfiability, and realisability

2.3 Specification and correctness proof

2.3.1 Gas burner revisited

2.4 Proof rules

2.4.1 Predicate calculus

2.4.2 Equality

2.4.4 Interval logic

2.4.5 Durations

2.4.6 Induction

2.4.7 Application to the gas burner

2.4.8 Further rules

Interval logic

Modal operators

Duration operator

Classic induction rule

2.5 Exercises

2.6 Bibliographic remarks

3 Properties and subsets of DC

3.1 Decidability results

3.1.1 Decidability for discrete time

Expressiveness of RDC

Realisability problem

Construction of L(F)

3.1.2 Undecidability for continuous time

Two-counter machines

Reduction of two-counter machines to DC

Discussion

3.2 Implementables

3.2.1 A controller for the gas burner

3.2.2 Correctness proof

3.3 Constraint Diagrams

3.3.1 Syntax and semantics

Phase sequence constraints

Length requirements

3.3.2 Generalised railroad crossing revisited

3.3.3 A real-time filter

3.3.4 Expressiveness

3.4 Exercises

3.5 Bibliographic remarks

4 Timed automata

4.1 Timed automata

4.2 Networks of timed automata

4.3 Reachability is decidable

4.3.1 Location reachability

4.3.2 Constraint reachability

4.4 The model checker UPPAAL

4.4.1 Data variables

4.4.2 Structuring facilities

4.4.3 Restricting nondeterminism

4.4.4 Operational semantics of networks

4.4.5 The logic of UPPAAL

4.5 Exercises

4.6 Bibliographic remarks

5 PLC-Automata

5.1 Programmable Logic Controllers

5.2 PLC-Automata

5.3 Translation into PLC source code

5.4 Duration Calculus semantics

5.4.1 Reaction times

5.5 Synthesis from DC implementables

5.5.1 Synthesis algorithm

5.6 Extensions of PLC-Automata

5.6.1 Hierarchical PLC-Automata

5.6.2 Data and timer variables

5.6.3 Networks of PLC-Automata

Parallel composition

Sequential composition

5.7 Exercises

5.8 Bibliographic remarks

6 Automatic verification

6.1 The approach

6.2 Requirements

6.2.1 Railroad crossing

6.2.2 Constructing test automata

Safety

Utility

6.2.3 Discussion

6.2.4 Automatically generated test automata

Test automata for DC implementables

Test automata for counterexample formulas

6.3 Specification

6.3.1 Railroad crossing

6.3.2 Timed automata semantics of PLC-Automata

6.4 Verification

6.4.1 Railroad crossing

Verifying safety

Verifying utility

6.4.2 Discussion

6.4.3 Separated assumptions

Application to railroad crossing

Discussion

6.4.4 Plant, sensors, and actuators

Application to railroad crossing

6.5 The tool Moby/RT

6.6 Summary

6.7 Exercises

6.8 Bibliographic remarks

Notations

Logic

Sets

Relations

Functions

Real numbers

Words and languages

Finite automata and regular languages

Transition systems

Bibliographic remarks

Bibliography

Index

This page intentionally left blank

Real-Time Systems Real-time systems need to react to certain input stimuli within given time bounds. For example, an airbag in a car has to unfold within 300 milliseconds in a crash. There are many embedded safety-critical applications and each requires real-time specification techniques. This textbook introduces three of these techniques, based on logic and automata: Duration Calculus, Timed Automata, and PLC-Automata. The techniques are brought together to form a seamless design flow, from real- time requirements specified in the Duration Calculus, via designs specified by PLC- Automata, and into source code for hardware platforms of embedded systems. The syntax, semantics, and proof methods of the specification techniques are introduced; their most important properties are established; and real-life examples illustrate their use. Detailed case studies and exercises conclude each chapter. Ideal for students of real-time systems or embedded systems, this text will also be of great interest to researchers and professionals in transportation and automation. E.-R. OLDEROG is Professor of Computer Science at the University of Oldenburg, Germany. In 1994 he was awarded the Leibniz Prize of the German Research Council (DFG). H. DIERKS is a researcher currently working with OFFIS, a technology transfer institute for computer science in Oldenburg, Germany.

REAL-TIME SYSTEMS Formal Specification and Automatic Verification ERNST-RÜDIGER OLDEROG 1 AND HENNING DIERKS 2 1 Department of Computing Science, University of Oldenburg, Germany 2 OFFIS, Oldenburg, Germany

CAMBRIDGE UNIVERSITY PRESS Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, São Paulo Cambridge University Press The Edinburgh Building, Cambridge CB2 8RU, UK Published in the United States of America by Cambridge University Press, New York www.cambridge.org Information on this title: www.cambridge.org/9780521883337 © E.-R. Olderog and H. Dierks 2008 This publication is in copyright. Subject to statutory exception and to the provision of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. First published in print format 2008 ISBN-13 978-0-511-42921-7 eBook (EBL) ISBN-13 978-0-521-88333-7 hardback Cambridge University Press has no responsibility for the persistence or accuracy of urls for external or third-party internet websites referred to in this publication, and does not guarantee that any content on such websites is, or will remain, accurate or appropriate.

Contents Preface Acknowledgements List of symbols System properties Introduction 1.1 What is a real-time system? 1.2 1.3 Generalised railroad crossing 1.4 Gas burner 1.5 Aims of this book 1.6 Exercises 1.7 Bibliographic remarks Syntax and semantics Speciﬁcation and correctness proof Duration Calculus 2.1 Preview 2.2 2.3 2.4 Proof rules 2.5 Exercises 2.6 Bibliographic remarks Implementables Properties and subsets of DC 3.1 Decidability results 3.2 3.3 Constraint Diagrams 3.4 Exercises 3.5 Bibliographic remarks Timed automata 4.1 Timed automata v 1 2 3 4 page vii xii xv 1 1 4 7 12 15 20 21 28 28 31 47 53 75 79 81 81 97 110 128 132 134 134

vi 5 6 Contents 4.2 Networks of timed automata 4.3 Reachability is decidable 4.4 The model checker UPPAAL 4.5 Exercises 4.6 Bibliographic remarks PLC-Automata 5.1 Programmable Logic Controllers 5.2 PLC-Automata 5.3 Translation into PLC source code 5.4 Duration Calculus semantics 5.5 5.6 Extensions of PLC-Automata 5.7 Exercises 5.8 Bibliographic remarks Synthesis from DC implementables Automatic veriﬁcation 6.1 The approach 6.2 Requirements 6.3 Speciﬁcation 6.4 Veriﬁcation 6.5 The tool Moby/RT 6.6 Summary 6.7 Exercises 6.8 Bibliographic remarks Notations Bibliography Index 145 153 165 184 187 189 190 192 197 201 212 227 237 240 241 241 243 257 265 283 287 289 290 293 304 313

分享到：

赞收藏

资料库

REAL-TIME SYSTEMS Formal Specification and Automatic Verificatio....pdf

相关推荐

开发技术

热门标签

最新资料