Verification of systems and circuits using LOTOS, Petri Nets, and CCS
A Step-by-Step Guide to Verification of Digital Systems This practical book provides a step-by-step, interactive introduction to formal verification of systems and circuits. The book offers theoretical background and introduces the application of three powerful verification toolsets: LOTOS-based CAD...
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | Libro electrónico |
| Idioma: | Inglés |
| Publicado: |
Hoboken, N.J. :
Wiley-Interscience
c2008.
|
| Edición: | 1st edition |
| Colección: | Wiley series on parallel and distributed computing.
|
| Materias: | |
| Ver en Biblioteca Universitat Ramon Llull: | https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009627630406719 |
Tabla de Contenidos:
- 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 Composition2.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 Implementations3.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 LTS to LOTOS; 4.4 Comparing Parallel Operators; 4.5 Sequential Composition; 4.6 Hiding; 4.7 Equivalences and Preorders; 4.8 About CADP; 4.8.1 Getting Started with CADP
- 4.8.2 Verifying Equivalences and Preorders Using CADP4.8.2.1 Verifying Equivalences Using CADP; 4.8.2.2 Verifying Preorders Using CADP; 4.8.3 Generating LTS of Choice Using CADP; 4.8.4 Generating LTS of Recursion Using CADP; 4.9 Full LOTOS-An Introduction; 4.9.1 The Full-LOTOS NOT-Gate Example; 4.9.1.1 The Full LOTOS NOT-File; 4.9.1.2 Applying CADP to Derive LTS for the NOT-Gate; 4.9.2 The Non-Terminating NOT-Gate; 4.9.3 The Max Specifications; 4.9.3.1 Max2 Specification; 4.9.3.2 Max3 Specification; 4.10 The Regular Mu-Calculus (RMC); 4.10.1 Introducing RMC by Examples; 4.11 Further Reading
- 4.12 Selected Solutions4.13 References; 5. Introducing Petri Nets; 5.1 About Petri Nets; 5.1.1 Petri Graphs and Petri Nets; 5.1.2 Enabling and Firing; 5.1.3 Another Definition of Petri Nets; 5.2 About Languages; 5.3 About PETRIFY; 5.4 Illustrating Petri Nets; 5.5 Labeled Nets; 5.6 Bounded Nets; 5.7 Observation Equivalence of LPNs; 5.8 From Blot to Petri Nets; 5.9 Liveness and Persistence; 5.10 Simple Reduction Rules; 5.11 Marked Graphs; 5.12 A Simple Net Algebra; 5.12.1 The Prefix Operator; 5.12.2 The Choice Operator; 5.12.3 The Star Operator; 5.12.4 Parallel Compositions
- 5.12.4.1 The Basic Approach
