VERIFICATION OF SYSTEMS AND CIRCUITS USING LOTOS, PETRI NETS, AND CCS -- CONTENTS -- 1. Introduction -- 1.1 Event-Based Approach -- 1.2 Event-Based Systems -- 1.3 Types of Verification -- 1.4 Toolsets Used -- 1.5 Level-Based Approach -- 1.6 Overview of the Book -- 1.7 References -- 2. Processes -- 2.1 Introduction -- 2.2 Examples of Processes and Basic Concepts -- 2.3 About Prefixing -- 2.4 Process Graphs -- 2.5 Choice Operator -- 2.6 Another Process Example -- 2.7 Equivalences -- 2.7.1 Strong Equivalence -- 2.7.2 Observation Equivalence -- 2.7.3 Some Additional Laws -- 2.8 Labeled Transition Systems (LTSs) -- 2.9 Parallel Operators -- 2.9.1 Parallel Composition -- 2.9.2 Synchronization Operator

4.8 About CADP -- 4.8.1 Getting Started with CADP -- 4.8.2 Verifying Equivalences and Preorders Using CADP -- 4.8.2.1 Verifying Equivalences Using CADP -- 4.8.2.2 Verifying Preorders Using CADP -- 4.8.3 Generating LTS of Choice Using CADP -- 4.8.4 Generating LTS of Recursion Using CADP -- 4.9 Full LOTOS-An Introduction -- 4.9.1 The Full-LOTOS NOT-Gate Example -- 4.9.1.1 The Full LOTOS NOT-File -- 4.9.1.2 Applying CADP to Derive LTS for the NOT-Gate -- 4.9.2 The Non-Terminating NOT-Gate -- 4.9.3 The Max Specifications -- 4.9.3.1 Max2 Specification -- 4.9.3.2 Max3 Specification -- 4.10 The Regular Mu-Calculus (RMC) -- 4.10.1 Introducing RMC by Examples -- 4.11 Further Reading -- 4.12 Selected Solutions -- 4.13 References -- 5. Introducing Petri Nets -- 5.1 About Petri Nets -- 5.1.1 Petri Graphs and Petri Nets -- 5.1.2 Enabling and Firing -- 5.1.3 Another Definition of Petri Nets -- 5.2 About Languages -- 5.3 About PETRIFY -- 5.4 Illustrating Petri Nets -- 5.5 Labeled Nets -- 5.6 Bounded Nets -- 5.7 Observation Equivalence of LPNs -- 5.8 From Blot to Petri Nets -- 5.9 Liveness and Persistence -- 5.10 Simple Reduction Rules -- 5.11 Marked Graphs -- 5.12 A Simple Net Algebra -- 5.12.1 The Prefix Operator -- 5.12.2 The Choice Operator -- 5.12.3 The Star Operator -- 5.12.4 Parallel Compositions -- 5.12.4.1 The Basic Approach -- 5.12.4.2 The Multiple-Labeled Case -- 5.13 Arc-Weighted Nets -- 5.13.1 Enabling and Firing in Arc-Weighted Nets -- 5.13.2 Arc-Weighted Versus Non-Labeled Nets -- 5.14 Readers-Writers System -- 5.14.1 A Readers-Writers System Net Representation -- 5.14.2 Verification of a Readers-Writers System -- 5.15 Inhibitor Nets -- 5.15.1 Introduction to Inhibitor Nets -- 5.15.2 The Expressive Power of Inhibitor Nets -- 5.16 True Concurrency -- 5.16.1 The Pi-Language -- 5.16.2 Pi-Equivalence -- 5.16.3 Concurrency-Preserving Synthesis.

5.17 Further Reading -- 5.18 Selected Solutions -- 5.19 References -- 6. Introducing CCS -- 6.1 About CCS -- 6.2 Operators 'Prefix' and 'Sum' -- 6.2.1 Semantics -- 6.3 Recursion -- 6.3.1 Semantics -- 6.4 Concurrency Operator -- 6.5 Equivalences -- 6.6 Restriction -- 6.7 CTL -- 6.7.1 Introducing CTL -- 6.8 The Concurrency Workbench (CWB) -- 6.8.1 The 'sim' and 'compile' Commands -- 6.8.2 Checking Equivalences -- 6.8.3 Checking Restrictions -- 6.8.4 HML Formulas -- 6.8.5 Equivalences-Counterexamples -- 6.8.6 More Equivalence Checking -- 6.8.7 Using the mu-Calculus -- 6.8.8 Using CTL -- 6.9 CCS and CWB Application Examples -- 6.9.1 The CCS XCEL-Circuit Example -- 6.9.1.1 The CCS Approach -- 6.9.1.2 Comparing the CCS Approach with the LOTOS Approach -- 6.9.2 The CCS CEL3-Circuit Example -- 6.10 Further Reading -- 6.11 Selected Solutions -- 6.12 References -- 7. Verification of Modular Asynchronous Circuits -- 7.1 About Asynchronous Circuits -- 7.1.1 Modular Asynchronous Circuits -- 7.1.2 Edge-Based (Dynamic) Versus Level-Based Behavior -- 7.2 XOR-Gates -- 7.2.1 LOTOS Representation of XOR-Gate -- 7.2.2 Petri Net Representation of XOR-Gate -- 7.2.3 CCS Representation of XOR-Gate -- 7.3 CEL-Circuit -- 7.3.1 LOTOS Representation of CEL-Circuit -- 7.3.2 Petri Net Representation of CEL-Circuit -- 7.3.3 CCS Representation of CEL-Circuit -- 7.4 Other Modules -- 7.4.1 Inverter -- 7.4.2 ICEL-Element -- 7.4.3 TOGGLE -- 7.4.4 CALL -- 7.5 Module Extensions -- 7.5.1 XORk (k > 2) Modules -- 7.5.2 CELk (k > 2) Modules -- 7.5.3 TOGk (k > 2) -- 7.6 Modular Networks -- 7.7 Realizations -- 7.7.1 Introduction to Realization -- 7.7.2 Type-A Realization -- 7.7.2.1 Type-A1 Realization -- 7.7.3 Type-B Realization -- 7.7.4 Type-C Realization -- 7.7.5 Type-D Realization -- 7.7.5.1 Extended Type-D Realizations -- 7.7.6 DI Realization -- 7.8 Verification of Extended Modules.

