Modeling and analysis of communicating systems
Groote, Jan Friso
Modeling and analysis of communicating systems - New Delhi : PHI Learning, 2016. - xvi, 376 p, ;
1.Introduction
1.1.Motivation
1.2.The mCRL2 approach
1.3.An overview of the book
1.4.Audience and suggested method of reading
2.Actions, Behavior, Equivalence, and Abstraction
2.1.Actions
2.2.Labeled transition systems
2.3.Equivalence of behaviors
2.3.1.Trace equivalence
2.3.2.Language and completed trace equivalence
2.3.3.Failures equivalence
2.3.4.Strong bisimulation equivalence
2.3.5.The Van Glabbeek linear time-branching time spectrum
2.4.Behavioral abstraction
2.4.1.The internal action τ
2.4.2.Weak trace equivalence
2.4.3.(Rooted) branching bisimulation
2.4.4.(Rooted) weak bisimulation
2.5.Historical notes
3.Data Types
3.1.Data type definition mechanism
3.2.Standard data types
3.2.1.Booleans
3.2.2.Numbers
3.3.Function data types
3.4.Structured data types
3.5.Lists
3.6.Sets and bags
3.7.Where expressions and priorities
3.8.Historical notes
Contents note continued: 4.Sequential Processes
4.1.Actions
4.2.Multi-actions
4.3.Sequential and alternative composition
4.4.Deadlock
4.5.The conditional operator
4.6.The sum operator
4.7.Recursive processes
4.8.Axioms for the internal action
4.9.Historical notes
5.Parallel Processes
5.1.The parallel operator
5.2.Communication among parallel processes
5.3.The allow operator
5.4.Blocking and renaming
5.5.Hiding internal behavior
5.6.Alphabet axioms
5.7.Historical notes
6.The Modal [µ]-calculus
6.1.Hennessy-Milner logic
6.2.Regular formulas
6.3.Fixed point modalities
6.4.Modal formulas and labeled transition systems
6.5.Modal formulas with data
6.6.Equations
6.7.Historical notes
7.Modeling System Behavior
7.1.Alternating bit protocol
7.2.Sliding window protocol
7.3.A patient support platform
7.4.Historical notes
8.Timed Process Behavior
8.1.Timed actions and time deadlocks
Contents note continued: 8.2.Timed transition systems
8.3.Timed process equivalences
8.3.1.Timed (strong) bisimulation
8.3.2.Timed branching bisimulation
8.3.3.Timed trace and timed weak trace equivalence
8.4.Timed processes
8.5.Modal formulas with time
8.6.Historical notes
9.Basic Manipulation of Processes
9.1.Derivation rules for equations
9.2.Derivation rules for formulas
9.3.The sum operator
9.4.The sum elimination lemma
9.5.Induction for constructor sorts
9.6.Recursive specification principle
9.7.Koomen's fair abstraction rule
9.8.Parallel expansion
9.8.1.Basic parallel expansion
9.8.2.Parallel expansion with data: two one-place buffers
9.8.3.Parallel expansion with time
9.9.Historical notes
10.Linear Process Equations and Linearization
10.1.Linear process equations
10.1.1.General linear process equations
10.1.2.Clustered linear process equations
10.2.Linearization
Contents note continued: 10.2.1.Linearization of sequential processes
10.2.2.Parallelization of linear processes
10.2.3.Linearization of n parallel processes
10.3.Proof rules for linear processes
10.3.1.τ-convergence
10.3.2.The convergent linear recursive specification principle (CL-RSP)
10.3.3.CL-RSP with invariants
10.4.Historical notes
11.Confluence and τ-prioritization
11.1.τ-confluence on labeled transition systems
11.2.τ-prioritization of labeled transition systems
11.3.Confluence and linear processes
11.4.τ-prioritization for linear processes
11.4.1.Using confluence for state space generation
11.5.Historical notes
12.Cones and Foci
12.1.Cones and foci
12.2.Protocol verification using the cones and foci
12.2.1.Two unbounded queues form a queue
12.2.2.Milner's scheduler
12.2.3.The alternating bit protocol
12.3.Historical notes
13.Verification of Distributed Systems
Contents note continued: 13.1.Tree identify protocol
13.1.1.The correctness of the tree identify protocol
13.2.Sliding window protocol
13.2.1.Some rules for modulo calculation
13.2.2.Linearization
13.2.3.Getting rid of modulo arithmetic
13.2.4.Proving the nonmodulo sliding window protocol equal to a first-in-first-out queue
13.2.5.Correctness of the sliding window protocol
13.3.Distributed summing protocol
13.3.1.A description in mCRL2
13.3.2.Linearization and invariants
13.3.3.State mapping, focus points, and final lemma
13.4.Historical notes
14.Verification of Modal Formulas Using Parameterized Boolean Equation Systems
14.1.Boolean equation systems
14.1.1.Boolean equation systems and model checking
14.1.2.Gaussian elimination
14.2.Parameterized Boolean equation systems
14.3.Translation of modal formulas to parameterized Boolean equation systems
14.4.Techniques for solving parameterized Boolean equation systems
Contents note continued: 14.4.1.Transforming a parameterized Boolean equation system to a Boolean equation system
14.4.2.Global solving techniques for parameterized Boolean equation systems
14.4.3.Local solving techniques for parameterized Boolean equation systems
14.5.Historical notes
15.Semantics
15.1.Semantics of data types
15.1.1.Signatures
15.1.2.Well-typed data expressions
15.1.3.Free variables and substitutions
15.1.4.Data specifications
15.1.5.Semantics of data types
15.2.Semantics of processes
15.2.1.Processes, action declarations, and process equations
15.2.2.Semantical multi-actions
15.2.3.Substitution on processes
15.2.4.Operational semantics
15.3.Validity of modal [µ]-calculus formulas
15.4.Semantics of parameterized Boolean equation systems
15.5.Soundness and completeness
15.6.Historical notes
A.Brief Tool Primer
A.1.Using the GUI or the command line interface
A.2.A simple running example
Contents note continued: A.3.Linearization
A.4.Manipulating the linear process
A.5.Manipulating and visualizing state spaces
A.6.Solving modal formulas and manipulating PBESs
B.Equational Definition of Built-In Data Types
B.1.Bool
B.2.Positive numbers
B.3.Natural numbers
B.4.Integers
B.5.Reals
B.6.Lists
B.7.Sets
B.8.Bags
B.9.Function update
B.10.Structured sorts
C.Plain-Text Notation
C.1.Data types
C.1.1.Sorts
C.1.2.Functions for any data type
C.1.3.Boolean expressions
C.1.4.Structured-data expressions
C.1.5.Numerical expressions
C.1.6.Function expressions
C.1.7.List expressions
C.1.8.Sets and bags
C.2.Processes
C.3.Modal logic
C.3.1.Action formulas
C.3.2.Regular expressions
C.3.3.State formulas
C.4.(Parameterized) Boolean equation systems
D.Syntax of the Formalisms
D.1.Comments
D.2.Keywords
D.3.Conventions to denote the context-free syntax
D.4.Identifiers and numbers
Contents note continued: D.5.Sort expressions and sort declarations
D.6.Constructors and mappings
D.7.Equations
D.8.Data expressions
D.9.Communication and renaming sets
D.10.Process expressions
D.11.Actions
D.12.Process and initial state declaration
D.13.Data specification
D.14.mCRL2 specification
D.15.Boolean equation systems
D.16.Parameterized Boolean equation systems
D.17.Action formulas
D.18.Regular formulas
D.19.State formulas
D.20.Action rename specifications
E.Axioms for Processes
F.Answers to Exercises.
9788120351837
621.382011 / GRO.M
Modeling and analysis of communicating systems - New Delhi : PHI Learning, 2016. - xvi, 376 p, ;
1.Introduction
1.1.Motivation
1.2.The mCRL2 approach
1.3.An overview of the book
1.4.Audience and suggested method of reading
2.Actions, Behavior, Equivalence, and Abstraction
2.1.Actions
2.2.Labeled transition systems
2.3.Equivalence of behaviors
2.3.1.Trace equivalence
2.3.2.Language and completed trace equivalence
2.3.3.Failures equivalence
2.3.4.Strong bisimulation equivalence
2.3.5.The Van Glabbeek linear time-branching time spectrum
2.4.Behavioral abstraction
2.4.1.The internal action τ
2.4.2.Weak trace equivalence
2.4.3.(Rooted) branching bisimulation
2.4.4.(Rooted) weak bisimulation
2.5.Historical notes
3.Data Types
3.1.Data type definition mechanism
3.2.Standard data types
3.2.1.Booleans
3.2.2.Numbers
3.3.Function data types
3.4.Structured data types
3.5.Lists
3.6.Sets and bags
3.7.Where expressions and priorities
3.8.Historical notes
Contents note continued: 4.Sequential Processes
4.1.Actions
4.2.Multi-actions
4.3.Sequential and alternative composition
4.4.Deadlock
4.5.The conditional operator
4.6.The sum operator
4.7.Recursive processes
4.8.Axioms for the internal action
4.9.Historical notes
5.Parallel Processes
5.1.The parallel operator
5.2.Communication among parallel processes
5.3.The allow operator
5.4.Blocking and renaming
5.5.Hiding internal behavior
5.6.Alphabet axioms
5.7.Historical notes
6.The Modal [µ]-calculus
6.1.Hennessy-Milner logic
6.2.Regular formulas
6.3.Fixed point modalities
6.4.Modal formulas and labeled transition systems
6.5.Modal formulas with data
6.6.Equations
6.7.Historical notes
7.Modeling System Behavior
7.1.Alternating bit protocol
7.2.Sliding window protocol
7.3.A patient support platform
7.4.Historical notes
8.Timed Process Behavior
8.1.Timed actions and time deadlocks
Contents note continued: 8.2.Timed transition systems
8.3.Timed process equivalences
8.3.1.Timed (strong) bisimulation
8.3.2.Timed branching bisimulation
8.3.3.Timed trace and timed weak trace equivalence
8.4.Timed processes
8.5.Modal formulas with time
8.6.Historical notes
9.Basic Manipulation of Processes
9.1.Derivation rules for equations
9.2.Derivation rules for formulas
9.3.The sum operator
9.4.The sum elimination lemma
9.5.Induction for constructor sorts
9.6.Recursive specification principle
9.7.Koomen's fair abstraction rule
9.8.Parallel expansion
9.8.1.Basic parallel expansion
9.8.2.Parallel expansion with data: two one-place buffers
9.8.3.Parallel expansion with time
9.9.Historical notes
10.Linear Process Equations and Linearization
10.1.Linear process equations
10.1.1.General linear process equations
10.1.2.Clustered linear process equations
10.2.Linearization
Contents note continued: 10.2.1.Linearization of sequential processes
10.2.2.Parallelization of linear processes
10.2.3.Linearization of n parallel processes
10.3.Proof rules for linear processes
10.3.1.τ-convergence
10.3.2.The convergent linear recursive specification principle (CL-RSP)
10.3.3.CL-RSP with invariants
10.4.Historical notes
11.Confluence and τ-prioritization
11.1.τ-confluence on labeled transition systems
11.2.τ-prioritization of labeled transition systems
11.3.Confluence and linear processes
11.4.τ-prioritization for linear processes
11.4.1.Using confluence for state space generation
11.5.Historical notes
12.Cones and Foci
12.1.Cones and foci
12.2.Protocol verification using the cones and foci
12.2.1.Two unbounded queues form a queue
12.2.2.Milner's scheduler
12.2.3.The alternating bit protocol
12.3.Historical notes
13.Verification of Distributed Systems
Contents note continued: 13.1.Tree identify protocol
13.1.1.The correctness of the tree identify protocol
13.2.Sliding window protocol
13.2.1.Some rules for modulo calculation
13.2.2.Linearization
13.2.3.Getting rid of modulo arithmetic
13.2.4.Proving the nonmodulo sliding window protocol equal to a first-in-first-out queue
13.2.5.Correctness of the sliding window protocol
13.3.Distributed summing protocol
13.3.1.A description in mCRL2
13.3.2.Linearization and invariants
13.3.3.State mapping, focus points, and final lemma
13.4.Historical notes
14.Verification of Modal Formulas Using Parameterized Boolean Equation Systems
14.1.Boolean equation systems
14.1.1.Boolean equation systems and model checking
14.1.2.Gaussian elimination
14.2.Parameterized Boolean equation systems
14.3.Translation of modal formulas to parameterized Boolean equation systems
14.4.Techniques for solving parameterized Boolean equation systems
Contents note continued: 14.4.1.Transforming a parameterized Boolean equation system to a Boolean equation system
14.4.2.Global solving techniques for parameterized Boolean equation systems
14.4.3.Local solving techniques for parameterized Boolean equation systems
14.5.Historical notes
15.Semantics
15.1.Semantics of data types
15.1.1.Signatures
15.1.2.Well-typed data expressions
15.1.3.Free variables and substitutions
15.1.4.Data specifications
15.1.5.Semantics of data types
15.2.Semantics of processes
15.2.1.Processes, action declarations, and process equations
15.2.2.Semantical multi-actions
15.2.3.Substitution on processes
15.2.4.Operational semantics
15.3.Validity of modal [µ]-calculus formulas
15.4.Semantics of parameterized Boolean equation systems
15.5.Soundness and completeness
15.6.Historical notes
A.Brief Tool Primer
A.1.Using the GUI or the command line interface
A.2.A simple running example
Contents note continued: A.3.Linearization
A.4.Manipulating the linear process
A.5.Manipulating and visualizing state spaces
A.6.Solving modal formulas and manipulating PBESs
B.Equational Definition of Built-In Data Types
B.1.Bool
B.2.Positive numbers
B.3.Natural numbers
B.4.Integers
B.5.Reals
B.6.Lists
B.7.Sets
B.8.Bags
B.9.Function update
B.10.Structured sorts
C.Plain-Text Notation
C.1.Data types
C.1.1.Sorts
C.1.2.Functions for any data type
C.1.3.Boolean expressions
C.1.4.Structured-data expressions
C.1.5.Numerical expressions
C.1.6.Function expressions
C.1.7.List expressions
C.1.8.Sets and bags
C.2.Processes
C.3.Modal logic
C.3.1.Action formulas
C.3.2.Regular expressions
C.3.3.State formulas
C.4.(Parameterized) Boolean equation systems
D.Syntax of the Formalisms
D.1.Comments
D.2.Keywords
D.3.Conventions to denote the context-free syntax
D.4.Identifiers and numbers
Contents note continued: D.5.Sort expressions and sort declarations
D.6.Constructors and mappings
D.7.Equations
D.8.Data expressions
D.9.Communication and renaming sets
D.10.Process expressions
D.11.Actions
D.12.Process and initial state declaration
D.13.Data specification
D.14.mCRL2 specification
D.15.Boolean equation systems
D.16.Parameterized Boolean equation systems
D.17.Action formulas
D.18.Regular formulas
D.19.State formulas
D.20.Action rename specifications
E.Axioms for Processes
F.Answers to Exercises.
9788120351837
621.382011 / GRO.M
