Introduction to Process AlgebraSpringer Science & Business Media, 23 déc. 1999 - 168 pages Automated and semi-automated manipulation of so-called labelled transition systems has become an important means in discovering flaws in software and hardware systems. Process algebra has been developed to express such labelled transition systems algebraically, which enhances the ways of manipulation by means of equational logic and term rewriting. The theory of process algebra has developed rapidly over the last twenty years, and verification tools have been developed on the basis of process algebra, often in cooperation with techniques related to model checking. This textbook gives a thorough introduction into the basics of process algebra and its applications. |
Table des matières
1 Introduction | 3 |
2 Basic Process Algebra | 9 |
22 Transition Rules for BPA | 10 |
23 Bisimulation Equivalence | 12 |
24 Axioms for BPA | 14 |
3 Algebra of Communicating Processes | 19 |
32 Left Merge and Communication Merge | 21 |
33 Axioms for PAP | 22 |
62 Bounded Retransmission Protocol | 80 |
63 Specification and Verification Techniques | 90 |
64 Tools | 94 |
7 Extensions | 99 |
72 State Operator | 101 |
73 Priorities | 107 |
A Equational Logic | 111 |
A2 Axiomatisations | 112 |
34 Deadlock and Encapsulation | 27 |
4 Recursion | 33 |
42 Transition Rules for Guarded Recursion | 35 |
43 Recursive Definition and Specification Principles | 38 |
44 Completeness for Regular Processes | 41 |
45 Approximation Induction Principle | 44 |
5 Abstraction | 49 |
52 Guarded Linear Recursion Revisited | 53 |
53 Axioms for the Silent Step | 55 |
54 Abstraction Operators | 59 |
55 An Example with Queues | 62 |
56 Cluster Fair Abstraction Rule | 65 |
6 Protocol Verifications | 71 |
A3 Initial Models | 113 |
A4 Term Rewriting | 115 |
B Structural Operational Semantics | 121 |
B2 The Meaning of Negative Premises | 123 |
B3 Bisimulation as a Congruence | 127 |
B4 Branching Bisimulation as a Congruence | 130 |
B5 Conservative Extension | 133 |
B6 Modal Logics | 135 |
Solutions to Selected Exercises | 139 |
References | 153 |
163 | |
Autres éditions - Tout afficher
Expressions et termes fréquents
alternating bit protocol atomic actions axiomatisation axioms Baeten basic process terms behaviour branching bisimulation equivalence CFAR channel closed terms communication Computer congruence conservative extension data packet datum deadlock Definition derived E₁ equality relation equivalence relation Example execute Exercise ƐACP finite function symbol Glabbeek guarded linear recursion guarded recursive specification Hence induction initial transitions intuition J.A. Bergstra labelled transition system linear recursive specification logic merge model checking modulo AC modulo bisimulation equivalence modulo rooted branching natural numbers negative premises normal form operational semantics ordinal numbers panth format positive after reduction process algebra process graph proof of Theorem protocol RBB cool format recursive equations regular process renaming rewrite rules right-hand side rooted branching bisimulation Sender sends signature silent step source-dependent T-transitions T₁ three-valued stable model transition rules truly silent unary function verification weight Y=bY