Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS

Michael Yoeli, PhD, is Professor Emeritus in the Department of Computer Science, Technion, Israel. He is the author or editor of several books on digital networks and formal verification. His research interests include theory and applications of Petri nets, formal verification of hardware design, formal verification and synthesis of modular asynchronous networks, and computer-assisted analysis of parallel systems. He was awarded a Certificate of Acknowledgment by the Israel Section of the IEEE and the Israel Chapter of the IEEE Computer Society. Rakefet Kol, PhD, is a member of the Electrical Engineering Department, Technion, Israel. Her research interests include computer architectures, asynchronous design, formal verification of hardware designs, and software engineering. She is a senior member of the IEEE and a professional member of the ACM.

• 1. Introduction 11.1 Event-Based Approach 21.2 Event-Based Systems 21.3 Types of Verification 21.4 Toolsets Used 31.5 Level-Based Approach 31.6 Overview of the Book 31.7 References 52. Processes 72.1 Introduction 72.2 Examples of Processes and Basic Concepts 72.3 About Prefixing 102.4 Process Graphs 102.5 Choice Operator 112.6 Another Process Example 132.7 Equivalences 132.7.1 Strong Equivalence 132.7.2 Observation Equivalence 142.7.3 Some Additional Laws 152.8 Labeled Transition Systems (LTSs) 152.9 Parallel Operators 162.9.1 Parallel Composition 162.9.2 Synchronization Operator k (Blot Version) 162.9.3 Examples of Parallel Compositions 172.9.4 More Laws 172.9.5 Sample Proof 182.9.6 Interleaving Operator kj 182.10 Sequential Composition 182.11 Further Reading 192.12 Selected Solutions 202.13 References 213. From Digital Hardware to Processes 233.1 The C-Element 233.1.1 The 2-Input CEL-Circuit 233.1.2 The 3-Input CEL-Circuit 253.1.3 The 4-Input CEL-Circuit 263.2 The XOR-Gate 263.2.1 The 2-Input XOR-Gate 263.2.2 The 3-Input XOR-Gate 273.3 TOGGLES 293.4 Modulo-N Transition Counters 303.4.1 Modulo-N Transition Counter Specification 303.4.2 Modulo-N Transition Counter Implementations 303.5 Modular Networks 313.6 Propositional Logic: A Review of Known Concepts 333.6.1 Logical Operators 343.6.2 Proving Logical Equivalences 353.6.3 Tautologies and the EQUIV Operator 363.7 Selected Solutions 363.8 References 374. Introducing LOTOS 394.1 From Blot to Basic LOTOS 394.1.1 Recursion 404.2 Some Semantics 414.3 From LTS to LOTOS 424.4 Comparing Parallel Operators 434.5 Sequential Composition 444.6 Hiding 444.7 Equivalences and Preorders 444.8 About CADP 454.8.1 Getting Started with CADP 454.8.2 Verifying Equivalences and Preorders Using CADP 464.8.3 Generating LTS of Choice Using CADP 474.8.4 Generating LTS of Recursion Using CADP 484.9 Full LOTOS—An Introduction 494.9.1 The Full-LOTOS NOT-Gate Example 494.9.2 The Non-Terminating NOT-Gate 514.9.3 The Max Specifications 524.10 The Regular Mu-Calculus (RMC) 534.10.1 Introducing RMC by Examples 534.11 Further Reading 554.12 Selected Solutions 564.13 References 575. Introducing Petri Nets 595.1 About Petri Nets 595.1.1 Petri Graphs and Petri Nets 595.1.2 Enabling and Firing 605.1.3 Another Definition of Petri Nets 615.2 About Languages 615.3 About PETRIFY 625.4 Illustrating Petri Nets 645.5 Labeled Nets 665.6 Bounded Nets 685.7 Observation Equivalence of LPNs 705.8 From Blot to Petri Nets 705.9 Liveness and Persistence 725.10 Simple Reduction Rules 725.11 Marked Graphs 745.12 A Simple Net Algebra 755.12.1 The Prefix Operator 755.12.2 The Choice Operator 775.12.3 The Star Operator 775.12.4 Parallel Compositions 795.13 Arc-Weighted Nets 805.13.1 Enabling and Firing in Arc-Weighted Nets 805.13.2 Arc-Weighted Versus Non-Labeled Nets 825.14 Readers–Writers System 835.14.1 A Readers–Writers System Net Representation 835.14.2 Verification of a Readers–Writers System 845.15 Inhibitor Nets 855.15.1 Introduction to Inhibitor Nets 855.15.2 The Expressive Power of Inhibitor Nets 855.16 True Concurrency 865.16.1 The Pi-Language 875.16.2 Pi-Equivalence 875.16.3 Concurrency-Preserving Synthesis 885.17 Further Reading 895.18 Selected Solutions 895.19 References 936. Introducing CCS 956.1 About CCS 956.2 Operators ‘Prefix’ and ‘Sum’ 956.2.1 Semantics 966.3 Recursion 976.3.1 Semantics 976.4 Concurrency Operator 976.5 Equivalences 986.6 Restriction 986.7 CTL 996.7.1 Introducing CTL 996.8 The Concurrency Workbench (CWB) 1006.8.1 The ‘sim’ and ‘compile’ Commands 1006.8.2 Checking Equivalences 1026.8.3 Checking Restrictions 1036.8.4 HML Formulas 1036.8.5 Equivalences—Counterexamples 1046.8.6 More Equivalence Checking 1056.8.7 Using the mu-Calculus 1066.8.8 Using CTL 1076.9 CCS and CWB Application Examples 1096.9.1 The CCS XCEL-Circuit Example 1096.9.2 The CCS CEL3-Circuit Example 1126.10 Further Reading 1136.11 Selected Solutions 1146.12 References 1157. Verification of Modular Asynchronous Circuits 1177.1 About Asynchronous Circuits 1177.1.1 Modular Asynchronous Circuits 1177.1.2 Edge-Based (Dynamic) Versus Level-Based Behavior 1187.2 XOR-Gates 1187.2.1 LOTOS Representation of XOR-Gate 1187.2.2 Petri Net Representation of XOR-Gate 1197.2.3 CCS Representation of XOR-Gate 1197.3 CEL-Circuit 1197.3.1 LOTOS Representation of CEL-Circuit 1207.3.2 Petri Net Representation of CEL-Circuit 1207.3.3 CCS Representation of CEL-Circuit 1207.4 Other Modules 1217.4.1 Inverter 1217.4.2 ICEL-Element 1217.4.3 TOGGLE 1227.4.4 CALL 1227.5 Module Extensions 1237.5.1 XORk (k . 2) Modules 1237.5.2 CELk (k . 2) Modules 1237.5.3 TOGk (k . 2) 1247.6 Modular Networks 1247.7 Realizations 1257.7.1 Introduction to Realization 1257.7.2 Type-A Realization 1257.7.3 Type-B Realization 1267.7.4 Type-C Realization 1287.7.5 Type-D Realization 1307.7.6 DI Realization 1317.8 Verification of Extended Modules 1317.8.1 Verification of XORk (k . 2) Modules 1327.8.2 Verification of CELk (k . 2) Modules 1357.8.3 Verification of TOGk (k . 2) Modules 1377.9 Verification of Parallel Control Structures 1377.10 Further Reading 1407.11 Selected Solutions 1407.12 References 1468. Verification of Communication Protocols 1478.1 Introduction 1478.2 Two Simple Communication Protocols 1478.2.1 Simple Communication Protocol SCP 1488.2.2 Simple Communication Protocol SCP1 1488.3 The Alternating Bit (AB) Protocol 1498.3.1 Introduction 1498.3.2 The Reliable Channel Case 1498.3.3 The Unreliable Channel Case 1518.4 Further Reading 1568.5 Selected Solutions 1568.6 References 1579. Verification of Arbiters 1599.1 Introduction 1599.2 A Random Arbiter (RGDA) 1599.2.1 Verifying RGDA Using LOTOS 1609.2.2 Verifying RGDA Using Petri Nets 1639.2.3 Verifying RGDA Using CCS 1659.3 A Token-Ring Arbiter 1679.3.1 A Petri Net Representation of a Token-Ring Arbiter 1679.3.2 Verification of a Token-Ring Arbiter Using Petri Net 1689.4 Further Reading 1689.5 Selected Solutions 1699.6 References 17110. More Verification Case Studies 17310.1 Verification of Combinational Logic 17310.1.1 The AND Gate 17310.1.2 Composite Gates 17510.2 Verification of Asynchronous Pipeline Controllers 17710.2.1 Introduction 17710.2.2 Latch Control Unit 17810.2.3 Phase Converters 18110.3 Verification of Producer–Consumer Systems 18310.3.1 Introduction 18310.3.2 Verifying Producer–Consumer Systems Using Petri Nets 18310.3.3 Occurrence Counts 18410.3.4 Verifying the Producer–Consumer System Using Occurrence Counts 18410.3.5 Verifying Producer–Consumer Systems Using LOTOS 18510.3.6 Verification of Multiple-Producer Multiple-Consumer Systems 18610.4 Verification Based on Design Approaches 18810.4.1 Synthesis Approach #1 18810.4.2 Synthesis Approach #2 18910.4.3 Extending the Synthesis Method by Adding XOR Modules 19010.4.4 A Decomposition Approach 19110.5 Verification of Toggles and Transition Counters 19310.5.1 Verification of k-Toggles 19310.5.2 Verification of Counters without Outputs 19410.5.3 Verification of Up–Down Counters with Output 19610.5.4 Verification of Modulo-N Transition Counters 19610.6 Vending Machines Verification—Revisited 19910.6.1 Verifying Vending Machines VeMa Using CCS 19910.6.2 Verifying Vending Machines VeMa Using LOTOS 20010.7 Pi-Realizations 20110.7.1 More on Modular Networks 20210.7.2 Introducing Circuits 20310.7.3 Concurrent Behavior of Circuits 20410.7.4 Pi-Specifications of Circuits 20510.7.5 Simple Verification Examples 20610.7.6 Applying Net Algebra 20610.7.7 Another Verification Example 20710.7.8 Some Pi Propositions 20910.8 A Comparison of Equivalence Relations 21010.8.1 An Equivalence Theorem 21010.8.2 An Application of the Equivalence Theorem 21110.9 Selected Solutions 21110.10 References 22311. Guide to Further Studies 22511.1 Verification of Telecommunication Systems 22511.1.1 Plain Old Telephone System (POTS) 22511.1.2 Advanced Telephone Systems 22611.1.3 ISDN Telephony 22611.2 Verification Using Colored Petri Nets 22611.3 Verification of Traffic Signal Control Systems 22611.4 References 227Index 229