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 || (Blot Version)

2.9.3 Examples of Parallel Compositions

2.9.4 More Laws

2.9.5 Sample Proof

2.9.6 Interleaving Operator |||

2.10 Sequential Composition

2.11 Further Reading

2.12 Selected Solutions

2.13 References

3. From Digital Hardware to Processes

3.1 The C-Element

3.1.1 The 2-Input CEL-Circuit

3.1.2 The 3-Input CEL-Circuit

3.1.3 The 4-Input CEL-Circuit

3.2 The XOR-Gate

3.2.1 The 2-Input XOR-Gate

3.2.2 The 3-Input XOR-Gate

3.3 TOGGLES

3.4 Modulo-N Transition Counters

3.4.1 Modulo-N Transition Counter Specification

3.4.2 Modulo-N Transition Counter Implementations

3.4.2.1 The Cases N = 3 and N = 4

3.4.2.2 The N > 4 Case

3.5 Modular Networks

3.6 Propositional Logic: A Review of Known Concepts

3.6.1 Logical Operators

3.6.2 Proving Logical Equivalences

3.6.3 Tautologies and the EQUIV Operator

3.7 Selected Solutions

3.8 References

4. Introducing LOTOS

4.1 From Blot to Basic LOTOS

4.1.1 Recursion

4.2 Some Semantics

4.3 From ...