HOME > Detail View

Detail View

Temporal verification of reactive systems : safety

Temporal verification of reactive systems : safety (Loan 1 times)

Material type
단행본
Personal Author
Manna, Zohar. Pnueli, A.
Title Statement
Temporal verification of reactive systems : safety / Zohar Manna, Amir Pnueli.
Publication, Distribution, etc
New York :   Springer ,   c1995.  
Physical Medium
xviii, 512 p. : ill. ; 25 cm.
ISBN
0387944591 (acid-free paper) 9780387944593
Bibliography, Etc. Note
Includes bibliographical references (p. [465]-479) and indexes.
Subject Added Entry-Topical Term
Computer software -- Verification. Parallel processing (Electronic computers)
000 00928camuu2200277 a 4500
001 000045426384
005 20080312091744
008 950119s1995 nyua b 001 0 eng
010 ▼a 95005442
020 ▼a 0387944591 (acid-free paper)
020 ▼a 9780387944593
035 ▼a (KERIS)REF000014734411
040 ▼a DLC ▼c DLC ▼d DLC ▼d 211009
050 0 0 ▼a QA76.76.V47 ▼b M36 1995
082 0 0 ▼a 005.2 ▼2 22
090 ▼a 005.2 ▼b M282t
100 1 ▼a Manna, Zohar.
245 1 0 ▼a Temporal verification of reactive systems : ▼b safety / ▼c Zohar Manna, Amir Pnueli.
260 ▼a New York : ▼b Springer , ▼c c1995.
300 ▼a xviii, 512 p. : ▼b ill. ; ▼c 25 cm.
504 ▼a Includes bibliographical references (p. [465]-479) and indexes.
650 0 ▼a Computer software ▼x Verification.
650 0 ▼a Parallel processing (Electronic computers)
700 1 ▼a Pnueli, A.
945 ▼a KINS

Holdings Information

No. Location Call Number Accession No. Availability Due Date Make a Reservation Service
No. 1 Location Science & Engineering Library/Sci-Info(Stacks2)/ Call Number 005.2 M282t Accession No. 121165987 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents

0: Preliminary Concepts.- 0.1 Fair Transition System.- 0.2 A Programming Language (SPL): Syntax.- 0.3 A Programming Language (SPL): Semantics.- 0.4 Modules.- 0.5 Temporal Logic.- 0.6 Specification of Properties.- 0.7 Overview of the Verification Framework.- Problems.- Bibliographic Remarks.- 1: Invariance: Proof Methods.- 1.1 Preliminary Notions.- 1.2 Invariance Rule.- 1.3 Finding Inductive Assertions: The Bottom-Up Approach.- 1.4 Finding Inductive Assertions: The Top-Down Approach.- 1.5 Refining Invariants.- Problems.- Bibliographic Remarks.- 2: Invariance: Applications.- 2.1 Parameterized Programs.- 2.2 Single-Resource Allocation.- 2.3 Multiple-Resource Allocation.- 2.4 Constructing Linear Invariants.- 2.5 Completeness.- 2.6 Finite-State Algorithmic Verification.- Problems.- Bibliographic Remarks.- 3: Precedence.- 3.1 Waiting-for Rule.- 3.2 Nested Waiting-for Rule.- 3.3 Verification Diagrams.- 3.4 Overtaking Analysis for a Resource Allocator.- 3.5 Completeness.- 3.6 Finite-State Algorithmic Verification.- Problems.- Bibliographic Remarks.- 4: General Safety.- 4.1 Invariance Rule for Past Formulas.- 4.2 Applications of the Past Invariance Rule.- 4.3 Compositional Verification.- 4.4 Causality Rule.- 4.5 Backward Analysis.- 4.6 Order-Preservation Properties.- 4.7 History Variables.- 4.8 Back-to Rule.- 4.9 Completeness.- 4.10 Finite-State Algorithmic Verification.- Problems.- Bibliographic Remarks.- 5: Algorithmic Verification of General Formulas.- 5.1 Satisfiability of a Temporal Formula.- 5.2 Satisfiability over a Finite-State Program.- 5.3 Validity over a Finite-State Program: Examples.- 5.4 Incremental Tableau Construction.- 5.5 Particle Tableaux.- Problems.- Bibliographic Remarks.- References.- Index to Symbols.- General Index.


Information Provided By: : Aladin

New Arrivals Books in Related Fields

이창현 (2021)