7.8.1 Verification of XORk (k > 2) Modules -- 7.8.1.1 Implementation of XORk -- 7.8.1.2 Verification of XORk Using Petri Nets and PETRIFY -- 7.8.1.3 Verification of XORk Using LOTOS and CADP -- 7.8.1.4 Verification of XORk Using CCS and CWB-NC -- 7.8.2 Verification of CELk (k > 2) Modules -- 7.8.2.1 Implementation of CELk -- 7.8.2.2 Verification of CELk Using Petri Nets and PETRIFY -- 7.8.2.3 Verification of CELk Using LOTOS and CADP -- 7.8.2.4 Verification of CELk Using CCS and CWB-NC -- 7.8.3 Verification of TOGk (k > 2) Modules -- 7.9 Verification of Parallel Control Structures -- 7.10 Further Reading -- 7.11 Selected Solutions -- 7.12 References -- 8. Verification of Communication Protocols -- 8.1 Introduction -- 8.2 Two Simple Communication Protocols -- 8.2.1 Simple Communication Protocol SCP -- 8.2.2 Simple Communication Protocol SCP1 -- 8.3 The Alternating Bit (AB) Protocol -- 8.3.1 Introduction -- 8.3.2 The Reliable Channel Case -- 8.3.2.1 A LOTOS Description of the Reliable Channel Case -- 8.3.3 The Unreliable Channel Case -- 8.3.3.1 A LOTOS Verification of the Unreliable Channel Case -- 8.3.3.2 A CCS Verification of the Unreliable Channel Case -- 8.4 Further Reading -- 8.5 Selected Solutions -- 8.6 References -- 9. Verification of Arbiters -- 9.1 Introduction -- 9.2 A Random Arbiter (RGDA) -- 9.2.1 Verifying RGDA Using LOTOS -- 9.2.1.1 Blot and LOTOS Representation of RGDA -- 9.2.1.2 Verification of RGDA Using LOTOS -- 9.2.1.2.1 Verifying Mutual Exclusion -- 9.2.1.2.2 Verifying Grant Only on Request -- 9.2.1.2.3 Verifying Fairness -- 9.2.2 Verifying RGDA Using Petri Nets -- 9.2.2.1 Petri Net Representation of RGDA -- 9.2.2.2 Verification of RGDA Using Petri Net -- 9.2.2.2.1 Verifying Mutual Exclusion -- 9.2.2.2.2 Verifying Grant Only on Request -- 9.2.2.2.3 Verifying Fairness -- 9.2.3 Verifying RGDA Using CCS -- 9.3 A Token-Ring Arbiter.

9.3.1 A Petri Net Representation of a Token-Ring Arbiter -- 9.3.2 Verification of a Token-Ring Arbiter Using Petri Net -- 9.4 Further Reading -- 9.5 Selected Solutions -- 9.6 References -- 10. More Verification Case Studies -- 10.1 Verification of Combinational Logic -- 10.1.1 The AND Gate -- 10.1.2 Composite Gates -- 10.2 Verification of Asynchronous Pipeline Controllers -- 10.2.1 Introduction -- 10.2.1.1 Transition Signaling -- 10.2.1.2 The Bundled Data Interface -- 10.2.2 Latch Control Unit -- 10.2.2.1 A Blot Specification of LCU -- 10.2.2.2 A LOTOS Specification of LCU -- 10.2.2.3 A LOTOS Implementation of LCU -- 10.2.2.4 Latch Problems -- 10.2.3 Phase Converters -- 10.2.3.1 2-Phase to 4-Phase Converter (PC24) -- 10.2.3.2 4-Phase to 2-Phase Converter (PC42) -- 10.3 Verification of Producer-Consumer Systems -- 10.3.1 Introduction -- 10.3.2 Verifying Producer-Consumer Systems Using Petri Nets -- 10.3.3 Occurrence Counts -- 10.3.4 Verifying the Producer-Consumer System Using Occurrence Counts -- 10.3.4.1 Verifying Liveness -- 10.3.4.2 Verifying Boundedness -- 10.3.4.3 Verifying Overflow/Underflow -- 10.3.5 Verifying Producer-Consumer Systems Using LOTOS -- 10.3.6 Verification of Multiple-Producer Multiple-Consumer Systems -- 10.3.6.1 A 2-Producer-2-Consumer System with Priority -- 10.4 Verification Based on Design Approaches -- 10.4.1 Synthesis Approach #1 -- 10.4.1.1 Realization -- 10.4.1.2 Formal Verification of the CXC-Circuit Example -- 10.4.1.3 Another Synthesis Verification Example -- 10.4.2 Synthesis Approach #2 -- 10.4.3 Extending the Synthesis Method by Adding XOR Modules -- 10.4.4 A Decomposition Approach -- 10.5 Verification of Toggles and Transition Counters -- 10.5.1 Verification of k-Toggles -- 10.5.2 Verification of Counters without Outputs -- 10.5.2.1 Direct Verification of udcount -- 10.5.2.2 Verification of udcount Using Petri Net.

10.5.3 Verification of Up-Down Counters with Output.