LOTOS and PETRI-NET BASED VERIFICATION

of SYSTEMS and CIRCUITS

 

Michael Yoeli

 

Table of Contents

[..] indicates # of book pages (text + figures) presently available

(+..) indicates # of additional book pages in preparation

Preface

 

Chapter 0 - Introduction

 

0.1 Transition-based vs. Level-based Approaches

0.2 Tool Sets Used

0.3 Toward Self-Study

0.4 The Intended Audience

0.5 Further Studies

 

Chapter 1 Processes

 

1.1          Event-based vs. Level-based Approaches

1.2          The Notion of Process

1.3          Examples of Processes

1.4          A Simple Law

1.5          Prefixing

1.6          Terminating Processes

1.7          Process Graphs

1.8          The Choice Operator

1.9          Observation Equivalence

1.10     Some Additional Laws

1.11     Labeled Transition Systems

1.12     Exercises

1.13     Additional Reading

1.14     References

1.15     Solutions of Exercises

 

Chapter 2 Parallel Operators

2.1 Introduction

2.2 The Synchronization Operator || (Blot Version)

2.3 Examples

2.4 Interleaving Operator |||

2.5 Some Laws

2.6 A Sample Proof

2.7 Sequential Composition

2.8 Exercises

2.9 Solutions of Exercises

 

Chapter 3 Basic LOTOS and CADP

 

3.1 About CADP

3.2 Getting Started with CADP

3.3 Equivalences

3.4 Choice

3.5 Comparing Parallel Operators

3.6 Recursion

3.7 More on Parallel Operators

3.8 From LTS to LOTOS

3.9 Hiding

3.10 Additional Exercises

3.11 Solution of Exercises

3.12 Further Reading

3.13 References

 

Chapter 4 Introducing Petri Nets

 

4.1 About Petri Nets

4.2 Petri Graphs and Petri Nets

4.3 Enabling and Firing

4.4 About Languages

4.5 PETRIFY

4.6 Some Solved Exercises

4.7 Further Reading

 

Chapter 5 More on Petri Nets and PETRIFY

 

5.1 Another Definition of Petri Nets

5.2 Labeled Nets

5.3 Bounded Nets

5.4 Observation Equivalence

5.5 From Blot to Petri Nets

5.6 Liveness and Persistence

5.7 Marked Graphs

5.8 Additional Exercises

5.9 Solution of Exercises

5.10 Further Reading

5.11 References

 

Chapter 6 A Simple Net Algebra

 

6.1 The Prefix Operator

6.2 The Choice Operator

6.3 The Star Operator

6.4 Example Exa6.1

6.5 Parallel Compositions

6.6 Towards Solutions

6.7 Further Reading

6.8 References

 

Chapter 7 - Growing Trees from Behaviour Expressions

 

7.1 Process Trees

7.2 Tree Equivalences

7.3 Operational Semantics

7.3.1 Prefix

7.3.2 Choice

7.3.3 Sequential Composition

7.3.4 Recursion

7.3.5 Parallel Composition

7.4 Deadlock

7.5 Laws

7.6 Exercises

7.7 Further Reading

7.8 References

7.9 Some Solutions

 

Chapter 8 Arbiters

 

8.1 Introduction

8.2 A Random Arbiter

8.3 A Blot Representstion

8.4 The Petri Net Approach

10.7 Further Reading

10.8 References

 

Chapter 9 Modular Asynchronous Circuits

 

9.1 About Asynchronous Circuits

9.2 Modular Asynchronous Circuits

9.3 Dynamic vs. Level-based Behaviour

9.4 An Illustrative Example

9.5 Other Modules

9.6 Modular Networks

9.7 Further Reading

9.8 References

 

Chapter 10 Concepts of Realization

 

10.1 Introduction

10.2 Type-A Realizations

10.3 Type-B Realizations

10.4 Type-C Realizations

