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

INDEX

Agent, 95

Alternating Bit (AB) communication protocol, 4, 149–155

AND Gate, 173

Arbiter(s), 4, 159–171

Random Arbiter (RGDA), 159–167

Token-Ring Arbiter, 167

Asynchronous circuits, 4, 117

Delay-insensitive circuits, 118

Modular Asynchronous Circuits 117

Asynchronous pipeline controllers verification, 177–180

Blot, 10, 39, 70

Buffer overflow, 185

Buffer underflow, 185

Bundled Data Interface, 178

CADP, 45–49

CALL module, 122

CCS (Calculus of Communication Systems), 95–115

CEL-Circuit (C-Element), 23–26, 112, 119–120

CELk Module, 123

Circuit specification, 127

Circuit Transition System (CTS), 127

Combinational Logic verification, 173–177

Communicating Sequential Processes (CSP), 19

Communication protocols verification, 4, 105, 147–158

Concurrency-Preserving synthesis, 88

Cover

Observational cover, 14

Strong cover, 14

CTL (Computation Tree Logic), 99–100, 107–109

CWB (Concurrency Workbench), 100–113

Deadlock, 17, 39, 72, 106

Decomposition design approach verification, 191–193

Edge-Based, 118, 130

Equivalence, 13

Counterexamples, 104

Equivalence Theorem, 210–211

Language equivalence, 88

Logical equivalence, 35

Observation equivalence, 14–15, 46, 70, 102

Pi-equivalence, 87

Process equivalence, 13

Strong equivalence, 13–18, 46, 98

Trace equivalent, 14–15, 102

Event-Based, 2, 4, 7, 23, 28, 33, 39, 118, 178

Fairness, 159, 163, 165, 168

Grant Only on Request, 159, 163, 165, 168

HML Formulas, 103–106

Internal event, 8

Inverter, 121

Labeled Transition System (LTS), 15

Language, ...