LOTOS and PETRI-NET BASED VERIFICATION

of SYSTEMS and CIRCUITS

Michael Yoeli

[..] 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.11     Labeled Transition Systems

1.12     Exercises

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.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.11  Solution of Exercises

3.13  References

Chapter 4 – Introducing Petri Nets

4.2      Petri Graphs and Petri Nets

4.3      Enabling and Firing

4.5      PETRIFY

4.6      Some Solved Exercises

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.9      Solution of Exercises

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.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.5    Laws

7.6    Exercises

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.8    References

Chapter 9 – Modular 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.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.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.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

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.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

Chapter 17 – True Concurrency

17.1   The Pi-Language

17.2   Pi-Equivalence

17.3   Concurrency-preserving Synthesis

17.4   An Exercise

17.6   Solution of Exercise Ex17.1

17.7   References

Chapter 18 – A Guide to Symbolic 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.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.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