10.5 The Petri-Net Approach Type-D Realizations

10.6 Further Reading

10.7 References

 

Chapter 11 Module Extensions

 

11.1 XORk (k>2) Modules

11.1.1 Implementation of XORk Module

11.1.2 Using Petri Nets and PETRIFY

11.1.3 XOR4 Implementation and Verification

(Petri-Net Approach)

11.1.4 XOR4 The LOTOS Approach

11.2 CELk (k>2) Modules

11.2.1 Formal Verification (Petri-Net Approach)

11.2.2 Formal Verification (LOTOS Approach}

11.3 Some Solutions

 

Chapter 12 Pipeline Controllers

 

12.1 Introduction

12.2 Transition Signaling

12.3 The Bundled Data Interface

12.4 LCU LOTOS based Specification

12.5 LCU LOTOS based Implementation

12.6 Phase Converters

12.6.1 2-Phase to 4-Phase Converter (PC24)

12.6.2 PC24 Implementation

12.6.3 4-Phase to 2-Phase Converter (PC42)

12.7 Further Reading

12.8 References

Chapter 13 Transition Counters

 

13.1 Counters without Outputs

13.2 Direct Verification

13.3 A Net Representation

13.4 Up-Down Counters with Outputs

13.5 Up-Down Counter k=4

13.6 Modulo-N Transition Counters

13.6.1 Specification

13.6.2 Decompositions

13.6.3 Modulo-3 Counter

13.7 Towards Solutions

13.8 References

 

Chapter 14 Some Communication Protocols

 

14.1 The SCP Protocol

14.2 A Petri Net Description

14.3 The Alternating-Bit (AB) Protocol

14.3.1 Introduction

14.3.2 The Reliable-Channel Case

14.3.3 A LOTOS Description of the Reliable-Channel Case

14.3.4 The Unreliable-Channel Case

14.4 References

14.5 About Solutions

 

Chapter 15 Verification of Design Approaches

 

15.1 Synthesis Approach #1

15.1.1 Realization

15.1.2 The CXC-circuit Example

15.1.3 Direct Verification

15.1.4 LOTOS-based Verification

15.1.5 A Research-oriented Problem

15.2 Synthesis Approach #2

15.2.1 Marked Graph Specification

15.2.2 Illustrating the Synthesis Procedure

15.3 Adding XOR (MERGE) Modules

15.4 Selected Solutions

 

Chapter 16 Producer-Consumer Systems

 

16.1 Petri-Net Approach

16.2 Occurrence Counts

16.3 Verification of the Producer-Consumer System of Section 16.1

16.4 A LOTOS-based Approach

16.5 Further Reading

 

Chapter 17 True Concurrency

 

17.1 The Pi-Language

17.2 Pi-Equivalence

17.3 Concurrency-preserving Synthesis

17.4 An Exercise

17.5 Further Reading

17.6 Solution of Exercise Ex17.1

17.7 References

 

Chapter 18 A Guide to Symbolic Model Checking

 

18.1 About Model Checking

18.2 Introduction to SMV

18.3 Getting Started with the Verifier SMV

18.4 Some Theoretical Background

18.5 Some Applications of SMV

18.6 More Experience with SMV

18.7 References

 

 

Chapter 19 LP (the Larch-Prover) and Arbiter Trees

 

19.1 Introduction

19.2 Initial Steps

19.3 Our First Interactive Session

19.4 Online Help

19.5 The Second InteractiveSession

19.6 Session #3

19.7 Session #4

19.8 Structural Induction

19.9 Defining the Natural Numbers

19.10 Introducing Arbiter Trees

19.11 The LP Approach

19.12 Further Reading

19.13 References

 

Chapter 20 Toward Real Systems

 

20.1 Full LOTOS

20.2 Telephone Switching Systems

20.3 More LOTOS-based Case Studies

20.4 Coloured Petri Nets

20.5 Traffic Signal Control

20.6 References