Verification of systems and circuits using LOTOS, Petri Nets, and CCS / by Michael Yoeli and Rakefet Kol.

Format:

Book

Author/Creator:

Yoeli, Michael, 1917-

Contributor:

Kol, Rakefet.

Series:

Wiley series on parallel and distributed computing.

Wiley series on parallel and distributed computing

Language:

English

Subjects (All):

Integrated circuits--Verification.

Integrated circuits.

Computer software--Verification.

Computer software.

LOTOS (Computer program language).

Petri nets.

Physical Description:

1 online resource (249 p.)

Edition:

1st edition

Place of Publication:

Hoboken, N.J. : Wiley-Interscience, c2008.

Language Note:

English

System Details:

text file

Summary:

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 CADP, Petri nets-based PETRIFY, and CCS-based CWB. The book covers verification of modular asynchronous circuits, alternating-bit protocols, arbiters, pipeline controllers, up-down counters, and phase converters, as well as many other verification examples. Using the given detailed examples, exerci

Contents:

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

Notes:

Description based upon print version of record.

Includes bibliographical references and index.

Description based on metadata supplied by the publisher and other sources.

ISBN:

9786611284671

9781281284679

128128467X

9780470253410

047025341X

9780470253397

0470253398

OCLC:

232611995