หน้าหลัก
RealTime Systems: Formal Specification and Automatic Verification
RealTime Systems: Formal Specification and Automatic Verification
ErnstRüdiger Olderog, Henning Dierks
0 /
0
คุณชอบหนังสือเล่มนี้มากแค่ไหน
คุณภาพของไฟล์เป็นอย่างไรบ้าง
ดาวน์โหลดหนังสือเพื่อประเมินคุณภาพของไฟล์
คุณภาพของไฟล์ที่คุณดาวน์โหลดมาเป็นอย่างไรบ้าง
Realtime 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 safetycritical applications and each requires realtime specification techniques. This text introduces three of these techniques, based on logic and automata: duration calculus, timed automata, and PLCautomata. The techniques are brought together to form a seamless design flow, from realtime requirements specified in the duration calculus; via designs specified by PLCautomata; 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 reallife examples illustrate their use. Detailed case studies and exercises conclude each chapter. Ideal for students of realtime systems or embedded systems, this text will also be of great interest to researchers and professionals in transportation and automation.
หมวดหมู่:
ปี:
2008
ฉบับพิมพ์ครั้งที่:
1
สำนักพิมพ์:
Cambridge University Press
ภาษา:
english
จำนวนหน้า:
338
ISBN 10:
0521883334
ISBN 13:
9780521883337
ไฟล์:
PDF, 1.73 MB
แท็กของคุณ:
ดาวน์โหลด (pdf, 1.73 MB)
 เปิดในเบราว์เซอร์
 Checking other formats...
 แปลงไปเป็น EPUB
 แปลงไปเป็น FB2
 แปลงไปเป็น MOBI
 แปลงไปเป็น TXT
 แปลงไปเป็น RTF
 ไฟล์ที่แปลงแล้วอาจแตกต่างไปจากต้นฉบับ หากเป็นไปได้ให้ดาวน์โหลดไฟล์ในรูปแบบดั้งเดิม.
รายงานปัญหา
This book has a different problem? Report it to us
กด ใช่ หาก
กด ใช่ หาก
กด ใช่ หาก
กด ใช่ หาก
คุณเปิดไฟล์ได้สำเร็จ
ไฟล์นี้เป็นไฟล์หนังสือ (การ์ตูนก็ได้เช่นกัน)
เนื้อหาหนังสือเล่มนี้มีความเหมาะสม
ชื่อเรื่อง ชื่อผู้แต่ง และ ภาษาในไฟล์ตรงตามคำอธิบายหนังสือ ละเว้นช่องอื่น ๆ เพราะมันเป็นช่องรอง!
กด ไม่ หาก
กด ไม่ หาก
กด ไม่ หาก
กด ไม่ หาก
 ไฟล์นี้เสีย
 ไฟล์นี้ได้รับการป้องกันด้วย DRM
 ไฟล์นี้ไม่ใช่หนังสือ (เช่น xls, html, xml)
 ไฟล์นี้เป็นบทความ
 ไฟล์นี้เป็นข้อความที่ตัดตอนมาจากหนังสือ
 ไฟล์นี้เป็นนิตยสาร
 ไฟล์นี้เป็นแบบทดสอบ
 ไฟล์นี้เป็นสแปม
คุณเชื่อว่าเนื้อหาหนังสือเล่มนี้ไม่เหมาะสมและควรถูกบล็อก
ชื่อเรื่อง ชื่อผู้แต่ง หรือ ภาษาในไฟล์ไม่ตรงตามคำอธิบายหนังสือ ละเว้นช่องอื่น ๆ
Are you sure you want to report this book? Please specify the reason below
Change your answer
Thanks for your participation!
Together we will make our library even better
Together we will make our library even better
ไฟล์จะถูกส่งไปยังที่อยู่อีเมลของคุณ อาจใช้เวลา 15 นาที ก่อนที่คุณจะได้รับ
ไฟล์จะถูกส่งไปยังบัญชี Kindle ของคุณ อาจใช้เวลา 15 นาที ก่อนที่คุณจะได้รับ
หมายเหตุ: คุณต้องยืนยันหนังสือทุกเล่มที่คุณจะส่งไปยัง Kindle ของคุณ ตรวจสอบกล่องจดหมายเข้าของคุณเพื่อค้นหาอีเมลยืนยันจาก Amazon Kindle Support
หมายเหตุ: คุณต้องยืนยันหนังสือทุกเล่มที่คุณจะส่งไปยัง Kindle ของคุณ ตรวจสอบกล่องจดหมายเข้าของคุณเพื่อค้นหาอีเมลยืนยันจาก Amazon Kindle Support
กำลังแปลงเป็น อยู่
การแปลงเป็น ล้มเหลว
คุณอาจสนใจ Powered by Rec2Me
บุ๊กลิสต์ที่เกี่ยวข้อง
0 comments
คุณเขียนบทวิจารณ์หนังสือ และแบ่งปันประสบการณ์ของคุณได้ ผู้อ่านคนอื่น ๆ มักจะสนใจความคิดเห็นของคุณเกี่ยวกับหนังสือที่คุณอ่าน ไม่ว่าคุณจะชอบหนังสือเล่มนี้หรือไม่ก็ตาม หากคุณให้ความคิดเห็นที่ตรงไปตรงมาและมีรายละเอียดแล้ว ผู้คนจะได้พบกับหนังสือเล่มใหม่ที่เหมาะสมกับพวกเขา
1

2

