Catalog

Record Details

Catalog Search



The spin model checker : primer and reference manual / Gerard J. Holzmann.

Book Book (©2004.)
Description: xii, 596 pages : illustrations ; 25 cm
Publisher: Boston : Addison-Wesley, ©2004.
1 of 1 copy available at NOBLE (All Libraries).
1 of 1 copy available at Gordon College. (Show all copies)
0 current holds with 1 total copy.
Library Location Call Number Status Due Date
Gordon College Stack Level 5 TA 168 .H65 2004 (Text to Phone) Available -

  • ISBN: 0321228626
  • ISBN: 9780321228628
  • ISBN: 9780321773715
  • ISBN: 0321773713
Bibliography, etc.: Includes bibliographical references (pages 545-552) and index.
Contents: 1. Finding Bugs in Concurrent Systems -- 2. Building Verification Models -- 3. An Overview of PROMELA -- 4. Defining Correctness Claims -- 5. Using Design Abstraction -- 6. Automata and Logic -- 7. PROMELA Semantics -- 8. Search Algorithms -- 9. Search Optimization -- 10. Notes on Model Extraction -- 11. Using SPIN -- 12. Notes on XSPIN -- 13. The TimeLine Editor -- 14. A Verification Model of a Telephone Switch -- 15. Sample SPIN Models -- 16. PROMELA Language Reference -- 17. Embedded C Code -- 18. Overview of SPIN Options -- 19. Overview of PAN Options -- App. A. Automata Products -- App. B. The Great Debates -- App. C. Exercises with SPIN -- App. D. Downloading SPIN.
Summary: The SPIN Model Checker is used for both teaching software verification techniques, and for validating large scale applications. The growing number of users has created a need for a more comprehensive user guide and a standard reference manual that describes the most recent version of the tool. This book fills that need. SPIN is used in over 40 countries. The offical SPIN web site, spinroot.com receives between 2500 and 3000 hits per day. It has been estimated that up to three-quarters of the $400 billion spent annually to hire programmers in the United States is ultimately spent on debugging.

Citation:

Holzmann, Gerard J. "The spin model checker : primer and reference manual." Boston : Addison-Wesley, ©2004.

Additional Resources