Reactive Systems

Höfundar: Luca Aceto; Anna Ingólfsdóttir; Kim Guldstrand Larsen; Jiri Srba (Útgáfa: 1)
Reactive Systems

Kaup valmöguleikar

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.

Nánar um bókina

Útgefandi
Cambridge University Press
ISBN
9780511332142
Print ISBN
9780521875462
Format
Page Fidelity (PDF)
Útgáfa
1
Höfundar
Luca Aceto; Anna Ingólfsdóttir; Kim Guldstrand Larsen; Jiri Srba
Tungumál
English
Útgefið
2007-08-09
Prent takmörkun á líftíma
10
Prent takmörkun
5
Afritunar takmörkun
5

Kaflar

  • Half-title
  • Title
  • Copyright
  • Contents
  • Figures and tables
  • Figures
  • Tables
  • Preface
  • Part I A Classic Theory of Reactive Systems
  • 1 Introduction
  • Aims of this book
  • 1.1 What are reactive systems?
  • 1.2 Process algebras
  • 2 The language CCS
  • 2.1 Some CCS process constructions
  • 2.1.1 The behaviour of processes
  • 2.2 CCS, formally
  • 2.2.1 The model of labelled transition systems
  • 2.2.2 The formal syntax and semantics of CCS
  • 2.2.3 Value-passing CCS
  • 3 Behavioural equivalences
  • 3.1 Criteria for good behavioural equivalence
  • 3.2 Trace equivalence: a first attempt
  • 3.3 Strong bisimilarity
  • 3.4 Weak bisimilarity
  • 3.5 Game characterization of bisimilarity
  • 3.5.1 Weak bisimulation games
  • 3.6 Further results on equivalence checking
  • 4 Theory of fixed points and bisimulation equivalence
  • 4.1 Posets and complete lattices
  • 4.2 Tarski?s fixed point theorem
  • 4.3 Bisimulation as a fixed point
  • 5 Hennessy?Milner logic
  • 5.1 Introduction to Hennessy?Milner logic
  • 5.2 Hennessy?Milner theorem
  • 6 Hennessy?Milner logic with recursive definitions
  • Introduction
  • 6.1 Examples of recursive properties
  • 6.2 Syntax and semantics of HML with recursion
  • 6.3 Largest fixed points and invariant properties
  • 6.4 A game characterization for HML with recursion
  • 6.4.1 Examples of use
  • 6.5 Mutually recursive equational systems
  • 6.6 Characteristic properties
  • 6.7 Mixing largest and least fixed points
  • 6.8 Further results on model checking
  • 7 Modelling and analysis of mutual exclusion algorithms
  • Introduction
  • 7.1 Specifying mutual exclusion in HML
  • 7.2 Specifying mutual exclusion using CCS itself
  • 7.3 Testing mutual exclusion
  • Part II A Theory of Real-time Systems
  • 8 Introduction
  • 8.1 Real-time reactive systems
  • 9 CCS with time delays
  • 9.1 Intuition
  • 9.2 Timed labelled transition systems
  • 9.3 Syntax and SOS rules of timed CCS
  • 9.4 Parallel composition
  • 9.5 Other timed process algebras and discussion
  • 10 Timed automata
  • 10.1 Motivation
  • 10.2 Syntax of timed automata
  • 10.3 Semantics of timed automata
  • 10.4 Networks of timed automata
  • 10.5 More on timed-automata formalisms
  • 11 Timed behavioural equivalences
  • 11.1 Timed and untimed trace equivalence
  • 11.2 Timed and untimed bisimilarity
  • 11.3 Weak timed bisimilarity
  • 11.4 Region graphs
  • 11.5 Zones and reachability graphs
  • 11.6 Further results on timed equivalences
  • 12 Hennessy?Milner logic with time
  • Introduction
  • 12.1 Basic logic
  • 12.2 Hennessy?Milner logic with time and regions
  • 12.3 Timed bisimilarity versus HML with time
  • 12.4 Recursion in HML with time
  • 12.4.1 Characteristic properties for timed bisimilarity
  • 12.4.2 Examples of real-time temporal properties
  • 12.5 More on timed logics
  • 13 Modelling and analysis of Fischer?s algorithm
  • Introduction
  • 13.1 Mutual exclusion using timing
  • 13.2 Modelling Fischer?s algorithm
  • 13.2.1 Proving mutual exclusion using UPPAAL
  • 13.2.2 An erroneous version of Fischer?s algorithm
  • 13.3 Further exercises on timing-based mutual exclusion algorithms
  • Appendix A Suggestions for student projects
  • A.1 Alternating-bit protocol
  • A.2 Gossiping girls
  • A.3 Implementation of regions
  • References
  • Index