This page intentionally left blank RealTime Systems Realtime 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 safetycritical applications and each requires realtime specification techniques. This textbook introduces three of these techniques, based on logic and automata: Duration Calculus, Timed Automata, and PLCAutomata. The techniques are brought together to form a seamless design flow, from realtime requirements specified in the Duration Calculus, via designs specified by PLCAutomata, 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 reallife examples illustrate their use. Detailed case studies and exercises conclude each chapter. Ideal for students of realtime 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. REALTIME SYSTEMS Formal Specification and Automatic Verification ERNSTRÜ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 ISBN13 9780511429217 eBook (EBL) ISBN13 hardback 9780521883337 Cambridge University Press has no responsibility for the persistence or accuracy of urls for external or thirdparty 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 page vii Preface Acknowledgements xii List of symbols xv 1 Introduction 1.1 What is a realtime system? 1.2 System properties 1.3 Generalised railroad crossing 1.4 Gas burner 1.5 Aims of this book 1.6 Exercises 1.7 Bibliographic remarks 1 1 4 7 12 15 20 21 2 Duration Calculus 2.1 Preview 2.2 Syntax and semantics 2.3 Speciﬁcation and correctness proof 2.4 Proof rules 2.5 Exercises 2.6 Bibliographic remarks 28 28 31 47 53 75 79 3 Properties and subsets of DC 3.1 Decidability results 3.2 Implementables 3.3 Constraint Diagrams 3.4 Exercises 3.5 Bibliographic remarks 81 81 97 110 128 132 4 Timed automata 4.1 Timed automata 134 134 v vi Contents 4.2 4.3 4.4 4.5 4.6 Networks of timed automata Reachability is decidable The model checker UPPAAL Exercises Bibliographic remarks 145 153 165 184 187 5 PLCAutomata 5.1 Programmable Logic Controllers 5.2 PLCAutomata 5.3 Translation into PLC source code 5.4 Duration Calculus semantics 5.5 Synthesis from DC implementables 5.6 Extensions of PLCAutomata 5.7 Exercises 5.8 Bibliographic remarks 189 190 192 197 201 212 227 237 240 6 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 241 241 243 257 265 283 287 289 290 Notations 293 Bibliography 304 Index 313 Preface Computers are used more and more to provide highquality and reliable products and services, and to control and optimise production processes. Such computers are often embedded into the products and thus hidden to the human user. Examples are computercontrolled washing machines or gas burners, electronic control units in cars needed for operating airbags and braking systems, signalling systems for highspeed trains, or robots and automatic transport vehicles in industrial production lines. In these systems the computer continuously interacts with a physical environment or plant. Such systems are thus called reactive systems. Moreover, common to all these applications is that the computer reactions should obey certain timing constraints. For example, an airbag has to unfold within milliseconds, not too early and not too late. Reactive systems with such constraints are called realtime systems. They often appear in safetycritical applications where a malfunction of the controller will cause damage and risk the lives of people. This is immediately clear for all applications in the transport sector where computers control cars, trains and planes. Therefore the design of realtime systems requires a high degree of precision. Here formal methods based on mathematical models of the system under design are helpful. They allow the designer to specify the system at diﬀerent levels of abstraction and to formally verify the consistency of these speciﬁcations before implementing them. In recent years signiﬁcant advances have been made in the maturity of formal methods that can be applied to realtime systems. Structure of this book In this advanced textbook we shall present three such formal approaches: vii viii Preface • Duration Calculus (DC for short), a logic and calculus for specifying highlevel requirements of realtime systems; • timed automata (TA for short), a statetransition model of realtime systems with the advantage of elaborate tool support for the automatic veriﬁcation of realtime properties; • PLCAutomata, a statetransition model of realtime systems with the advantage of being implementable, for example in the programming language C or on Programmable Logic Controllers (PLCs for short), a hardware platform that is widespread in the automation industry. This book is the ﬁrst one that presents the above three approaches to the speciﬁcation of realtime systems in a coherent way. This is achieved by combining the approaches into a design method for realtime systems, reaching from requirements down to executable code as illustrated in Figure 0.1. Here: • Realtime requirements are speciﬁed in the Duration Calculus or subsets thereof. • Designs are speciﬁed by PLCAutomata. • Implementations are written as C programs with timers or as programs that are executable on PLCs. • Automatic veriﬁcation of requirements is performed using the modelchecking tool UPPAAL for timed automata. • A tool Moby/RT, built for PLCAutomata, allows the user to invoke algorithms for generating C or PLC code from such automata, and to automatically verify properties speciﬁed in a subset of Duration Calculus by using UPPAAL as a backend veriﬁcation engine. The connection is that PLCAutomata have both a semantics in terms of the Duration Calculus and an equivalent one in terms of timed automata. To verify that a PLCAutomaton satisﬁes a given realtime requirement expressed in the Duration Calculus, there are two possibilities: either a proof can be conducted in the Duration Calculus exploiting the corresponding semantics of the PLCAutomaton, or, for certain types of requirement, an automatic veriﬁcation is possible using the tool UPPAAL and the timed automata semantics of the PLCAutomaton. How to read this book The titles and dependencies of the chapters are shown in Figure 0.2. First, the introduction in Chapter 1 should be read. Here two case studies (railroad Preface Requirements ix DC Subsets of DC TA Designs Implementations Automatic veriﬁcation PLCAutomata C code or PLC code Fig. 0.1. Overview of design method crossing and gas burner) provide a feeling for the delicacies of realtime systems. Then one can continue with Chapter 2 (Duration Calculus) or Chapter 4 (Timed automata). Chapter 2 presents the basic knowledge of the Duration Calculus. First, the syntax and semantics of the logic are deﬁned. Then the proof rules of the calculus are introduced, including a simple induction rule. These rules are applied to the case study of the gas burner. Chapter 3 presents advanced topics on the Duration Calculus. First, decidability results are discussed for the cases of discrete and continuous time domains. Then a subset of the Duration Calculus that is closer to the implementation level is presented, the socalled DC implementables. Finally, Constraint Diagrams are introduced as a graphic representation for requirements with a semantics in the Duration Calculus. Chapter 4 presents the basic facts of timed automata. In particular, the most prominent result of timed automata is shown: the decidability of the reachability problem. It is then explained which variant of timed automata and properties the model checker UPPAAL can decide. Chapter 5 introduces PLCAutomata as a class of implementable realtime automata. First, these automata are motivated using an example of a realtime ﬁlter. Then it is described how PLCAutomata can be compiled into code that is executable on Programmable Logic Controllers (PLCs). To link the PLCAutomata with the Duration Calculus, their semantics are deﬁned in terms of this logic. As a consequence, a general result estimating the reaction times of PLCAutomata to input stimuli can be proved. Also, an x Preface algorithm is discussed that synthesises a PLCAutomaton from a given set of DC implementables provided this set is consistent. Finally, hierarchical PLCAutomata are deﬁned. Chapter 6 ties together the results of Chapters 4 and 5 for the purposes of automatic veriﬁcation. It turns out that certain realtime properties of PLCAutomata can be proven automatically using the model checker UPPAAL for timed automata. To this end, an alternative and equivalent semantics of PLCAutomata in terms of timed automata is deﬁned. Then it is shown that realtime requirements expressed in a subset of Constraint Diagrams can be veriﬁed against PLCAutomata by checking the reachability of certain states with UPPAAL. This is all supported by the tool Moby/RT, which is described brieﬂy as well. Also, Moby/RT enables the user to compile PLCAutomata into PLC code or C code. 1 Introduction 2 Duration Calculus 3 Properties and subsets 4 Timed automata 5 PLCAutomata 6 Automatic veriﬁcation Fig. 0.2. Dependency of chapters Actually, only Section 5.5 (Synthesis) of Chapter 5 depends on Section 3.2 (DC implementables) of Chapter 3. The remainder of Chapter 5 can thus also be read immediately after Chapter 2. Intended audience This textbook is appropriate for either a course on formal methods for realtime systems in the upper division of undergraduate studies or for graduate Preface xi studies in computer science and engineering. It can also be used for self study, and will be of interest for engineers of embedded realtime systems. Readers are expected to have a basic understanding of mathematical and logical notations. Courses based on this book Our own course on realtime systems at the University of Oldenburg is for M.Sc. and advanced B.Sc. students in computer science with an interest in embedded systems; it proceeds as follows: Course at Oldenburg Introduction Duration Calculus Properties and subsets Timed automata PLCAutomata Automatic veriﬁcation 1 2 3.1–3.2 4 5.1–5.5 6 (only short indication) The course takes one semester with three hours of lectures and one hour of exercises per week. At Oldenburg an indepth study of Chapter 6 (Automatic veriﬁcation) with the use of the tools UPPAAL and Moby/RT is delegated to practical work of the students in separate labs on realtime systems. There LEGO Mindstorm robots are used for implementing the systems. Once desirable realtime properties have been veriﬁed, the compiler from PLCAutomata to C is applied to generate code for the LEGO Mindstorms. An alternative usage of the material of this book could be in (part of) a course on timed automata as follows: Course based on timed automata Introduction Timed automata PLCAutomata Automatic veriﬁcation 1 4 5.1–5.3 and 5.6 6 Further information and additional material can be found on the webpage http://csd.informatik.unioldenburg.de/rtbook. Acknowledgements Our ﬁrst inspiring contacts with realtime systems were in the context of the basic research project ProCoS (Provably Correct Systems) funded by the European Commission from 1989 to 1995. This project was planned by Dines Bjørner (Technical University of Denmark), Tony Hoare (Oxford University), and Hans Langmaack (University of Kiel). Its goal was to develop a mathematical basis for the development of embedded, realtime, computer systems. Returning from a sabbatical at the University of Austin at Texas, Tony Hoare was impressed by the work of Robert S. Boyer and J Strother Moore on mechanical veriﬁcation exempliﬁed in a case study known as the “CLInc Stack”. Talking to Dines Bjørner and Hans Langmaack, a project on the foundation of veriﬁcation of manylayered systems was conceived: ProCoS. The diﬀerent levels of abstraction studied in this project became known as the “ProCoS Tower”. They comprise (informal) expectations, (formal) requirements, (formal) system speciﬁcations, programs (occam), machine code (for transputers), and circuit diagrams (netlists). During the project the case study of a gas burner was deﬁned in collaboration with a Danish gas burner manufacturer. At the project start in 1989 the ﬁrst author of this book moved from Kiel to Oldenburg to take up a professorship in computing science at the University of Oldenburg and became one of the site leaders of ProCoS. He is very grateful for six rewarding years of research contacts with the members of the ProCoS project group, in particular Hans Langmaack, Tony Hoare, Dines Bjørner, Zhou Chaochen, He Jifeng, Jonathan Bowen, Michael R. Hansen, Anders P. Ravn, Hans Rischel, Kirsten M. Hansen, Martin Fränzle, Markus MüllerOlm, Stephan Rössig, and Michael Schenke. Two highlights evolved during the ProCoS project: the case study of the gas burner and the Duration Calculus, both featuring prominently in this book. xii Acknowledgements xiii In the ﬁrst years of ProCoS the second author of this book was a student of computing science and mathematics at Oldenburg. His ﬁrst contact with the realtime systems of ProCoS was during his master thesis on “The production cell as a veriﬁed realtime system” – formalised using the Duration Calculus. The next decisive step was the collaborative project UniForM (Universal Workbench for Formal Methods) together with Bernd KriegBrückner and Jan Peleska (University of Bremen) as well as Alexander Baer and Wolfgang Nowak (company Elpro AG in Berlin). One of the challenges of this project was to develop a formal method to support the realtime programming of tram control systems targeted at Programmable Logic Controllers. Motivated by this challenge the second author developed the concept of a PLCAutomaton, which serves for design speciﬁcations in this book. Inspired by ProCoS and UniForM the research on speciﬁcation and veriﬁcation of realtime systems gained momentum at our group on “Correct System Design” at Oldenburg. In particular, we wish to thank Cheryl Kleuker, who contributed Constraint Diagrams, Jochen Hoenicke, who can spot even subtle errors in a minute, and Andreas Schäfer, who saw how to extend the Duration Calculus to cope with space and time. Under the guidance of Josef Tapken the tool Moby/RT was developed to provide support for the theory presented in this book. We are particularly grateful to the following people who helped create this tool: Hans Fleischhack, Marc Lettrari, Michael Möller, Marco Oetken, Josef Tapken, and Tobe Toben. The second author spent an extended research visit at the Aalborg University to work with the UPPAAL group on automatic veriﬁcation and planning of timed automata. He would like to thank Kim Larsen, Gerd Behrmann, Alexandre David, Anders P. Ravn, Wang Yi, and Paul Petterson for inspiring cooperation. Both authors are pleased to acknowledge the research momentum gained by the Collaborative Research Center AVACS (Automatic Veriﬁcation and Analysis of Complex Systems) which has been funded by the German Research Council (DFG) since 2004. AVACS groups at the universities of Oldenburg, Freiburg and Saarbrücken, as well as the MaxPlanck Institute for Informatics in Saarbrücken, address automatic veriﬁcation and analysis of realtime systems, hybrid systems, and systems of systems. In the research area of realtime systems we would like to thank our close colleagues Werner Damm, Bernd Becker, Reinhard Wilhelm, Johannes Faber, Roland Meyer, Ingo Brückner, Heike Wehrheim, Bernd Finkbeiner, Andreas Podelski, Andrey Rybalchenko, Viorica SofroniStokkermans, Bernhard Nebel, Jörg Hoﬀmann, and Sebastian Kupferschmid. We also thank WillemPaul xiv Acknowledgements de Roever for his support of this largescale project and for many refreshing remarks and suggestions over the years. Everyone who has written a book knows how diﬃcult it is to ﬁnd the time to work intensively on the manuscript. Very helpful in this respect was a sabbatical of the ﬁrst author in the winter semester 2004/05 at ETH Zürich. Many thanks to my perfect hosts David Basin and Barbara Geiser. The ﬁrst author would also like to thank Krzysztof R. Apt, with whom he wrote his ﬁrst book, for setting a lucid example of how a book should look and for many pieces of invaluable advice during the past years. We are very grateful to Michael Möller for creating a draft on which the cover design of this book is based. Last but not least we wish to thank David Tranah and his team from Cambridge University Press who have been very supportive throughout this book project. List of symbols [ν] (region) [ϕ] (region) −→ (followedby) −→0 (followedbyinitially) 159 159 98 99 θ −−−−→ (leadsto) α −→ (discrete transition) t −→ (delay transition) 99 140, 142 139, 142 ≤θ −−−−→ (upto) ≤θ DN F (P ) Des1 (requirement) Des2 (requirement) E (empty) FA (ﬁnite alternation) GVar (set of global variables) Intv (set of closed intervals) Lab (set of labels) N (natural numbers) O (open) Obs (set of observables) Pred (π, t) Pref (preﬁx operator) Q (rational numbers) R (real numbers) R(X, V ) (reset operations) Req (requirement) Time (time domain) Track Val (set of valuations) X (set of clocks) Z (integer) a! (output action) a? (input action) appr bounds(π) chan (underlying channel) chan b • A (restriction) cross delay[ν] (delay operation) empty ﬁrst(π) free (set of free global variables) g (gate) kern(L) (kernel) , ν −−−−→ 0 (uptoinitially) (provability) ; (chop) ◦ (relational composition) ∼ = (region equivalence) def = (equality by deﬁnition) def ⇐⇒ (equivalence by deﬁnition) 2 (everywhere) 3F (somewhere) P (almost everywhere) t P (variant with duration) ≤t (variant with bound) P I[[P ]] = (models) =0 (models from 0) =1 (isomorphism) A (approaching) Act (set of actions) B?! (action set) Chan (set of channels) Cl (closed) Cr (cross) 100 101 54 39 140 157 37 9 44 43 43 43 43 43 34 45 46 241 147 9 136 136 136 9 9 xv 86 15 15 9 65 31 36 136 294 9 31 218 114 294 294 167 14 4 9 32 136 294 136 136 9 215 136 146 9 163 9 220 40 9 88 140 xvi List of symbols (control vector) 148, , ν , t (timestamped conﬁg.) max (maximum) min (minimum) obs (observable) r1 , . . . , rn (reset operations) r (reset operations) Φ(V ) (integer constraint) Φ(X) (clock constraint) Φ(X, V ) (guards) Ψ(V ) (integer expression) α (complementary action) λ (label) ν (clock valuation) ν + t (time shift) ν[Y := t] (modiﬁcation) τ (internal action) θ (DC term) ξ (computation path) C(A1 , . . . , An ) (network) D (data type) I (interpretation) N (network to timed automata) P (power set) R (structure of real numbers) R(A) (region automaton) X (formula variable) 173 142 298 298 4 167 167 166 136 167 166 136 136 138 139 139 136 36 142 173 4 32 148 295 61 160 72 1 Introduction 1.1 What is a realtime system? This book is about the design of certain kinds of reactive systems. A reactive system interacts with its environment by reacting to inputs from the environment with certain outputs. Usually, a reactive system is not supposed to stop but should be continuously ready for such interactions. In the real world there are plenty of reactive systems around. A vending machine for drinks should be continuously ready for interacting with its customers. When a customer inputs suitable coins and selects “coﬀee” the vending machine should output a cup of hot coﬀee. A traﬃc light should continuously be ready to react when a pedestrian pushes the button indicating the wish to cross the street. A cash machine of a bank should continuously be ready to react to customers’ desire for extracting money from their bank account. Reactive systems are seen in contrast to transformational systems, which are supposed to compute a single input–output transformation that satisﬁes a certain relation and then terminate. For example, such a system could input two matrices and compute its product. We wish to design reactive systems that interact in a welldeﬁned relation to the real, physical time. A realtime system is a reactive system which, for certain inputs, has to compute the corresponding outputs within given time bounds. An example of a realtime system is an airbag. When a car is forced into an emergency braking its airbag has to unfold within 300 milliseconds to protect the passenger’s head. Thus there is a tight upper time bound for the reaction. However, there is also a lower time bound of 100 milliseconds. If the airbag unfolds too early, it will deﬂate and thus lose its protective impact before the passenger’s head sinks into it. This shows that both lower and upper time bounds are important. The outputs of a realtime system may depend on the behaviour of its inputs over time. For instance, a watchdog 1 2 Introduction has to raise an alarm (output) if an input signal is absent for a period of t seconds. Realtime constraints often arise indirectly out of safety requirements. For example, a gas burner should avoid a critical concentration of unburned gas in the air because this could lead to an explosion. This is an untimed safety requirement. To achieve it, a controller for a gas burner could react to a ﬂame failure by shutting down the gas valve for a suﬃciently large period of time so that the gas can evaporate during that period. This way the safety requirement is reduced to a realtime constraint. The gas burner is an example of a safety critical system: a malfunction of such a system can cause loss of goods, money, or even life. Other examples are the airbag in a car, traﬃc controllers, auto pilots, and patient monitors. Realtime constraints are sometimes classiﬁed into hard and soft. Hard constraints must be fulﬁlled without exception, whereas soft ones should not be violated. For example, a car control system should meet the realtime requirements for the air condition, but must meet the realtime constraints for the airbag. In constructing a realtime system the aim is to control a physically existing environment, the plant, in such a way that the controlled plant satisﬁes all desired timing requirements: see Figure 1.1. sensors plant controller actuators Fig. 1.1. Realtime system The controller is a digital computer that interacts with the plant through sensors and actuators. By reading the sensor values the controller inputs information about the current state of the plant. Based on this input the controller can manipulate the state of the plant via the actuators. A precise model of controller, sensors, and actuators has to take reaction times of these components into account because they cannot work arbitrarily fast. In many cases the plant is distributed over diﬀerent physical locations. Also the controller might be implemented on more than one machine. Then one talks of distributed systems. For instance, a railway station consists of many points and signals in the ﬁeld together with several track sensors and actuators. Often the controller is hidden to human beings. Such realtime 1.1 What is a realtime system? 3 systems are called embedded systems. Examples of embedded systems range from controllers in washing machines to airbags in cars. When we model the plant in Figure 1.1 in more detail we arrive at hybrid systems. These are deﬁned as reactive systems consisting of continuous and discrete components. The continuous components are timedependent physical variables of the plant ranging over a continuous value set, like temperature, pressure, position, or speed. The discrete component is the digital controller that should inﬂuence the physical variables in a desired way. For example, a heating system should keep the room temperature within certain bounds. Realtime systems are systems with at least one continuous variable, that is time. Often realtime systems are obtained as abstractions from the more detailed hybrid systems. For example, the exact position of a train relative to a railroad crossing may be abstracted into the values far away, near by, and crossing. Figure 1.2 summarises the main classes of systems discussed above and shows their containment relations: hybrid systems are a special class of realtime systems, which in turn are a special class of reactive systems. reactive systems interact with their environment realtime systems have to compute outputs within certain time intervals hybrid systems work with both discrete and continuous components Fig. 1.2. Classes of systems Since realtime systems often appear in safetycritical applications, their design requires a high degree of precision. Here, formal methods based on mathematical models of the system under design are helpful. They allow the designer to specify the system at diﬀerent levels of abstraction and to formally verify the consistency of these speciﬁcations before implementing 4 Introduction them. In recent years signiﬁcant advances have been made in the maturity of formal methods that can be applied to realtime systems. When considering formal methods for specifying and verifying systems we have the reverse set of inclusions of Figure 1.2, as shown in Figure 1.3: formal methods for hybrid systems can also be used to analyse realtime systems, and formal methods for realtime systems can also be used to analyse reactive systems. methods for hybrid systems methods for realtime systems methods for reactive systems Fig. 1.3. Formal methods for systems classes 1.2 System properties To describe realtime systems formally, we start by representing them by a collection of timedependent state variables or observables obs, which are functions obs : Time −→ D where Time denotes the time domain and D is the data type of obs. Such observables describe an inﬁnite system behaviour, where the current data values are recorded at each moment of time. For example, a gas valve might be described using a Boolean, i.e. {0,1}valued observable G : Time −→ {0, 1} indicating whether gas is present or not, a railway track by an observable Track : Time −→ {empty, appr, cross} where appr means a train is approaching and cross means that it is crossing the gate, and the current communication trace of a reactive system by an observable trace : Time −→ Comm∗ 1.2 System properties 5 where Comm∗ denotes the set of all ﬁnite sequences over a set Comm of possible communications. Thus depending on the choice of observables we can describe a realtime system at various levels of detail. There are two main choices for time domain Time: • discrete time: Time = N, the set of natural numbers, and • continuous time: Time = R≥0 , the set of nonnegative real numbers. A discretetime model is appropriate for speciﬁcations which are close to the level of implementation, where the time rate is already ﬁxed. For higher levels of speciﬁcations continuous time is well suited since the plant models usually use continuousstate variables. Moreover, continuoustime models avoid a tooearly introduction of hardware considerations. Throughout this book we shall use the continuoustime model and consider discrete time as a special case. To describe desirable properties of a realtime system, we constrain the values of their observables over time, using formulas of a suitable logic. In this introduction we simply take predicate logic involving the usual logical connectives ¬ (negation), ∧ (conjunction), ∨ (disjunction), =⇒ (implication), and ⇐⇒ (equivalence) as well as the quantiﬁers ∀ (for all) and ∃ (there exists). When expressing properties of realtime systems quantiﬁcation will typically range over time points, i.e. elements of the time domain Time. Later in this book we introduce dedicated notations for specifying realtime systems. In the following we discuss some typical types of properties. For reactive systems properties are often classiﬁed into safety and liveness properties. For realtime systems these concepts can be reﬁned. Safety properties. Following L. Lamport, a safety property states that something bad must never happen. The “bad thing” represents a critical system state that should never occur, for instance a train being inside a crossing with the gates open. Taking a Boolean observable C : Time −→ {0, 1}, where C(t) = 1 expresses that at time t the system is in the critical state, this safety property can be expressed by the formula ∀t ∈ Time • ¬C(t). (1.1) Here C(t) abbreviates C(t) = 1 and thus ¬C(t) denotes that at time t the system is not in the critical state. Thus for all time points it is not the case that the system is in the critical state. In general, a safety property is characterised as a property that 6 Introduction can be falsiﬁed in bounded time. In case of (1.1) exhibiting a single time point t0 with C(t0 ) suﬃces to show that (1.1) does not hold. In the example, a crossing with permanently closed gates is safe, but it is unacceptable for the waiting cars and pedestrians. Therefore we need other types of properties. Liveness properties. Safety properties state what may or may not occur, but do not require that anything ever does happen. Liveness properties state what must occur. The simplest form of a liveness property guarantees that something good eventually does happen. The “good thing” represents a desirable system state, for instance the gates being open for the road traﬃc. Taking a Boolean observable G : Time −→ {0, 1}, where G(t) = 1 expresses that at time t the system is in the good state, this liveness property can be expressed by the formula ∃t ∈ Time • G(t). (1.2) In other words, there exists a time point in which the system is in the good state. Note that this property cannot be falsiﬁed in bounded time. If for any time point t0 only ¬G(t) has been observed for t ≤ t0 , we cannot complain that (1.2) is violated because eventually does not say how long it will take for the good state to occur. Such liveness property is not strong enough in the context of realtime systems. Here one would like to see a time bound when the good state occurs. This brings us to the next kind of property. Bounded response properties. A bounded response property states that a desired system reaction to an input occurs within a time interval [b, e] with lower bound b ∈ Time and upper bound e ∈ Time where b ≤ e. For example, whenever a pedestrian at a traﬃc light pushes the button to cross the road, the light for pedestrians should turn green within a time interval of, say, [10, 15]. The need for an upper bound is clear: the pedestrian wants to cross the road within a short time (and not eventually). However, also a lower bound is needed because the traﬃc light must not change from green to red instantaneously, but only after a yellow phase of, say, 10 seconds to allow cars to slow down gently. With P (t) representing the pushing of the button at time t and G(t) representing a green traﬃc light for the pedestrians at time t, we can express the desired property by the formula ∀t1 ∈ Time • (P (t1 ) =⇒ ∃t2 ∈ [t1 + 10, t1 + 15] • G(t2 )). (1.3) 1.3 Generalised railroad crossing 7 Note that this property can be falsiﬁed in bounded time. When for some time point t1 with P (t1 ) we ﬁnd out that during the time interval [t1 + 10, t1 + 15] no green light for the pedestrians appeared, property (1.3) is violated. Duration properties. A duration property is more subtle. It requires that for observation intervals [b, e] satisfying a certain condition A(b, e) the accumulated time in which the system is in a certain critical state has an upper bound u(b, e). For example, the leak state of a gas burner, where gas escapes without a ﬂame burning, should occur at most 5% of the time of a whole day. To measure the accumulated time t of a critical state C(t) in a given interval [b, e] we use the integral notion of mathematical calculus: e C(t)dt. b Then the duration property can be expressed by a formula e C(t)dt ≤ u(b, e) . ∀b, e ∈ Time • A(b, e) =⇒ (1.4) b Again this property can be falsiﬁed in ﬁnite time. If we can point out an interval [b, e] satisfying the condition A(b, e) where the value of the integral is too high, property (1.4) is violated. 1.3 Generalised railroad crossing This case study is due to C. Heitmeyer and N. Lynch [HL94]. It concerns a railroad crossing with a physical layout as shown in Figure 1.4, for the case of two tracks. In the safetycritical area “Cross” the road and the tracks intersect. The gates (indicated by “Gate”) can move from fully “closed” (where the angle is 0◦ ) to fully “open” (where the angle is 90◦ ). Moving the gates up and down takes time. Sensors at the tracks will detect whether a train is approaching the crossing, i.e. entering the area marked by “Approach”. 1.3.1 The problem Given are two time parameters ξ1 , ξ2 > 0 describing the reaction times needed to open and close the gates, respectively. In the following problem description time intervals are used that collect all time points in which at least one train is in the area “Cross”. These are called occupancy intervals and denoted by [τi , νi ] where the subscripts i ∈ N enumerate their successive 8 Introduction Gate Approach Cross Approach Gate Fig. 1.4. Generalised railroad crossing occurrences. As usual, a closed interval [τi , νi ] is the set of all time points t with τi ≤ t ≤ νi . Moreover, for a time point t let g(t) denote the angle of the gates, ranging from 0 (closed) to 90 (open). The task is to construct a controller that operates the gates of the railroad crossing such that the following two properties hold for all time points t: • Safety: t ∈ i∈N [τi , νi ] =⇒ g(t) = 0, i.e. the gates are closed inside all occupancy intervals. • Utility: t ∈ / i∈N [τi −ξ1 , νi +ξ2 ] =⇒ g(t) = 90, i.e. outside the occupancy intervals extended by the reaction times ξ1 and ξ2 the gates are open. This problem statement is taken from the article of Heitmeyer and Lynch [HL94]. Note that the safety and utility properties are consistent, i.e. the gate is never required to be simultaneously open and closed. To see this, take a time point t satisfying the precondition (the lefthand side of the implication) of the utility property. Then in particular, t∈ / [τi , νi ], i∈N which implies that t does not satisfy the precondition of the safety property. Thus never both g(t) = 0 and g(t) = 90 are required. Note, however, that depending on the choice of the time parameters ξ1 , ξ2 and the timing of the trains it may well be that in between two successive trains there is not enough time to open the gate, i.e. two successive time intervals [τi − ξ1 , νi + ξ2 ] and may overlap (see also Figure 1.5). [τi+1 − ξ1 , νi+1 + ξ2 ] 1.3 Generalised railroad crossing 9 In the following we formalise and analyse this case study in terms of predicate logic over suitable observables. 1.3.2 Formalisation The railroad crossing can be described by two observables: Track : Time g : Time −→ −→ {empty, appr, cross} [0, 90] (state of the track) (angle of the gate). Note that via the three values of the observable Track we have abstracted from further details of the plant like the exact position of the train on the track. The value empty expresses that no train is in the areas “Approach” or “Cross”, the value appr expresses that a train is in the area “Approach” and none is in “Cross”, and the value cross expresses that a train is in the area “Cross”. The observable g ranges over all values of the gate angle in the interval [0, 90]. We will use the following abbreviations: E(t) stands for Track(t) = empty A(t) stands for Track(t) = appr Cr(t) stands for Track(t) = cross O(t) stands for g(t) = 90 Cl(t) stands for g(t) = 0. Requirements. With these observables and abbreviations we can specify the requirements of the generalised railroad crossing in predicate logic. The safety requirement is easy to specify: Safety ⇐⇒ ∀t ∈ Time • Cr(t) =⇒ Cl(t) def (1.5) where ⇐⇒ means equivalence by deﬁnition. Thus whenever a train is in the crossing the gates are closed. Note that this formula is logically equivalent to the property Safety above because by the deﬁnition of Cr(t) we have ∀t ∈ Time • Cr(t) ⇐⇒ t ∈ [τi , νi ], def i∈N i.e. Cr(t) holds if and only if t is in one of the occupancy intervals. Without the reaction times ξ1 and ξ2 of the gate the utility requirement could simply be speciﬁed as ∀t ∈ Time • ¬Cr(t) =⇒ O(t). 10 Introduction However, the property Utility refers to (the complements of) the intervals [τi − ξ1 , νi + ξ2 ], which are not directly expressible by a certain value of the observable Track. In Figure 1.5 the occupancy intervals [τi , νi ] and their extensions to [τi − ξ1 , νi + ξ2 ] are shown for i = 0, 1, 2. Only outside of the latter intervals, in the areas exhibited by the thick line segments, are the gates required to be open. ξ1 0 τ0 ξ2 ν0 ξ1 τ1 ξ2 ξ1 ν1 τ2 ξ2 ν2 Fig. 1.5. Utility requirement We specify this as follows. Consider a time point t. If in a suitable time interval containing t there is no train in the crossing then O(t) should hold. Calculations show that this interval is given by [t − ξ2 , t + ξ1 ]. Thus ¬Cr(t̃) should hold for all time points t̃ with t − ξ2 ≤ t̃ ≤ t + ξ1 . This is expressed by the following formula: Utility ⇐⇒ ∀t ∈ Time • def (1.6) (∀t̃ ∈ Time • t − ξ2 ≤ t̃ ≤ t + ξ1 =⇒ ¬Cr(t̃)) =⇒ O(t). Note the subtlety that t − ξ2 may be negative whereas t̃ ∈ Time is by deﬁnition nonnegative. It can be shown that this formula Utility is equivalent to the property Utility above (see Exercise 1.2). For the generalised railroad crossing all functions Track and g are admissible that satisfy the two requirements above. These functions can be seen as interpretations of the observables Track and g. They are presented as timing diagrams. Figure 1.6 shows an admissible interpretation of Track and g. Assumptions. In this case study Track is an input observable which can be read but not inﬂuenced by the controller. By contrast, g is an output observable since it can be inﬂuenced by the controller via actuators. The correct behaviour of the controller often depends on some assumptions about the input observables. Here we make the following assumptions about Track: • Initially the track is empty: Init ⇐⇒ E(0). def 1.3 Generalised railroad crossing 11 Track cross appr empty Time g 90 0 ≤ ξ1 ≤ ξ2 ≤ ξ1 Time Fig. 1.6. An admissible interpretation of the observables Track and g • Trains cannot enter the crossing without approaching it: EtoCr ⇐⇒ ∀b, e ∈ Time • (b ≤ e ∧ E(b) ∧ Cr(e)) def =⇒ ∃t ∈ Time • b < t < e ∧ A(t). • Approaching trains eventually cross: AtoE ⇐⇒ ∀b, e ∈ Time • (b ≤ e ∧ A(b) ∧ E(e)) def =⇒ ∃t ∈ Time • b < t < e ∧ Cr(t). Some assumptions about the speed of the approaching trains are also needed. If a train could approach the crossing arbitrarily fast, a typical reaction time of half a minute for the gates to close would not suﬃce. We assume that the fastest train will take a time of ρ to reach the crossing after being detected in the approaching area. Here ρ > 0 is another time parameter. On the other hand, trains which are arbitrarily slow in the approaching area are 12 Introduction not acceptable in the presence of the utility requirement. Therefore we assume that trains need not more than ρ to pass through the approaching area. • Fastest train: TFast ⇐⇒ ∀c, d ∈ Time • (c < d ∧ E(c) ∧ Cr(d)) =⇒ d − c ≥ ρ. def • Slowest train: TSlow ⇐⇒ ∀c ∈ Time • A(c) =⇒ (∃d ∈ Time• c < d < c+ρ ∧¬A(d)). def 1.3.3 Design For the design of the controller we stipulate that the gate is closed at most ξ1 seconds after detection of an approaching train: DesG ⇐⇒ ∀c, d ∈ Time • d − c ≥ ξ1 ∧ def (∀t ∈ Time • c < t < d =⇒ ¬E(t)) =⇒ Cl (d). Under the assumptions Asm ⇐⇒ Init ∧ TFast ∧ ρ ≥ ξ1 def we can then prove that the following implication holds: (Asm ∧ DesG) =⇒ Safety. Thus for all interpretations of Track and g satisfying Asm and DesG, the safety requirement Safety holds. Proof: See Exercise 1.3. 1.4 Gas burner This case study was introduced in [RRH93, HHF+ 94] during the EU project ProCoS (Provably Correct Systems, 1989–95, [BHL+ 96]). The physical components of the plant are shown in Figure 1.7. 1.4.1 The problem The desired functionality of the gas burner is as follows: • If the thermostat signals to switch on the heating the gas valve opens and the burner tries to ignite it for a short period of time. 1.4 Gas burner 13 gas valve  ﬂame sensor thermostat Fig. 1.7. Gas burner • If the thermostat signals to switch oﬀ the heating the gas valve closes. Important is the following safetycritical aspect of the gas burner. If gas eﬀuses without a burning ﬂame in front of the gas valve the concentration of unburned gas can reach critical limits and thus cause an explosion. This has to be avoided. To this end, the following realtime constraint on the system is introduced: • For each time interval with a duration of at least 60 seconds the (accumulated) duration of gas leaks is at most 5% of the overall duration. Note that this requirement does not exclude short gas leaks because they are unavoidable before ignition. If the system satisﬁes this requirement the gas burner is safe. 1.4.2 Formalisation We concentrate on the safety aspect of the gas burner and introduce two Boolean observables: G describes whether the gas valve is open, and F whether the ﬂame is burning as detected by the ﬂame sensor. G : Time −→ {0, 1} F : Time −→ {0, 1}. 14 Introduction The safetycritical state L describes when gas leaks, i.e. when G holds but F def does not. It is formalised by the Boolean expression L ⇐⇒ G ∧ ¬F , which is time dependent just as G and F are: L : Time −→ {0, 1}. Figure 1.8 exhibits an example of interpretations for F and G and the resulting value for L. G F L 1 0 1 0 1 0 Time ≥ 60 Fig. 1.8. Interpretations for F , G, and L The realtime requirement is that for each time interval of at least 60 seconds duration the shaded periods do not exceed 5%, i.e. onetwentieth of that duration. To measure in a given interval [b, e] the sum of the durations of all subintervals in which L(t) = 1 holds, we use the integral notation e L(t)dt. b Here L is considered as a function from real numbers to real numbers, which is integrable under suitable assumptions. The requirement can now be formalised as follows: e e−b def . (1.7) Req ⇐⇒ ∀b, e ∈ Time • e − b ≥ 60 =⇒ L(t)dt ≤ 20 b Looking at this highlevel requirement it is diﬃcult to see how to construct a controller that guarantees it. 1.5 Aims of this book 15 1.4.3 Design As a step towards a controller we make the design decision to introduce two realtime constraints that seem easier to implement and that together imply the requirement Req. (i) The controller can stop each leak within a second : Des1 ⇐⇒ ∀b, e ∈ Time • (∀t ∈ Time • b ≤ t ≤ e =⇒ L(t)) def =⇒ e − b ≤ 1. This constraint restricts the duration of each leak state to at most one second. (ii) After each leak the controller waits for 30 seconds before opening the gas valve again: Des2 ⇐⇒ ∀b, e ∈ Time • (L(b) ∧ L(e) ∧ def ∃t ∈ Time • (b < t < e ∧ ¬L(t))) =⇒ e − b ≥ 30. This constraint requests a distance of at least 30 seconds between any two subsequent leak states. This is illustrated in Figure 1.9. L ¬L L e b ≥ 30 Fig. 1.9. Realtime constraint Des2 From these design constraints it is possible to prove the desired requirement because the following implication holds: (Des1 ∧ Des2) =⇒ Req, i.e. for all interpretations of G and F satisfying Des1 and Des2, the safety requirement Req holds. 1.5 Aims of this book Using predicate logic as a speciﬁcation language for realtime systems has several disadvantages. First, as we have seen in the examples above, we 16 Introduction have to spell out explicitly all quantiﬁcations over time. Second, there is no support for an automatic veriﬁcation of properties that one might want to prove about such speciﬁcations. Third, there is no obvious way to implement a realtime system once it is speciﬁed in predicate logic. To overcome these disadvantages we shall consider three dedicated formal speciﬁcation languages for realtime systems: Duration Calculus, timed automata, and PLCAutomata. 1.5.1 Duration Calculus The Duration Calculus (abbreviated DC) was introduced by Zhou Chaochen in collaboration with M.R. Hansen, C.A.R. Hoare, A.P. Ravn, and H. Rischel. The DC is a temporal logic and calculus for describing and reasoning about properties that timedependent observables satisfy over time intervals. In particular, safety properties, bounded response, and duration properties (hence the name of the calculus) can be expressed in DC. Example 1.1 The safety requirement Req for the gas burner that we formalised in Section 1.4.2 using predicate logic can be expressed in DC more concisely by the duration formula . 2 ≥ 60 =⇒ L ≤ 20 It states that for all observation intervals (2) of length at least 60 seconds ( ≥ 60) the accumulated duration of a gas leak L is at most 5%, i.e. one twentieth of the length of the interval ≤ 20 . Note that in contrast to the formula in predicate logic this DC formula avoids any explicit quantiﬁcation over time points. An advantage of DC is that it enables us to express a highlevel declarative view of realtime systems without implementation bias. We shall therefore use DC as a speciﬁcation language for system requirements. The price to pay is that for the continuoustime domain the satisﬁability problem of the DC is in general undecidable. Thus we cannot hope for automatic veriﬁcation procedures for the full DC. Also direct tool support for the DC is at present rather limited. 1.5 Aims of this book 17 1.5.2 Timed automata Timed automata (abbreviated TA) were introduced by R. Alur and D. Dill as operational models of realtime systems that extend ﬁnitestate automata by explicit, realvalued clock variables. Example 1.2 The timed automaton in Figure 1.10 is due to K.G. Larsen and models a light controller. It has three states called oﬀ, light, bright and four transitions labelled with the input action press? modelling the eﬀects of pressing the light switch. Additionally, this timed automaton uses a clock variable x. The value of this clock can be tested and reset with the transitions. press? press? oﬀ press? light x := 0 x≤3 bright press? x>3 Fig. 1.10. Timed automaton The timed behaviour speciﬁed by this automaton is as follows. Initially, the automaton is in state oﬀ. When the switch is pressed once, the light goes on. If the switch is pressed twice quickly (within 3 seconds) the light gets bright. Otherwise the light will be switched oﬀ with the second pressing. A strong advantage of TA is that they come with automatic veriﬁcation procedures for certain properties like reachability of states. The model checker UPPAAL developed at the universities of Uppsala and Aalborg is the leading tool for carrying out such veriﬁcations. We shall therefore use TA and UPPAAL when we want to verify properties of realtime systems automatically. In particular, a subset of DC can be translated into semantically equivalent TA and thus used as a speciﬁcation language for properties in such an automatic veriﬁcation. 18 Introduction However, since the complexity of automatic veriﬁcation grows exponentially with the number of clocks, the current veriﬁcation technology based on TA quickly reaches its limits when the realtime systems get larger. Another limitation of TA is that they are not always implementable because they allow for nondeterministic backtracking, perfect timing, and timelocks. 1.5.3 PLCAutomata PLCAutomata were introduced by H. Dierks as a special class of realtime automata that model a cyclic behaviour consisting of sensor reading, state transformation, and actuator writing. Example 1.3 Figure 1.11 shows a PLCAutomaton specifying a watchdog. The automaton s∨n s n OK 0s q0 s n Test Alarm 9 s, {n} 0.25 s 0s q1 q2 Fig. 1.11. PLCAutomaton has three states q0 , q1 , q2 and polls with a cycle time of 0.25 seconds the current sensor value. If in its initial state q0 the sensor value s (signal present) is read, the automaton outputs OK. If n (no signal) is read the automaton switches to the state q1 and outputs Test. The inscription in the lower part of this state indicates that here further readings of the sensor value n will be ignored for 9 seconds. However, reactions to the sensor value s are still possible and will cause a switch to the initial state q0 with output OK. If after having been 9 seconds in state q1 still the sensor value n is read, the automaton switches into the state q2 and outputs Alarm. The automaton will then stay in this state. A strong advantage of PLCAutomata is that they can be implemented on a standard hardware platform known as Programmable Logic Controllers (abbreviated PLCs). This explains the name of the automata model. We shall therefore use PLCAutomata as a stepping stone towards an implementation of realtime systems. Once such a system is represented as a network 1.5 Aims of this book 19 of cooperating PLCAutomata it can be compiled automatically into PLC code. Moreover, it is also possible to compile it into code for other hardware platforms as long as they satisfy certain minimal requirements. 1.5.4 Tying it all together Figure 1.12 gives an overview of a design process for realtime systems that forms the backbone of our exposition on formal speciﬁcation and automatic veriﬁcation in this book. abstraction formal description semantic automatic level language integration veriﬁcation Requirements Duration Calculus Constraint Diagrams operational semantics logical semantics DC equiv. ⇑ satisﬁed by timed automata  logical Designs PLCAutomata semantics DC equiv. timed automata UPPAAL operational semantics compiler Programs C code PLC code Moby/RT Fig. 1.12. Overview We consider three levels of abstraction: • requirements will be speciﬁed in Duration Calculus, • designs will be speciﬁed as PLCAutomata, • programs will be written as C code or PLC code. Further on, • automatic veriﬁcation will be performed using timed automata and the model checker UPPAAL. 20 Introduction PLCAutomata are connected to the two other speciﬁcation languages, DC and timed automata, in that they have a logical semantics in terms of DC formulas and an equivalent operational semantics in terms of timed automata. This enables us to automatically verify properties speciﬁed in subsets of DC via translation into timed automata. The veriﬁcation can be performed using any model checker for timed automata. In this book we shall use the tool UPPAAL for this purpose. 1.6 Exercises Exercise 1.1 (System properties) State for each of the following classes of system properties one requirement for an elevator: • • • • safety properties, liveness properties, bounded response properties, duration properties. Exercise 1.2 (Utility) Prove that the formula Utility in (1.6) is equivalent to the original property Utility required for the generalised railroad crossing. Exercise 1.3 (Safety property) Prove that in the generalised railroad crossing case study the following implication holds: (Asm ∧ DesG) =⇒ Safety where Asm, DesG, and Safety are deﬁned as in Section 1.3. Exercise 1.4 (Singletrack line segment) Consider the railroad system in Figure 1.13. The two circular tracks share a safetycritical section: a line segment with a single track only. Suppose that there are exactly two trains driving in opposite directions along this segment. We assume that the trains cannot change their direction. Each entry of the critical section is guarded by a block signal. The points can be assumed to be switched into the right direction when a train is approaching the critical section. 1.7 Bibliographic remarks Approach1 Sig1 21 Leave1 Critical Sig2 Leave2 Approach2 Fig. 1.13. Singletrack line segment (a) How can the positions of the trains and the states of the block signals be described by observables? Give suitable data types for these observables and argue whether a discrete or continuoustime domain is a more suitable choice. (b) Use formulas of predicate logic as in the case study of the generalised railroad crossing to describe the following requirements: – Safety: “There are never two trains at the same time in the critical section.” – Bounded response: “If a train approaches a block signal, it will show a green light within ξwait time.” (c) Formalise the following design speciﬁcations in predicate logic: – A train needs at most ξcross time units to pass the critical section. – A train enters the critical section only if the block signal shows green. – If one of the block signals shows green, the other one shows red. (d) Explain in which case a railroad system that satisﬁes all design speciﬁcations of (c) can nevertheless fail to satisfy the safety requirement. 1.7 Bibliographic remarks Realtime (and hybrid) systems is a very active ﬁeld of research. The current research on realtime systems is presented in journals, at various specialised conferences such as RTSS (IEEE RealTime Systems Symposium), EuroMicro, FTRTFT (Formal Techniques in RealTime and FaultTolerant Systems), FORMATS (Formal Modelling and Analysis of Timed Systems), Hybrid Systems and HSCC (Hybrid Systems: Computation and Control), 22 Introduction and as part of more general conferences. The IEEE Computer Society has a special Technical Committee on RealTime Systems. Only a few books summarising aspects of this large area exist today. The book by H. Kopetz [Kop97] discusses a wide range of concepts needed for the design of distributed embedded realtime systems, including the notion of time, faulttolerance, realtime communications, timetriggered protocols and architectures. It contains a wealth of examples drawn from industrial, in particular automotive applications. The presentation is mostly informal, it does not introduce formal methods to reason about properties of realtime systems. A. Burns and A. Wellings introduce in their book [BW01] many concepts of realtime systems including scheduling, and present in depth important concepts and languages for programming concurrent and realtime systems. They do not discuss formal methods for specifying and verifying realtime systems. The book by J.W.S. Liu [Liu00] is devoted to scheduling algorithms for realtime systems, but also discusses realtime communication protocols and realtime operating systems. A very good overview on diﬀerent methods in scheduling theory, and the speciﬁcation and veriﬁcation of realtime systems, is provided in a book edited by M. Joseph [Jos96]. Another collective work is the book edited by C. Heitmeyer and D. Mandrioli where the generalised railroad crossing (see Section 1.3) case study is used to illustrate and compare various formal speciﬁcation methods for realtime systems [HM96]. A monograph devoted to the Duration Calculus and its extensions is authored by Zhou Chaochen and M.R. Hansen [ZH04]. The book by J.C.M. Baeten and C.A. Middelburg presents a processalgebraic approach to realtime systems [BM02]. A speciﬁc process algebra, i.e. RealTime CSP, is presented in [Dav93]. Reactive systems, speciﬁed by Milner’s Calculus of Communicating Systems (CCS) and timed automata, are presented in the book [AILS07]. In the following we give some pointers to the literature on topics touched upon in this introduction. Subsequent chapters of this book give more detailed bibliographic remarks on the topics discussed there. Case studies. The case study of the Generalised Railroad Crossing was introduced by C. Heitmeyer and N. Lynch [HL94]. Since then it has been used as a benchmark to compare diﬀerent approaches to the speciﬁcation and veriﬁcation of realtime systems (see e.g. [HM96]). The case study of the Gas Burner was introduced in the collaborative European research project ProCoS (Provably Correct Systems) [HHF+ 94, BHL+ 96]. The safety requirement Req (see Subsection 1.4.2) was deﬁned 1.7 Bibliographic remarks 23 in cooperation with engineers of a company producing gas burners. The ﬁrst formal speciﬁcation and correctness proof of the gas burner appeared in [RRH93]. Another prominent case study is the Steam Boiler by J.R. Abrial, E. Börger and H. Langmaack, to which various approaches to the speciﬁcation and veriﬁcation of realtime systems have been applied and compared [ABL96]. Temporal logics. For reasoning about the inﬁnite computations of reactive systems temporal logic has been introduced by A. Pnueli [Pnu77]. In this logic safety and liveness properties of reactive systems [OL82] can be speciﬁed and proven [MP91, MP95]. Whereas safety properties represent requirements that should be continuously maintained by the system, liveness properties represent requirements whose eventual realisation must be guaranteed, for instance that every query is eventually answered or that a process has inﬁnitely often access to a critical resource. Safety properties can be checked by looking at the ﬁnite preﬁxes of a computation, but liveness properties can be checked only by looking at the whole inﬁnite computation, and are thus more diﬃcult to prove. B. Alpern and F.B. Schneider [AS85, AS87] and Z. Manna and A. Pnueli [MP90] presented diﬀerent characterisations of safety and liveness properties, as a partition or as a hierarchy of properties, respectively. Logics for reasoning about properties of realtime systems are mostly extensions of temporal logics for reactive systems. Only if the time domain is discrete can one use the same temporal logic as for reactive systems, for example CTL (Computation Tree Logic) [CES86]. For the continuoustime domain MTL (Metric Temporal Logic) [Koy90] and TCTL (Timed Computational Tree Logic) [ACD93] have been proposed. Lamport advocates an “oldfashioned recipe” for real time which rejects using any special notation but takes a normal temporal logic augmented with explicit clock variables [AL92]. In our opinion this leads to complicated reasoning similar to that in Sections 1.3 and 1.4 based on predicate logic. These are all pointbased temporal logics. By contrast, the Duration Calculus, which is used in this book, is an intervalbased temporal logic for real time extending previous work on Interval Temporal Logic [Mos85]. Logic is often claimed to be an obstacle for direct use by engineers. Therefore formal graphic notations have been proposed for the speciﬁcation of behavioural properties. Well known are MSCs (Message Sequence Charts) developed for applications in telecommunication systems [ITU94, MR94]. In their original form MSCs describe only typical communication traces of a re 24 Introduction active system. To overcome this shortcoming, MSCs have been extended to LSCs (Live Sequence Charts), a graphic notation for a fragment of temporal logic [DH01]. To specify realtime properties graphically, Constraint Diagrams have been proposed [Die96]. Their semantics is deﬁned in terms of the Duration Calculus. We shall introduce Constraint Diagrams in Chapter 3 of this book. Statetransition models. The most popular description technique for reactive systems is statetransition models. Finite automata are well understood since the early days of computing and come with a graphic representation that appeals to engineers. This basic model has been extended in many ways: Büchi automata accept inﬁnite sequences [Tho90], Petri nets have an explicit representation of concurrency [Rei85], statecharts have this as well but also a concept of hierarchy [Har87], action systems add inﬁnite data domains to the ﬁnite control state space [Bac90]. All these statetransition models have been extended to deal with time. In this book we shall deal with two such models for continuous real time. Timed automata were introduced by R. Alur and D. Dill as an extension of Büchi automata by realvalued clocks [AD94]. The most interesting result on timed automata is that certain important properties like the emptiness problem for timed languages and the reachability problem for states are decidable [ACD93, AD94]. This is remarkable because timed automata, although they have only ﬁnitely many control points, describe systems with inﬁnitely many (in fact, uncountably many) states due to their use of clocks ranging over the real numbers. This result has triggered the development of tools for the automatic veriﬁcation of properties of timed automata, in particular UPPAAL [LPW97], KRONOS [Yov97], and HyTech [HHW97]. Although timed automata are an operational model of realtime systems, they cannot always be implemented. This is because a timed automaton is just an acceptor of the desired inﬁnite runs of a realtime system. If after ﬁnitely many steps the timed automaton cannot extend its computation to an inﬁnite run meeting the required timing conditions, these steps are just not accepted. Operationally speaking, the timed automaton has then to backtrack, which is impossible for an implementation representing a controller of a realtime system. PLCAutomata were developed by H. Dierks as a statetransition model of realtime systems that can be implemented on a simple hardware platform, i.e. PLCs (Programmable Logic Controllers) [Die00a]. PLCs are widespread in industrial control and automation applications [Lew95]. PLCAutoma 1.7 Bibliographic remarks 25 ta are not only useful when PLCs serve as an implementation platform. They can be implemented on any hardware platform that performs a nonterminating loop consisting of inputting sensor values, updating the state in accordance with timer values, and outputting actuator values. PLCAutomata are well connected to both the Duration Calculus and timed automata in that they have (equivalent) semantics in each of these other speciﬁcation languages [DFMV98]. This enables us to use PLCAutomata as design speciﬁcations for realtime systems and verify their properties, speciﬁed in subsets of the Duration Calculus, using the modelchecking techniques that are available for timed automata. Process algebras. The essence of process algebras is to use composition operators like parallel composition to structure statetransition models and to study algebraic laws of these operators under certain notions of behavioural equivalence of statetransition models like bisimulation [Mil89]. The most prominent process algebras are CCS (Calculus of Communicating Systems) [Mil89], CSP (Communicating Sequential Processes) [Hoa85, Ros98], and ACP (Algebra of Communicating Systems) [BW90]. All these process algebras have been extended by timing operators, for instance CCS to Timed CCS [Yi91], CSP to Timed CSP [Dav93, DS95, Sch95], ACP to a RealTime Process Algebra [BB91]. A diﬃculty with these algebras is that their semantics is based on certain scheduling assumptions on the actions like urgency, which are diﬃcult to calculate with. We do not pursue the process algebraic approach here, but apply some of their composition operators such as parallel composition and restriction to timed automata. Synchronous languages. The socalled synchronous languages like ESTEREL [BdS91], LUSTRE [CPHP87], and SIGNAL [BlGJ91] are speciﬁcation languages for realtime systems that are based on the discretetime model and the synchrony hypothesis that there is no reaction time between input and output. This idealised model is justiﬁed when the computation time is negligibly small, for example when the system is implemented on a single computer but does not suﬃce for reasoning about distributed systems. By contrast, PLCAutomata, our model reﬂecting the implementation level, are based on the continuoustime model and the assumption that computation and reaction do take time. The latter is essential for their implementability on hardware platforms like distributed networks of PLCs. 26 Introduction Programming languages. To program realtime systems several wellknown programming languages oﬀer (extensions with) realtime constructs like timers and scheduling facilities, in particular Ada, RealTime Java, C/POSIX, and occam2. For details we refer to the book by A. Burns and A. Wellings [BW01]. Additionally, some languages dedicated to particular hardware platforms have been developed, for instance ST (Structured Text) for programming PLCs. ST is a standard in the automation industry; it comprises control structures of an imperative programming language and timers [IEC93]. This language will be discussed brieﬂy in Chapter 5 of this book. Scheduling theory. Scheduling theory can be viewed as a veriﬁcation technique for realtime systems that are speciﬁed as sets of tasks [LL73]. In its simplest setting, only certain time parameters of each task are known, for instance the period (when the task has to be executed), the worstcase execution time (an upper bound of how long the execution may take), and the deadline (an upper time bound before which the execution needs to be completed). A scheduling algorithm will then order the execution of the tasks in an attempt to meet all deadlines, and it will compute the worstcase behaviour. Thus it constructively solves the problem of whether certain bounded response properties are satisﬁed. For more details see for example the books [Jos96, Liu00, BW01]. A task system abstracts from the input and output data and their functional dependency, which is speciﬁed along with the realtime constraints in a highlevel speciﬁcation of a realtime system as shown in this introduction. Task systems appear when a realtime system is to be implemented using a realtime operating system [But02]. The topics of realtime operating systems, scheduling theory, and the analysis of worstcase execution times (WCET) of programs is not part of this book. Our considerations on implementation of realtime systems end at the level of distributed programs with certain assumptions on the upper bounds of their execution cycles. These assumptions have to be discharged separately. Veriﬁcation tools. For the veriﬁcation of properties of speciﬁcations at the requirements or design level we discuss automatic and deductive approaches. Since the pioneering work by Clarke and Emerson [CE81] and by Queille and Sifakis [QS82] model checking, i.e. the automatic veriﬁcation of (mostly temporal) properties of (mostly ﬁnite state) systems, has been developed and applied to an impressive range of cases [CGP00]. As mentioned earlier, Alur, Courcoubetis and Dill have shown that model checking can also be 1.7 Bibliographic remarks 27 applied to verify properties of realtime systems modelled as timed automata [ACD93, AD94]. This is remarkable because timed automata have an inﬁnite state space due to their realvalued clocks. This has led to the development of tools like UPPAAL [LPW97], KRONOS [Yov97], and HyTech [HHW97]. However, the complexity of this automatic veriﬁcation grows exponentially with the number of clocks. Despite the successes in model checking, tackling the huge state spaces that easily arise when considering systems consisting of a parallel composition of many components or of many realtime clocks remains a problem of current research. To apply modelchecking techniques, some preparatory abstraction from the details of the system is therefore necessary. To reason about such abstractions interactive theorem provers can be used. In the area of realtime PVS (Prototype Veriﬁcation System) [ORS92] is often used because it combines the expressive power of higherorder logic with some eﬃcient decision algorithms, in particular for realnumber arithmetic. Mostly, PVS is used to build a direct model of the application problem in higherorder logic and to reason about this model (see e.g. [FW96]). Other approaches proceed by ﬁrst embedding a more speciﬁc realtime logic into PVS and then using the embedded logic for dealing with applications [Ska94]. For the Duration Calculus some tools supporting veriﬁcation have been developed. For the case of discrete time the validity problem of the Duration Calculus is decidable [ZHS93]. P.K. Pandya has exploited this result for the construction of the tool DCVALID [Pan01]. For the case of continuoustime Duration Calculus, J.U. Skakkebæk provided proof support via an embedding of the calculus into the logic of PVS [Ska94]. Similar work was done by S. Heilmann on the basis of the interactive theorem prover Isabelle [Hei99]. The Moby/DC tool provides a semidecision procedure for a subset of (continuoustime) Duration Calculus [DT03], and the Moby/RT tool offers model checking of PLCAutomata against speciﬁcations written in this subset [OD03]. 2 Duration Calculus The Duration Calculus (DC for short) was introduced by Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn. It is an interval temporal logic for continuous time that enables the user to specify desirable properties of a realtime system without bothering about their implementation. A DC formula describes how timedependent state variables or observables of the realtime system should behave in certain time intervals. In particular, this intervalbased view can measure the accumulated duration of states. Depending on the choice of observables both abstract, highlevel and concrete, lowlevel speciﬁcations can be formulated in the Duration Calculus. This chapter is organised as follows. After an informal preview of the Duration Calculus, we introduce its syntax, semantics, and proof rules. Among the proof rules we present an induction rule that is simpler to apply than the classic induction rule of the Duration Calculus. We explain how to use the Duration Calculus as a speciﬁcation language for realtime systems and illustrate this with the gas burner example introduced in the introductory chapter. Properties and subsets of the Duration Calculus will be discussed in the subsequent chapter. 2.1 Preview In Chapter 1 we modelled (examples of) realtime systems by collections of timedependent state variables or observables obs, i.e. functions of the form obs : Time −→ D where Time denotes the time domain, usually the nonnegative real numbers, and D is the data type of obs. Duration Calculus is a logic (and calculus) that is tailored to expressing properties of such observables in a concise way. 28 2.1 Preview 29 As a ﬁrst contact with Duration Calculus, let us look once more at the examples of Chapter 1. Examples 2.1 For the railroad crossing of Section 1.3 let us take E, A, Cr, O, and Cl, introduced as abbreviations in Subsection 1.3.2, as independent Boolean observables E, A, Cr, O, Cl : Time −→ {0, 1} denoting an empty track, an approaching train, a train crossing the gate area, an open gate, and a closed gate, respectively. Often one wishes to specify that a certain property holds throughout an observation interval. To this end, the Duration Calculus oﬀers the everywhere operator written by embracing the property with ceiling brackets . For example, an arbitrary time interval where the track is empty is expressed by the formula E. Similarly, A and Cr denote intervals where a train is approaching and where a train is crossing the gate area, respectively. To specify behaviour patterns consisting of several intervals, the Duration Calculus oﬀers the chop operator ; of interval logic. It “chops” larger intervals into smaller subintervals. For example, a behaviour where ﬁrst the track is empty, then a train is approaching, and ﬁnally it is crossing the gate area is expressed by the formula E ; A ; Cr . To measure the length of an interval the operator is used. For example, A ∧ = 10 expresses an interval of length 10 (seconds) where a train is approaching. To specify that any approaching phase cannot last longer than 15 (seconds), we use implication and write A =⇒ ≤ 15. Informally, this formula states that approaching trains are not driving too slow. To specify that every E–A–Cr behaviour pattern has a duration of at least 10 (seconds) we write (E ; A ; Cr) =⇒ ≥ 10. (2.1) There is one subtlety with this formula. Since the implication should hold for every E–A–Cr pattern, the boundary intervals E and Cr may be 30 Duration Calculus arbitrarily small. Thus in (2.1), actually measures the length of the approaching phase A. Informally, it states that approaching trains are not driving too fast. To specify the safety property that the gate is closed whenever a train is in the crossing, we simply state the implication Cr =⇒ Cl , i.e. for every interval where a train is in the crossing the gate is closed. In contrast to the predicate calculus formula (1.5) in Section 1.3, no explicit quantiﬁcation over time is needed in this Duration Calculus formula. The Utility property requires that the gate must open when there is no train in the crossing for a suﬃciently long time. In Duration Calculus, this can be expressed as follows: (¬Cr ∧ > ξ1 + ξ2 ) =⇒ 3 O . (2.2) This formula states that in every observation interval where there is no train in the crossing and which has a suﬃcient length (here greater than ξ1 + ξ2 , the time needed to open and close the gate), a subinterval can be found where the gate is open. The existence of this subinterval is formalised by the diamond operator 3, which in Duration Calculus is an abbreviation: 3 O ⇐⇒ (true ; O ; true). Thus the subinterval where O holds throughout is surrounded by two arbitrary intervals speciﬁed by true. Note that (2.2) is much shorter than the corresponding predicate calculus formula (1.6) in Section 1.3. For the gas burner of Section 1.4 let us take L as an independent Boolean observable L : Time −→ {0, 1} standing for a gas leak. In Duration Calculus, the safety requirement (1.7) of Section 1.4 that gas must not leak too long can be expressed using the integral operator : ≥ 60 =⇒ L ≤ . 20 This formula states that in each observation interval of length at least 60 (seconds) the duration of L, i.e. the accumulated time where the gas burner leaks, is onetwentieth of that length. In contrast to the predicate calculus formula (1.7), no explicit quantiﬁcation over the integral time bounds is needed in this Duration Calculus formula. The name Duration Calculus 2.2 Syntax and semantics 31 stems from the ability to (conveniently) specify accumulated durations of states with the integral operator. The examples show two characteristics of the Duration Calculus: • Whereas the predicate calculus formulas of Chapter 1 used time points to express properties of observables, the Duration Calculus uses time intervals. This allows for a convenient way of specifying patterns of behaviour sequences. • Unlike the predicate calculus formulas of Chapter 1, the Duration Calculus avoids references to time at the explicit syntactic level and pushes quantiﬁcation over time interval to the implicit semantics level. This results often in very concise speciﬁcations. 2.2 Syntax and semantics We now turn to the formal deﬁnition of the Duration Calculus. In this section we introduce its syntactic constituents together with their meaning or semantics. The calculus consists of state assertions, terms, and formulas, constructed from certain symbols which we introduce ﬁrst. 2.2.1 Symbols We start from the following sets of symbols: • A set of function symbols with typical elements f, g, each one with a certain arity n ∈ N. Function symbols of arity 0 are called constants. We assume the presence of the constants 0, 1 and in fact m for all m ∈ N, and of the binary function symbols + and ·. • A set of predicate symbols with typical elements p, q, each one with a certain arity n ∈ N. We assume the presence of two predicate symbols of arity 0, namely true and false, and of the binary predicate symbols =, <, >, ≤, and ≥. • A set GVar of global variables with typical elements x, y, z, to be used as parameters of a realtime system that do not change over time. • A set Obs of timedependent state variables or observables with typical elements X, Y, Z, each one of a certain (mostly ﬁnite) data type D. Boolean observables are those of data type {0, 1}. • A set of further symbols comprising the logical connectives ¬, ∧, ∨, =⇒, and ⇐⇒ , the quantiﬁers ∀ and ∃, and the symbols , , ; , •, and elements d taken from the data types D of observables. 32 Duration Calculus Semantics. The meaning of the symbols involves the sets {tt, ﬀ} of the truth values “true” and “false”, R of the real numbers, and Time of time, with typical element t. Mostly we consider Time = R≥0 (continuous time) and only in Subsection 3.1.1 alternatively Time = N (discrete time). The semantics of an nary function symbol f is a function, denoted by fˆ, with fˆ : Rn −→ R, and the semantics of an nary predicate symbol p is a function, denoted by p̂, with p̂ : Rn −→ {tt, ﬀ}. In particular, for n = 0 we have fˆ ∈ R and p̂ ∈ {tt, ﬀ}. Examples 2.2 The semantics of the function and predicate symbols mentioned above is ﬁxed throughout this book. The most important cases are as follows: • • • • • • • ˆ = ﬀ, ˆ = tt and false true 0̂ ∈ R is the number zero, 1̂ ∈ R is the number one, +̂ : R2 −→ R is the addition of real numbers, ˆ· : R2 −→ R is the multiplication of real numbers, = ˆ : R2 −→ {tt, ﬀ} is the equality relation on real numbers, ˆ : R2 −→ {tt, ﬀ} is the less than relation on real numbers. < The remaining cases can be deﬁned as abbreviations in the usual way. Since this semantics is the expected one, we shall often simply use the symbols ˆ 0, 1, +, ·, =, < when we mean their semantics 0̂, 1̂, +̂,ˆ·, =, ˆ <. The semantics of a global variable is not ﬁxed, but given by a valuation. This is a mapping V that assigns to each global variable x a real number V(x) ∈ R. We use Val to denote the set of all valuations, i.e. Val = GVar −→ R. The adjective global indicates that the value of a global variable is independent of the time. By contrast, the semantics of a state variable is timedependent. It is given by an interpretation I, which is a mapping that assigns to each state variable X of type D a function I(X) : Time −→ D 2.2 Syntax and semantics 33 such that I(X)(t) denotes the value in D that X has at t ∈ Time. For the interpretation of X we shall also write XI instead of I(X). Such an interpretation can be displayed by a timing diagram. Example 2.3 Consider an observable X of data type {up, down}. The following timing diagram shows (an initial part) of an interpretation I of X, i.e. a function XI : Time −→ {up, down}: XI up down Time 0 1 2 3 4 Thus in the formal account on Duration Calculus we carefully distinguish between syntax and semantics of observables. An observable like X is just a syntactic name which can be interpreted semantically by any function XI from Time to the data type of X, here {up, down}. Later in Subsection 2.2.3 we restrict the set of admissible functions XI somewhat. The meaning of the logical connectives and the quantiﬁers is standard: ¬ denotes negation, ∧ denotes conjunction, ∨ denotes disjunction, =⇒ denotes logical implication, ⇐⇒ denotes logical equivalence, ∀ denotes the universal quantiﬁer for all, and ∃ denotes the existential quantiﬁer there exists. The meaning of the symbols , , ; , •, and d ∈ D will be explained in the following subsections when they are needed. 2.2.2 State assertions State assertions are Boolean combinations of basic properties of state variables. The set of state assertions, with typical elements P, Q, R, is deﬁned by the following abstract syntax: P ::= 0  1  X = d  ¬P  P1 ∧ P2 where d belongs to the data type D of the observable X. For a Boolean observable X (with D = {0, 1}) we abbreviate the basic property X = 1 to X. In the case P1 ∧ P2 the subscripts 1 and 2 serve to distinguish the ﬁrst 34 Duration Calculus and second subassertion. This notation is helpful when structural induction on state assertions is used as in the deﬁnition of semantics below. For conciseness we show here only the logical connectives ¬ and ∧. The other connectives ∨, =⇒, and ⇐⇒ are considered as abbreviations in the usual way. It is well known that the presence of several binary inﬁx operators may lead to syntactic ambiguities when assertions are written as strings. Consider for instance P ∧ Q ⇐⇒ R. Does this mean P ∧ (Q ⇐⇒ R) or (P ∧ Q) ⇐⇒ R ? There are two standard solutions to this problem: either use brackets (as above) or deﬁne priorities for the connectives such that a connective of higher priority binds stronger than one of lower priority. We deﬁne the following priority groups from highest to lowest priority: • negation ¬ , • the binary connectives ∧ and ∨ , • the binary connectives =⇒ and ⇐⇒ . For example, ¬P ∧ Q stands for (¬P ) ∧ Q. Note that brackets may always be used to clarify the intended structure of an assertion. Semantics. Obviously, the semantics of a state assertion depends on the interpretation of the state variables occurring in it and is thus time dependent. Given an interpretation I, assigning to each state variable X a function XI : Time −→ D, the semantics of a state assertion P is a function I[[P ]] : Time −→ {0, 1} such that I(P )(t) denotes the value of P at t ∈ Time. This value is deﬁned inductively on the structure of P : I[[0]](t) = 0, I[[1]](t) = 1, I[[X = d]](t) = 1, if XI (t) = d 0, otherwise, I[[¬P ]](t) = 1 − I[[P ]](t), I[[P1 ∧ P2 ]](t) = 1, if I[[P1 ]](t) = 1 and I[[P2 ]](t) = 1 0, otherwise. 2.2 Syntax and semantics 35 For a Boolean observable X we have the following special case of the third clause of this deﬁnition: I[[X]](t) = I[[X = 1]](t) = XI (t). The function I[[P ]] is also called an interpretation of P and often written as PI instead of I[[P ]]. Using numbers 0 and 1 as values of this interpretation instead of truth values tt and ﬀ is convenient in the next subsection when deﬁning the semantics of terms which are constructed from state assertions. Again, the interpretation PI can be displayed by a timing diagram. Example 2.4 For Boolean observables G and F let L be the state assertion G ∧ ¬F . Recall our convention for Boolean observables: G abbreviates G = 1 and F abbreviates F = 1. Thus L actually stands for G = 1 ∧ ¬ (F = 1). Consider the following interpretations FI : Time −→ {0, 1} and GI : Time −→ {0, 1} and the induced semantics LI : Time −→ {0, 1} of the state assertion L: GI FI LI 1 0 1 0 1 0 Time 0 1 1.2 2 3 4 Fig. 2.1. Interpretations for F , G, and L From the interpretations of Figure 2.1 we see that LI (1.2) = 1 and LI (2) = 0. Formally, this is calculated as follows. At time 1.2 we have LI (1.2) = I[[L]](1.2) = I[[G ∧ ¬F ]](1.2) =1 36 Duration Calculus because I[[G]](1.2) = GI (1.2) = 1 and I[[¬F ]](1.2) = 1 − I[[F ]](1.2) = 1 − FI (1.2) = 1−0 = 1. At time 2 we calculate LI (2) = I[[L]](2) = I[[G ∧ ¬F ]](2) =0 because I[[G]](2) = GI (2) = 0. 2.2.3 Terms Duration terms, abbreviated DC terms or just terms, are expressions that denote real numbers that depend on time intervals. The set of terms, with the typical element θ, is deﬁned by the following abstract syntax: θ ::= x   P  f (θ1 , . . . , θn ) where according to our conventions x is a global variable, P is a state assertion, and f is an nary function symbol. The symbol stands for the length operator and the symbol for the integral operator. A term without the symbols and is called rigid. Note that in this abstract syntax we write function symbols f in preﬁx notation. However, concrete binary function symbols like + and · we shall write in inﬁx notation as usual. For example, we write θ1 + θ2 rather than +(θ1 , θ2 ). As for assertions, this may lead to syntactic ambiguities when terms are written as strings, which have to be removed by using brackets or priorities. Semantics. The semantics of a term depends not only on a given interpretation of the state variables occurring in its state assertions and a given valuation of its global variables, but also on a given time interval. To this end, we introduce the set Intv of all closed intervals in the time domain: Intv = { [b, e]  b, e ∈ Time and b ≤ e} def 2.2 Syntax and semantics 37 def where = means equal by deﬁnition. Intervals of the form [b, b] are called point intervals. The semantics of a term θ is a function I[[θ]] : Val × Intv −→ R such that I[[θ]](V, [b, e]) is the real number that θ denotes under the interpretation I, the valuation V, and the interval [b, e]. This value is deﬁned inductively on the structure of θ: I[[x]](V, [b, e]) = V(x), I[[]](V, [b, e]) = e − b, e PI (t)dt, I[[ P ]](V, [b, e]) = b I[[f (θ1 , . . . , θn )]](V, [b, e]) = fˆ(I[[θ1 ]](V, [b, e]), . . . , I[[θn ]](V, [b, e])). Thus the value of a global variable x depends only on the valuation V, the value of the symbol is the length of the given interval [b, e], the value of the term P is calculated by the integral of the function PI from b to e, and the value of a composed term f (θ1 , . . . , θn ) is determined by applying the function fˆ inductively to the arguments I[[θ1 ]](V, [b, e]), . . . , I[[θn ]](V, [b, e]). e The integral b PI (t)dt measures the accumulated duration that the state assertion P holds (has the value 1) in the time interval [b, e], but we have to ensure that it exists. Since PI : Time −→ {0, 1}, this function correctly maps (in the case of continuous time) real numbers to real numbers, but it might not be (Riemann)integrable. For instance, the socalled Dirichlet function PI (t) = 1, if t ∈ Q 0, if t ∈ /Q yielding 1 for rational t and 0 for irrational t is discontinuous everywhere and thus not integrable. Convention. To exclude such functions, the Duration Calculus considers only interpretations I satisfying the following condition of ﬁnite variability: For each state variable X and each interval [b, e] there is a ﬁnite partition of [b, e] such that the interpretation XI is constant on each part. Thus on each interval [b, e] the function XI has only ﬁnitely many points of discontinuity. This is suﬃcient to guarantee integrability of the functions PI . The following annotated timing diagram illustrates this condition: 38 Duration Calculus PI Time e b Remark 2.5 The semantics I[[θ]](V, [b, e]) of a term θ is insensitive against changes of the interpretation I at individual e time points. This is a simple consequence of the fact that the integral b PI (t)dt is insensitive against such changes. Remark 2.6 The semantics I[[θ]](V, [b, e]) of a rigid term θ does not depend on the interval [b, e]. Thus semantically, rigid terms behave like global variables in that they denote a value that depends only on the valuation V. Example 2.7 Consider θ = x · L. Assume that V(x) = 20 and that LI is given by the following timing diagram: LI 1 0 Time 0 1 2 3 4 Then the semantics I[[θ]](V, [1, 4]) can be calculated as follows: I[[θ]](V, [1, 4]) = I[[x]](V, [1, 4]) ˆ· I[[ L]](V, [1, 4]) 4 LI (t)dt = V(x) ˆ· 1 = 20 ˆ· 2 = 40. 2.2 Syntax and semantics 39 Note that in this calculation we used the ˆ notation for the meaning of the symbol ·, i.e. multiplication of real numbers, but we omitted it for the meaning of the constants 1, 4, 20, 2, and 40. 2.2.4 Formulas Duration formulas, abbreviated DC formulas or just formulas, are the core of the Duration Calculus. They describe properties of observables depending on time intervals. The set of formulas, with typical elements F, G, H, is deﬁned by the following abstract syntax: F ::= p(θ1 , . . . , θn )  ¬F1  F1 ∧ F2  ∀x • F1  F1 ; F2 where p is an nary predicate symbol, θ1 , . . . , θn are terms, the symbol • is used for separation in quantiﬁed formulas, and the symbol ; denotes the socalled chop operator. Formulas of the form p(θ1 , . . . , θn ) are called atomic formulas. Note that true and false are special cases of atomic formulas where the predicate symbol p has arity n = 0. A formula is called rigid if it contains only rigid terms, i.e. if it does not contain symbols or . A formula is called chopfree if it does not contain the ; operator. Note that quantiﬁcation is only possible over (ﬁrstorder) global variables x (representing real numbers), not over (secondorder) state variables (representing functions from real numbers to data values). For conciseness we show here only the logical connectives ¬ and ∧, and the universal quantiﬁer ∀. The connectives ∨, =⇒, and ⇐⇒ , and the existential quantiﬁer ∃ are considered as abbreviations in the usual way. Also we write predicate symbols p here in preﬁx notation. However, concrete binary predicate symbols like = and < we shall write in inﬁx notation as usual. For example, we write θ1 < θ2 rather than < (θ1 , θ2 ). As for state assertions, this may lead to syntactic ambiguities when formulas are written as strings, which have to be removed by using brackets or priorities. We deﬁne the following ﬁve priority groups from highest to lowest priority: • • • • • negation ¬ , the chop operator ; , the binary connectives ∧ and ∨ , the binary connectives =⇒ and ⇐⇒ , the quantiﬁers ∀ and ∃. For example, ¬F ; G ∨ H stands for ((¬F ) ; G) ∨ H, and ∀x • F ∧ G stands for ∀x • (F ∧ G). 40 Duration Calculus As usual, quantiﬁcation leads to the notion of free and bound variables. A global variable x is called a free variable of a formula F if it occurs in F outside all subformulas of the form ∀x • Q or ∃x • Q, and x is called a bound variable of F if it occurs in F inside some subformula of the form ∀x • Q or ∃x • Q. By free(F ) we denote the set of all free global variables in F . For example, x ∈ free( ≤ x ∧ ∀x • x + 0 = 0). In fact, x occurs also bound in this formula. An important syntactic operation on formulas F is the substitution of a term θ for a variable x in F . We write F [x := θ] to denote the formula that results from F by performing the following two steps: (i) F is transformed into F̃ by a renaming of bound variables in F such that no free occurrence of x in F̃ appears within a quantiﬁed subformula of the form ∃z • G or ∀z • G for some z occurring in θ. (ii) F [x := θ] results from F̃ by textually replacing all free occurrences of x in F̃ by θ. The ﬁrst step ensures that there is no clash of a variable z in θ with a bound variable in F . If such a clash cannot occur this step can be omitted. Note that free(F ) = free(F̃ ) and that the formula F [x := θ] is unique up to a renaming of bound variables only. Example 2.8 def def Consider F ⇐⇒ (x ≥ y =⇒ ∃z • z ≥ 0 ∧ x = y + z) and θ1 = . Then F [x := θ1 ] ⇐⇒ ( ≥ y =⇒ ∃z • z ≥ 0 ∧ = y + z). def In this substitution no bound renaming of z is needed. This is diﬀerent if we def consider θ2 = + z. Now z needs to be renamed in F , say into z̃, yielding def F̃ ⇐⇒ (x ≥ y =⇒ ∃z̃ • z̃ ≥ 0 ∧ x = y + z̃), before the replacement of x by θ2 can take place, yielding F [x := θ2 ] ⇐⇒ ( + z ≥ y =⇒ ∃z̃ • z̃ ≥ 0 ∧ + z = y + z̃) def as the result of the substitution. Semantics. The semantics of a formula depends on a given interpretation of the state variables occurring in its terms, a given valuation of the global 2.2 Syntax and semantics 41 variables occurring in its terms, and a given time interval. The semantics of a formula F is a function I[[F ]] : Val × Intv −→ {tt, ﬀ} such that I[[F ]](V, [b, e]) is the truth value of F under the interpretation I, the valuation V, and the interval [b, e]. This value is deﬁned inductively on the structure of F : I[[p(θ1 , . . . , θn )]](V, [b, e]) = p̂(I[[θ1 ]](V, [b, e]), . . . , I[[θn ]](V, [b, e])), I[[¬F1 ]](V, [b, e]) = tt iﬀ I[[F1 ]](V, [b, e]) = ﬀ, I[[F1 ∧ F2 ]](V, [b, e]) = tt iﬀ I[[F1 ]](V, [b, e]) = tt and I[[F2 ]](V, [b, e]) = tt, I[[∀x • F1 ]](V, [b, e]) = tt iﬀ for all d ∈ R the following holds: I[[F1 ]](V[x := d], [b, e]) = tt, I[[F1 ; F2 ]](V, [b, e]) = tt iﬀ there is an m ∈ [b, e] such that I[[F1 ]](V, [b, m]) = tt and I[[F2 ]](V, [m, e]) = tt. The ﬁrst four cases are standard. In case of an atomic formula p(θ1 , . . . , θn ) the truth value is determined by applying the function p̂ to the values I[[θ1 ]](V, [b, e]), . . . , I[[θn ]](V, [b, e]) of the terms θ1 , . . . , θn . In the cases of negation and conjunction the truth values are deﬁned as expected. In case of the universal quantiﬁer we refer to the modiﬁed valuation V[x := d] which agrees with V on all global variables except for x, where the value is modiﬁed to d: V[x := d](y) = V(y), if x = y d, otherwise. The chop operator deserves attention. Intuitively, a formula F1 ; F2 holds on an interval [b, e] if this interval can be “chopped” into an initial subinterval [b, m] and a ﬁnal subinterval [m, e] such that F1 holds on [b, m] and F2 holds on [m, e]. Example 2.9 With the same LI as in Example 2.7 we obtain I[[ L = 0 ; L = 1]](V, [0, 2]) = tt 42 Duration Calculus because I[[ L = 0]](V, [0, 1]) = 1 LI (t)dt = ˆ 0 = tt 2 LI (t)dt = ˆ 1 = tt 0 and I[[ L = 1]](V, [1, 2]) = 1 holds. Remark 2.10 (Rigid and chopfree) Let F be a duration formula, I be an interpretation, V be a valuation, and [b, e] ∈ Intv. • If F is rigid then its semantics I[[F ]](V, [b, e]) does not depend on the interval [b, e], i.e. I[[F ]](V, [b, e]) = I[[F ]](V, [b , e ]) holds for all [b, e], [b , e ] ∈ Intv. • Consider a term θ occurring in F . If F is chopfree or θ is rigid then in the calculation of the semantics I[[F ]](V, [b, e]) of F , every occurrence of θ in F denotes the same value. By contrast, in Example 2.9 above, the formula L = 0; L = 1 is not chopfree, and in the calculation of its semantics I[[ L = 0 ; L = 1]](V, [0, 2]) the two occurrences of the term θ = L denote diﬀerent values, i.e. 1 and 2. The following Substitution Lemma states that the syntactic operation of substitution corresponds on the semantic side to a suitable modiﬁcation of the valuation. Lemma 2.11 (Substitution) Consider a formula F , a global variable x, and a term θ such that F is chopfree or θ is rigid. Then the following holds for all interpretations I, valuations V, and intervals [b, e]: I[[F [x := θ]]](V, [b, e]) = I[[F ]](V[x := d], [b, e]) where d = I[[θ]](V, [b, e]). Proof idea: Use induction on the structure of F and exploit Remark 2.10. Note that without the restrictions on F and θ the lemma does not hold. For instance, consider F ⇐⇒ = x ; = x =⇒ = 2 · x def 2.2 Syntax and semantics 43 and θ = . Then I[[F ]](V, [b, e]) = tt for every interpretation I, every valuation V, and every interval [b, e]. Thus in particular, I[[F ]](V[x := d], [b, e]) = tt for d = I[[θ]](V, [b, e]). However, for b < e I[[F [x := θ]]](V, [b, e]) = I[[ = ; = =⇒ = 2 · ]](V, [b, e]) = ﬀ because = is trivially true whereas = 2 · is false. Abbreviations. The following abbreviations of formulas are often used: • point interval ⇐⇒ = 0. def The formula holds in an interval [b, e] if this is a point interval, i.e. if b = e holds. • almost everywhere P def P ⇐⇒ P = ∧ > 0. The formula P holds in an interval [b, e] if b < e and P is 1 almost everywhere in [b, e] so that the integral P yields e − b, the length of the interval. “Almost” reﬂects the fact that P can be 0 at ﬁnitely many time points in the interval [b, e] without aﬀecting the value of the integral. The following two variants of this notation constrain the length of the interval by a time bound t ∈ Time: • P holds for time t P t ⇐⇒ P ∧ = t. def • P holds up to time t P ≤t ⇐⇒ P ∧ ≤ t. def • For some subinterval F holds 3F ⇐⇒ true ; F ; true. def The 3 operator is a modal operator of interval logic, read as diamond. The formula 3F holds in an interval [b, e] if F holds in some subinterval of [b, e], i.e. if [b, e] can be chopped into an arbitrary initial subinterval, a subinterval where F holds, and an arbitrary ﬁnal subinterval. This is illustrated by the following ﬁgure: 44 Duration Calculus 3F F Time ; b e ; • For all subintervals F holds 2F ⇐⇒ ¬3¬F. def The 2 operator is the dual modal operator of interval logic, read as box. Its deﬁnition by double negation means that there should be no subinterval where F is false. In other words, the formula 2F holds in an interval [b, e] if F holds in every subinterval of [b, e]. This is illustrated by the following diagram: 2F F Time e b Example 2.12 Assume the following interpretation I of the observable L: LI 1 0 Time 0 1 2 3 4 5 6 2.2 Syntax and semantics Let V be an arbitrary valuation. Then the I[[ L = 0 I[[ L = 1 I[[ L = 0; L = 1 I[[ ¬L I[[ L I[[ ¬L ; L I[[ ¬L ; L ; ¬L I[[ 3 L I[[ 3 ¬L I[[ 3 ¬L2 I[[ ¬L2 ; L1 ; ¬L3 45 following statements hold: ]](V, [0, 2]) = 1, ]](V, [2, 6]) = 1, ]](V, [0, 6]) = 1, ]](V, [0, 2]) = 1, ]](V, [2, 3]) = 1, ]](V, [0, 3]) = 1, ]](V, [0, 6]) = 1, ]](V, [0, 6]) = 1, ]](V, [0, 6]) = 1, ]](V, [0, 6]) = 1, ]](V, [0, 6]) = 1. Note how the chop operator is used to describe sequential behaviour. For example, the formula ¬L ; L ; ¬L expresses that a phase where ¬L holds is followed by a phase where L holds, which is followed by a phase where again ¬L holds. 2.2.5 Validity, satisﬁability, and realisability In the following let I be an interpretation, V be a valuation, [b, e] be an interval, and F be a DC formula. Then F holds in I, V, [b, e], in symbols I, V, [b, e] = F, iﬀ I[[F ]](V, [b, e]) = tt. The formula F is satisﬁable iﬀ F holds in some interpretation I, some valuation V, and some interval [b, e]. We say that I and V realise (or are a model of ) F , in symbols I, V = F, iﬀ I, V, [b, e] = F holds for all intervals [b, e]. We call F realisable iﬀ some interpretation I and some valuation V realise F . We say that I realises (or is a model of ) F , in symbols I = F, iﬀ I, V, [b, e] = F holds for all valuations V and all intervals [b, e]. The formula F is valid , in symbols = F, iﬀ all interpretations I and all valuations V realise F . 46 Duration Calculus Remark 2.13 For all DC formulas F the following properties hold: (i) Duality: F is satisﬁable iﬀ ¬F is not valid. F is valid iﬀ ¬F is not satisﬁable. (ii) If F is valid then F is realisable, but not vice versa. (iii) If F is realisable then F is satisﬁable, but not vice versa. Example 2.14 The formulas ≥ 0, = 1, = 30 ⇐⇒ = 10 ; = 20, ((F ; G) ; H) ⇐⇒ (F ; (G ; H)) (associativity of ; ) are all valid. Note that in the third formula the three occurrences of all refer to diﬀerent lengths. For a given interval [b, e] the formula = 30 refers to the length e − b = 30, whereas (due to the chop operator) = 10 and = 20 refer to two adjacent subintervals [b, m] and [m, e] of length m−b = 10 and e − m = 20. The formula L≤x is realisable (and hence satisﬁable) by an appropriate interpretation LI and valuation of x, but it is not valid. The formula =2 is satisﬁable, but not realisable. Initial values of state variables are often important for the correctness of realtime systems. Therefore, we introduce a specialised version of the realisation relation that considers only intervals starting at time 0. We say that I and V realise F from 0 (or are a model of F from 0 ), in symbols I, V =0 F, iﬀ I, V, [0, t] = F holds for all time points t. Intervals of the form [0, t] are called initial intervals. We call F realisable from 0 iﬀ some interpretation I and some valuation V realise F from 0. Again, we simplify the notation if F is independent of the valuation V. Then we say that I realises F from 0 (or is a model of F from 0 ), in symbols I =0 F, 2.3 Speciﬁcation and correctness proof 47 iﬀ I, V, [0, t] = F holds for all valuations V and all time points t. The formula F is valid from 0 , in symbols =0 F, iﬀ all interpretations I and all valuations V realise F from 0. Proposition 2.15 For all interpretations I, valuations V, and DC formulas F the following properties hold: (i) I, V = F implies I, V =0 F , but not vice versa. (ii) If F is realisable then F is realisable from 0, but not vice versa. (iii) F is valid iﬀ F is valid from 0. Proof: Re (i): By deﬁnition, I, V = F implies I, V =0 F . To see that the converse is false, consider F = ∨ X = 1 ; true. Then I =0 F means that XI is 1 initially, but I = F requires that XI is 1 (almost) everywhere. Re (ii): Again by deﬁnition, if F is realisable then F is realisable from 0. To see that the converse is false, we reﬁne the argument above and consider F = ( ∨ X = 1 ; true) ∧ ( ≥ 2 =⇒ 3 X = 0). Then F is realisable from 0, e.g. by the following interpretation XI : XI (t) = 1, if t ≤ 1 0, if t > 1. However, F is not realisable in the general sense because the ﬁrst conjunct of F requires that XI is