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