Item Successfully Added to Cart
An error was encountered while trying to add the item to the cart. Please try again.
OK
Please make all selections above before adding to cart
OK
The following link can be shared to navigate to this page. You can select the link to copy or click the 'Copy To Clipboard' button below.
Copy To Clipboard
Successfully Copied!
The SPIN Verification System
 
Edited by: Jean-Charles Grégoire INRS-Telecommunications, Montreal, QC, Canada
Gerard J. Holzmann Lucent Technologies, Murray Hill, NJ
Doron A. Peled Lucent Technologies, Murray Hill, NJ
A co-publication of the AMS and DIMACS
Front Cover for The SPIN Verification System
Available Formats:
Hardcover ISBN: 978-0-8218-0680-7
Product Code: DIMACS/32
List Price: $67.00
MAA Member Price: $60.30
AMS Member Price: $53.60
Electronic ISBN: 978-1-4704-3990-3
Product Code: DIMACS/32.E
List Price: $63.00
MAA Member Price: $56.70
AMS Member Price: $50.40
Bundle Print and Electronic Formats and Save!
This product is available for purchase as a bundle. Purchasing as a bundle enables you to save on the electronic version.
List Price: $100.50
MAA Member Price: $90.45
AMS Member Price: $80.40
Front Cover for The SPIN Verification System
Click above image for expanded view
  • Front Cover for The SPIN Verification System
  • Back Cover for The SPIN Verification System
The SPIN Verification System
Edited by: Jean-Charles Grégoire INRS-Telecommunications, Montreal, QC, Canada
Gerard J. Holzmann Lucent Technologies, Murray Hill, NJ
Doron A. Peled Lucent Technologies, Murray Hill, NJ
A co-publication of the AMS and DIMACS
Available Formats:
Hardcover ISBN:  978-0-8218-0680-7
Product Code:  DIMACS/32
List Price: $67.00
MAA Member Price: $60.30
AMS Member Price: $53.60
Electronic ISBN:  978-1-4704-3990-3
Product Code:  DIMACS/32.E
List Price: $63.00
MAA Member Price: $56.70
AMS Member Price: $50.40
Bundle Print and Electronic Formats and Save!
This product is available for purchase as a bundle. Purchasing as a bundle enables you to save on the electronic version.
List Price: $100.50
MAA Member Price: $90.45
AMS Member Price: $80.40
  • Book Details
     
     
    DIMACS - Series in Discrete Mathematics and Theoretical Computer Science
    Volume: 321997; 203 pp
    MSC: Primary 68;

    What is Spin? Spin is a general tool for the specification and formal verification of software for distributed systems. It has been used to detect design errors in a wide range of applications, such as abstract distributed algorithms, data communications protocols, operating systems code, and telephone switching code. The verifier can check for basic correctness properties, such as absence of deadlock and race conditions, logical completeness, or unwarranted assumptions about the relative speeds of correctness properties expressed in the syntax of Linear-time Temporal Logic (LTL). The tool translates LTL formulae automatically into automata representations, which can be used in an efficient on-the-fly verifications procedure.

    This DIMACS volume presents the papers contributed to the second international workshop that was held on the Spin verification system at Rutgers University in August 1996. The work covers theoretical and foundational studies of formal verification, empirical studies of the effectiveness of different types of algorithms, significant practical applications of the Spin verifier, and discussions of extensions and revisions of the basic code.

    Readership

    Graduate students, theorists and practicioners in formal methods, formal verification of software and automata theory.

  • Table of Contents
     
     
    • Chapters
    • State space compression with graph encoded sets
    • Not checking for closure under stuttering
    • On nested depth first search
    • Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL
    • The application of PROMELA and SPIN in the BOS project
    • Implementing and verifying MSC specifications using PROMELA/XSPIN
    • Creating implementations from PROMELA models
    • Modelling and verification of the MCS layer with SPIN
    • Protocol verification with reactive PROMELA/RSPIN
    • Outline for an operational semantics of PROMELA
    • A simulation and validation tool for self-stabilizing protocols
    • Dynamic analysis of SA/RT models using SPIN and modular verification
    • Memory efficient state storage in SPIN
  • Request Review Copy
Volume: 321997; 203 pp
MSC: Primary 68;

What is Spin? Spin is a general tool for the specification and formal verification of software for distributed systems. It has been used to detect design errors in a wide range of applications, such as abstract distributed algorithms, data communications protocols, operating systems code, and telephone switching code. The verifier can check for basic correctness properties, such as absence of deadlock and race conditions, logical completeness, or unwarranted assumptions about the relative speeds of correctness properties expressed in the syntax of Linear-time Temporal Logic (LTL). The tool translates LTL formulae automatically into automata representations, which can be used in an efficient on-the-fly verifications procedure.

This DIMACS volume presents the papers contributed to the second international workshop that was held on the Spin verification system at Rutgers University in August 1996. The work covers theoretical and foundational studies of formal verification, empirical studies of the effectiveness of different types of algorithms, significant practical applications of the Spin verifier, and discussions of extensions and revisions of the basic code.

Readership

Graduate students, theorists and practicioners in formal methods, formal verification of software and automata theory.

  • Chapters
  • State space compression with graph encoded sets
  • Not checking for closure under stuttering
  • On nested depth first search
  • Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL
  • The application of PROMELA and SPIN in the BOS project
  • Implementing and verifying MSC specifications using PROMELA/XSPIN
  • Creating implementations from PROMELA models
  • Modelling and verification of the MCS layer with SPIN
  • Protocol verification with reactive PROMELA/RSPIN
  • Outline for an operational semantics of PROMELA
  • A simulation and validation tool for self-stabilizing protocols
  • Dynamic analysis of SA/RT models using SPIN and modular verification
  • Memory efficient state storage in SPIN
Please select which format for which you are requesting permissions.