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 Half-title......Page 3 Title......Page 5 Copyright......Page 6 Contents......Page 7 Figures......Page 10 Tables......Page 11 Preface......Page 12 Aims of this book......Page 19 1.1 What are reactive systems?......Page 20 1.2 Process algebras......Page 23 2.1 Some CCS process constructions......Page 25 2.1.1 The behaviour of processes......Page 32 2.2 CCS, formally......Page 34 2.2.1 The model of labelled transition systems......Page 35 2.2.2 The formal syntax and semantics of CCS......Page 39 2.2.3 Value-passing CCS......Page 46 3.1 Criteria for good behavioural equivalence......Page 49 3.2 Trace equivalence: a first attempt......Page 52 3.3 Strong bisimilarity......Page 54 3.4 Weak bisimilarity......Page 71 3.5 Game characterization of bisimilarity......Page 83 3.5.1 Weak bisimulation games......Page 88 3.6 Further results on equivalence checking......Page 90 4.1 Posets and complete lattices......Page 93 4.2 Tarski’s fixed point theorem......Page 96 4.3 Bisimulation as a fixed point......Page 103 5.1 Introduction to Hennessy–Milner logic......Page 107 5.2 Hennessy–Milner theorem......Page 116 Introduction......Page 120 6.1 Examples of recursive properties......Page 125 6.2 Syntax and semantics of HML with recursion......Page 127 6.3 Largest fixed points and invariant properties......Page 131 6.4 A game characterization for HML with recursion......Page 133 6.4.1 Examples of use......Page 135 6.5 Mutually recursive equational systems......Page 138 6.6 Characteristic properties......Page 143 6.7 Mixing largest and least fixed points......Page 152 6.8 Further results on model checking......Page 157 Introduction......Page 160 7.1 Specifying mutual exclusion in HML......Page 165 7.2 Specifying mutual exclusion using CCS itself......Page 167 7.3 Testing mutual exclusion......Page 170 8.1 Real-time reactive systems......Page 177 9.1 Intuition......Page 179 9.2 Timed labelled transition systems......Page 181 9.3 Syntax and SOS rules of timed CCS......Page 183 9.4 Parallel composition......Page 187 9.5 Other timed process algebras and discussion......Page 191 10.1 Motivation......Page 193 10.2 Syntax of timed automata......Page 194 10.3 Semantics of timed automata......Page 198 10.4 Networks of timed automata......Page 203 10.5 More on timed-automata formalisms......Page 208 11.1 Timed and untimed trace equivalence......Page 211 11.2 Timed and untimed bisimilarity......Page 213 11.3 Weak timed bisimilarity......Page 218 11.4 Region graphs......Page 221 11.5 Zones and reachability graphs......Page 232 11.6 Further results on timed equivalences......Page 236 Introduction......Page 238 12.1 Basic logic......Page 239 12.2 Hennessy–Milner logic with time and regions......Page 247 12.3 Timed bisimilarity versus HML with time......Page 250 12.4 Recursion in HML with time......Page 255 12.4.1 Characteristic properties for timed bisimilarity......Page 259 12.4.2 Examples of real-time temporal properties......Page 263 12.5 More on timed logics......Page 264 Introduction......Page 266 13.1 Mutual exclusion using timing......Page 268 13.2 Modelling Fischer’s algorithm......Page 269 13.2.1 Proving mutual exclusion using UPPAAL......Page 271 13.2.2 An erroneous version of Fischer’s algorithm......Page 274 13.3 Further exercises on timing-based mutual exclusion algorithms......Page 276 A.1 Alternating-bit protocol......Page 279 A.2 Gossiping girls......Page 280 A.3 Implementation of regions......Page 281 References......Page 285 Index......Page 299 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.