Reactive Systems : Modelling, Specification and Verification

Formal methods is the term used to describe the specification and verification of software and software systems using mathematical logic. Various methodologies have been developed and incorporated into software tools. An important subclass is distributed systems. There are many books that look at particular methodologies for such systems, e.g. CSP, process algebra. This book offers a more balanced introduction for graduate students that describes the various approaches, their strengths and weaknesses, and when they are best used. Milner's CCS and its operational semantics are introduced, together with notions of behavioural equivalence based on bisimulation techniques and with variants of Hennessy-Milner modal logics. Later in the book, the presented theories are extended to take timing issues into account. The book has arisen from various courses taught in Iceland and Denmark and is designed to give students a broad introduction to the area, with exercises throughout. Cover ......Page 1 Reactive Systems......Page 2 Reactive Systems - Modelling, Specification and Verification......Page 4 ISBN-10: 0521875463 ISBN-13: 9780521875462 ISBN-10: 0511335350 ISBN-13: 9780511335358......Page 5 Contents......Page 6 Figures......Page 9 Tables......Page 10 Preface......Page 11 Aims of this book......Page 18 1.1 What are reactive systems?......Page 19 1.2 Process algebras......Page 22 2.1 Some CCS process constructions......Page 24 2.1.1 The behaviour of processes......Page 31 2.2 CCS, formally......Page 33 2.2.1 The model of labelled transition systems......Page 34 2.2.2 The formal syntax and semantics of CCS......Page 38 2.2.3 Value-passing CCS......Page 45 3.1 Criteria for good behavioural equivalence......Page 48 3.2 Trace equivalence: a first attempt......Page 51 3.3 Strong bisimilarity......Page 53 3.4 Weak bisimilarity......Page 70 3.5 Game characterization of bisimilarity......Page 82 3.5.1 Weak bisimulation games......Page 87 3.6 Further results on equivalence checking......Page 89 4.1 Posets and complete lattices......Page 92 4.2 Tarski's fixed point theorem......Page 95 4.3 Bisimulation as a fixed point......Page 102 5.1 Introduction to Hennessy–Milner logic......Page 106 5.2 Hennessy–Milner theorem......Page 115 Introduction......Page 119 6.1 Examples of recursive properties......Page 124 6.2 Syntax and semantics of HML with recursion......Page 126 6.3 Largest fixed points and invariant properties......Page 130 6.4 A game characterization for HML with recursion......Page 132 6.4.1 Examples of use......Page 134 6.5 Mutually recursive equational systems......Page 137 6.6 Characteristic properties......Page 142 6.7 Mixing largest and least fixed points......Page 151 6.8 Further results on model checking......Page 156 Introduction......Page 159 7.1 Specifying mutual exclusion in HML......Page 164 7.2 Specifying mutual exclusion using CCS itself......Page 166 7.3 Testing mutual exclusion......Page 169 8.1 Real-time reactive systems......Page 176 9.1 Intuition......Page 178 9.2 Timed labelled transition systems......Page 180 9.3 Syntax and SOS rules of timed CCS......Page 182 9.4 Parallel composition......Page 186 9.5 Other timed process algebras and discussion......Page 190 10.1 Motivation......Page 192 10.2 Syntax of timed automata......Page 193 10.3 Semantics of timed automata......Page 197 10.4 Networks of timed automata......Page 202 10.5 More on timed-automata formalisms......Page 207 11.1 Timed and untimed trace equivalence......Page 210 11.2 Timed and untimed bisimilarity......Page 212 11.3 Weak timed bisimilarity......Page 217 11.4 Region graphs......Page 220 11.5 Zones and reachability graphs......Page 231 11.6 Further results on timed equivalences......Page 235 Introduction......Page 237 12.1 Basic logic......Page 238 12.2 Hennessy–Milner logic with time and regions......Page 246 12.3 Timed bisimilarity versus HML with time......Page 249 12.4 Recursion in HML with time......Page 254 12.4.1 Characteristic properties for timed bisimilarity......Page 258 12.4.2 Examples of real-time temporal properties......Page 262 12.5 More on timed logics......Page 263 Introduction......Page 265 13.1 Mutual exclusion using timing......Page 267 13.2 Modelling Fischer's algorithm......Page 268 13.2.1 Proving mutual exclusion using UPPAAL......Page 270 13.2.2 An erroneous version of Fischer's algorithm......Page 273 13.3 Further exercises on timing-based mutual exclusion algorithms......Page 275 A.1 Alternating-bit protocol......Page 278 A.2 Gossiping girls......Page 279 A.3 Implementation of regions......Page 280 References......Page 284 Index......Page 298 Containing case studies and numerous exercises, this title is a broad and accessible introduction to the Hennessy-Milner logic aimed at graduate students and based on taught courses in Iceland and Denmark

accessible Text Describing The Process Algebraic Approach To The Specification And Verification Of Software And Software Systems Using Mathematical Logic.