The Spin Model Checker: Primer and Reference Manual

Hardcover (Print)
Used and New from Other Sellers
Used and New from Other Sellers
from $27.00
Usually ships in 1-2 business days
(Save 63%)
Other sellers (Hardcover)
  • All (7) from $27.00   
  • New (2) from $104.64   
  • Used (5) from $27.00   
Close
Sort by
Page 1 of 1
Showing All
Note: Marketplace items are not eligible for any BN.com coupons and promotions
$104.64
Seller since 2007

Feedback rating:

(5850)

Condition:

New — never opened or used in original packaging.

Like New — packaging may have been opened. A "Like New" item is suitable to give as a gift.

Very Good — may have minor signs of wear on packaging but item works perfectly and has no damage.

Good — item is in good condition but packaging may have signs of shelf wear/aging or torn packaging. All specific defects should be noted in the Comments section associated with each item.

Acceptable — item is in working order but may show signs of wear such as scratches or torn packaging. All specific defects should be noted in the Comments section associated with each item.

Used — An item that has been opened and may show signs of wear. All specific defects should be noted in the Comments section associated with each item.

Refurbished — A used item that has been renewed or updated and verified to be in proper working condition. Not necessarily completed by the original manufacturer.

New
Brand new book. We Pack Carefully and Ship Daily!

Ships from: Miamisburg, OH

Usually ships in 1-2 business days

  • Canadian
  • International
  • Standard, 48 States
  • Standard (AK, HI)
  • Express, 48 States
  • Express (AK, HI)
$224.39
Seller since 2008

Feedback rating:

(191)

Condition: New
0321228626 New. Looks like an interesting title!

Ships from: Naperville, IL

Usually ships in 1-2 business days

  • Standard, 48 States
  • Standard (AK, HI)
Page 1 of 1
Showing All
Close
Sort by

Overview

Master SPIN, the breakthrough tool for improving software reliability

SPIN is the world's most popular, and arguably one of the world's most powerful, tools for detecting software defects in concurrent system designs. Literally thousands of people have used SPIN since it was first introduced almost fifteen years ago. The tool has been applied to everything from the verification of complex call processing software that is used in telephone exchanges, to the validation of intricate control software for interplanetary spacecraft.

This is the most comprehensive reference guide to SPIN, written by the principal designer of the tool. It covers the tool's specification language and theoretical foundation, and gives detailed advice on methods for tackling the most complex software verification problems.

  • Sum Design and verify both abstract and detailed verification models of complex systems software
  • Sum Develop a solid understanding of the theory behind logic model checking
  • Sum Become an expert user of the SPIN command line interface, the Xspin graphical user interface, and the TimeLine editing tool
  • Sum Learn the basic theory of omega automata, linear temporal logic, depth-first and breadth-first search, search optimization, and model extraction from source code

The SPIN software was awarded the prestigious Software System Award by the Association for Computing Machinery (ACM), which previously recognized systems such as UNIX, SmallTalk, TCP/IP, Tcl/Tk, and the World Wide Web.

Read More Show Less

Product Details

  • ISBN-13: 9780321228628
  • Publisher: Addison-Wesley
  • Publication date: 11/1/2003
  • Edition description: New Edition
  • Pages: 608
  • Product dimensions: 7.10 (w) x 9.60 (h) x 1.32 (d)

Meet the Author

DR. GERARD J. HOLZMANN is the principal designer of the SPIN system. Formerly Directory of Computing Principles Research at Bell Laboratories in Murray Hill, N.J., he recently joined NASA's Jet Propulsion Laboratory in Pasadena, CA, to help set up a new Laboratory for Reliable Software. Holzmann's earlier books include Design and Validation of Computer Protocols (Prentice Hall), and The Early History of Data Networks (IEEE CS Press).

Read More Show Less

Read an Excerpt

Preface

''The worst thing about new books is thatthey keep us from reading the old ones.' '(Joseph Joubert, 1754-1824)

A system is correct if it meets its design requirements. This much is agreed.But if the system we are designing is a piece of software, especially if itinvolves concurrency, how can we show this? It is not enough to merely showthat a system can meet its requirements. A few tests generally suffice todemonstrate that. The real test is to show that a system cannot fail to meet itsrequirements.

Dijkstra's well-known dictum on testing1 applies especially to concurrentsoftware: the non-determinism of concurrent system executions makes it hardto devise a traditional test suite with sufficient coverage. There are fundamentalproblems here, related to both the limited controllability of events in distributedsystem executions and to the limited observability of those events.

A well-designed system provably meets its design requirements. But, if wecannot achieve this degree of certainty with standard test methods, what elsecan we do? Using standard mathematics is not much of an option in thisdomain. A thorough hand proof of even simple distributed programs canchallenge the most hardened mathematician. At first blush, mechanical proofprocedures also do not seem to hold much promise: it was shown long ago that it is fundamentally impossible to construct a general proof procedure forarbitrary programs.3 So what gives?

1. The quote ''Program testing can be used to show the presence of bugs, but never to showtheir absence'' first appeared in Dijkstra 1972, p. 6. The quote has a curious pendant in Dijkstra1965 that is rarely mentioned: ''One cannever guarantee that a proof is correct, the bestone can say is: "I have not discovered any mistakes."''

2. For instance, process scheduling decisions made simultaneously by different processors atdistinct locations in a larger network.

Fortunately, if some modest conditions are met, we can mechanically verifythe correctness of distributed systems software. It is the subject of this bookto show what these ''modest conditions'' are and how we can use relativelysimple tool-based verification techniques to tackle demanding software designproblems.LOGIC MODEL CHECKING

The method that we will use to check the correctness of software designs isstandard in most engineering disciplines. The method is called model checking.When the software itself cannot be verified exhaustively, we can build asimplified model of the underlying design that preserves its essential characteristicsbut that avoids known sources of complexity. The design model canoften be verified, while the full-scale implementation cannot.

Bridge builders and airplane designers apply much the same technique whenfaced with complex design problems. By building and analyzing models (orprototypes) the risk of implementing a subtly flawed design is reduced. It isoften too expensive to locate or fix design errors once they hav e reached theimplementation phase. The same is true for the design of complex software.The modeling techniques that we discuss in this book work especially well forconcurrent software, which, as luck will have it, is also the most difficult todebug and test with traditional means.

The models we will build can be seen as little programs, written in, what mayat first look like, a strangely abstract language. The models that are written inthis language are in fact executable. The behaviors they specify can be simulatedand explored exhaustively by the model checker in the hunt for logicerrors. Constructing and executing these high-level models can be fun andinsightful. It often also gives a sufficiently different perspective on a programmingproblem that may lead to new solutions, even before any precise checks are performed.

A logic model checker is designed to use efficient procedures for characterizingall possible executions, rather than a small subset, as one might see in trialexecutions. Since it can explore all behaviors, the model checker can apply arange of sanity checks to the design model, and it can successfully identifyunexecutable code, or potentially deadlocking concurrent executions. It canev en check for compliance with complex user-defined correctness criteria.Model checkers are unequalled in their ability to locate subtle bugs in systemdesigns, providing far greater control than the more traditional methods basedon human inspection, testing, or random simulation.

Model checking techniques have been applied in large scale industrial applications,to reduce the reliance on testing, to detect design flaws early in adesign cycle, or to prove their absence in a final design. Some examples ofthese applications are discussed in this book.THE SPIN MODEL CHECKER

The methodology we describe in this book centers on the use of the modelchecker SPIN. This verification system was developed at Bell Labs in theeighties and nineties and is freely available from the Web (see Appendix D).The tool continues to evolve and has over many years attracted a fairly broadgroup of users in both academia and industry. At the time of writing, SPIN isone of the most widely used logic model checkers in the world.

In 2002 SPIN was recognized by the ACM (the Association for ComputingMachinery) with its most prestigious Software System Award. In receivingthis award, SPIN was placed in the league of truly breakthrough software systemssuch as UNIX, TeX, Smalltalk, Postscript, TCP/IP, and Tcl/Tk. Theaw ard has brought a significant amount of additional attention to the tool andits underlying technology. With all these developments there has been agrowing need for a single authoritative and comprehensive user guide. This book is meant to be that guide.

The material in this book can be used either as classroom material or as aself-study guide for new users who want to learn about the background anduse of logic model checking techniques. A significant part of the book isdevoted to a comprehensive set of reference materials for SPIN that combinesinformation that both novice and experienced users can apply on a daily basis.BOOK STRUCTURE

SPIN can be used to thoroughly check high-level models of concurrent systems.This means that we first have to explain how one can convenientlymodel the behavior of a concurrent system in such a way that SPIN can checkit. Next, we have to show how to define correctness properties for the detailedchecks, and how to design abstraction methods that can be used to renderseemingly complex verification problems tractable. We do all this in the firstpart of this book, Chapters 1 to 5.

The second part, Chapters 6 to 10, provides a treatment of the theory behindsoftware model checking, and a detailed explanation of the fundamental algorithmsthat are used in SPIN.

The third part of the book, Chapters 11 to 15, contains more targeted help ingetting started with the practical application of the tool. In this part of thebook we discuss the command line interface to SPIN, the graphical user interfaceXSPIN, and also a closely related graphical tool that can be used for anintuitive specification of correctness properties, the Timeline editor. This partis concluded with a discussion of the application of SPIN to a range of standardproblems in distributed systems design.

Chapters 16 to 19, the fourth and last part of the book, include a complete setof reference materials for SPIN and its input language, information that was sofar only available in scattered form in books, tutorials, papers, and Web pages.This part contains a full set of manual pages for every language construct andev ery tool option available in the most recent versions of SPIN and XSPIN.The Web site http://spinroot.com/spin/Doc/Book_extras/ contains online versions of all examples used in this book, some lecture materials, and an up to date list of errata.

For courses in model checking techniques, the material included here can provideboth a thorough understanding of the theory of logic model checking andhands-on training with the practical application of a well-known model checkingsystem. For a more targeted use that is focused directly on the practicalapplication of SPIN, the more foundational part of the book can be skipped.A first version of this text was used for several courses in formal verificationtechniques that I taught at Princeton University in New Jersey, at ColumbiaUniversity in New York, and at the Royal Institute of Technology in Stockholm,Sweden, in the early nineties. I am most grateful to everyone who gavefeedback, caught errors, and made suggestions for improvements, as well as toall dedicated SPIN users who have graciously done this throughout the years,and who fortunately continue to do so.

I especially would like to thank Dragan Bosnacki, from Eindhoven Universityin The Netherlands, who read multiple drafts for this book with an unusuallykeen eye for spotting inconsistencies, and intercepting flaws. I would alsolike to thank Al Aho, Rajeev Alur, Jon Bentley, Ramesh Bharadwaj, EdBrinksma, Marsha Chechik, Costas Courcoubetis, Dennis Dams, Matt Dwyer,Vic Du, Kousha Etessami, Michael Ferguson, Rob Gerth, Patrice Godefroid,Jan Hajek, John Hatcliff, Klaus Havelund, Leszek Holenderski, BrianKernighan, Orna Kupferman, Bob Kurshan, Pedro Merino, Alice Miller, DougMcIlroy, Anna Beate Oestreicher, Doron Peled, Rob Pike, Amir Pnueli, AnujPuri, Norman Ramsey, Jim Reeds, Dennis Ritchie, Willem-Paul de Roever,Judi Romijn, Theo Ruys, Ravi Sethi, Margaret Smith, Heikki Tauriainen, KenThompson, Howard Trickey, Moshe Vardi, Phil Winterbottom, Pierre Wolper,Mihalis Yannakakis, and Ozan Yigit, for their often profound influence thathelped to shape the tool, and this book.

Gerard J. Holzmann

gholzmann@acm.org

Read More Show Less

Table of Contents

Preface
Introduction
1 Finding Bugs in Concurrent Systems 1
2 Building Verification Models 7
3 An Overview of PROMELA 33
4 Defining Correctness Claims 73
5 Using Design Abstraction 101
6 Automata and Logic 127
7 PROMELA Semantics 153
8 Search Algorithms 167
9 Search Optimization 191
10 Notes on Model Extraction 217
11 Using SPIN 245
12 Notes on XSPIN 267
13 The TimeLine Editor 283
14 A Verification Model of a Telephone Switch 299
15 Sample SPIN Models 325
16 PROMELA Language Reference 363
17 Embedded C Code 495
18 Overview of SPIN Options 513
19 Overview of PAN Options 527
App. A Automata Products 553
App. B The Great Debates 563
App. C Exercises with SPIN 573
App. D Downloading SPIN 579
Tables and Figures 581
Index 585
Read More Show Less

Preface

Preface

''The worst thing about new books is thatthey keep us from reading the old ones.' '(Joseph Joubert, 1754-1824)

A system is correct if it meets its design requirements. This much is agreed.But if the system we are designing is a piece of software, especially if itinvolves concurrency, how can we show this? It is not enough to merely showthat a system can meet its requirements. A few tests generally suffice todemonstrate that. The real test is to show that a system cannot fail to meet itsrequirements.

Dijkstra's well-known dictum on testing1 applies especially to concurrentsoftware: the non-determinism of concurrent system executions makes it hardto devise a traditional test suite with sufficient coverage. There are fundamentalproblems here, related to both the limited controllability of events in distributedsystem executions and to the limited observability of those events.

A well-designed system provably meets its design requirements. But, if wecannot achieve this degree of certainty with standard test methods, what elsecan we do? Using standard mathematics is not much of an option in thisdomain. A thorough hand proof of even simple distributed programs canchallenge the most hardened mathematician. At first blush, mechanical proofprocedures also do not seem to hold much promise: it was shown long ago that it is fundamentally impossible to construct a general proof procedure forarbitrary programs.3 So what gives?

1. The quote ''Program testing can be used to show the presence of bugs, but never to showtheir absence'' first appeared in Dijkstra 1972, p. 6. The quote has a curious pendant in Dijkstra1965 that is rarely mentioned: ''One can never guarantee that a proof is correct, the bestone can say is: "I have not discovered any mistakes."''

2. For instance, process scheduling decisions made simultaneously by different processors atdistinct locations in a larger network.

Fortunately, if some modest conditions are met, we can mechanically verifythe correctness of distributed systems software. It is the subject of this bookto show what these ''modest conditions'' are and how we can use relativelysimple tool-based verification techniques to tackle demanding software designproblems.

LOGIC MODEL CHECKING

The method that we will use to check the correctness of software designs isstandard in most engineering disciplines. The method is called model checking.When the software itself cannot be verified exhaustively, we can build asimplified model of the underlying design that preserves its essential characteristicsbut that avoids known sources of complexity. The design model canoften be verified, while the full-scale implementation cannot.

Bridge builders and airplane designers apply much the same technique whenfaced with complex design problems. By building and analyzing models (orprototypes) the risk of implementing a subtly flawed design is reduced. It isoften too expensive to locate or fix design errors once they hav e reached theimplementation phase. The same is true for the design of complex software.The modeling techniques that we discuss in this book work especially well forconcurrent software, which, as luck will have it, is also the most difficult todebug and test with traditional means.

The models we will build can be seen as little programs, written in, what mayat first look like, a strangely abstract language. The models that are written inthis language are in fact executable. The behaviors they specify can be simulatedand explored exhaustively by the model checker in the hunt for logicerrors. Constructing and executing these high-level models can be fun andinsightful. It often also gives a sufficiently different perspective on a programmingproblem that may lead to new solutions, even before any precise checks are performed.

A logic model checker is designed to use efficient procedures for characterizingall possible executions, rather than a small subset, as one might see in trialexecutions. Since it can explore all behaviors, the model checker can apply arange of sanity checks to the design model, and it can successfully identifyunexecutable code, or potentially deadlocking concurrent executions. It canev en check for compliance with complex user-defined correctness criteria.Model checkers are unequalled in their ability to locate subtle bugs in systemdesigns, providing far greater control than the more traditional methods basedon human inspection, testing, or random simulation.

Model checking techniques have been applied in large scale industrial applications,to reduce the reliance on testing, to detect design flaws early in adesign cycle, or to prove their absence in a final design. Some examples ofthese applications are discussed in this book.

THE SPIN MODEL CHECKER

The methodology we describe in this book centers on the use of the modelchecker SPIN. This verification system was developed at Bell Labs in theeighties and nineties and is freely available from the Web (see Appendix D).The tool continues to evolve and has over many years attracted a fairly broadgroup of users in both academia and industry. At the time of writing, SPIN isone of the most widely used logic model checkers in the world.

In 2002 SPIN was recognized by the ACM (the Association for ComputingMachinery) with its most prestigious Software System Award. In receivingthis award, SPIN was placed in the league of truly breakthrough software systemssuch as UNIX, TeX, Smalltalk, Postscript, TCP/IP, and Tcl/Tk. Theaw ard has brought a significant amount of additional attention to the tool andits underlying technology. With all these developments there has been agrowing need for a single authoritative and comprehensive user guide. Thisbook is meant to be that guide.

The material in this book can be used either as classroom material or as aself-study guide for new users who want to learn about the background anduse of logic model checking techniques. A significant part of the book isdevoted to a comprehensive set of reference materials for SPIN that combinesinformation that both novice and experienced users can apply on a daily basis.

BOOK STRUCTURE

SPIN can be used to thoroughly check high-level models of concurrent systems.This means that we first have to explain how one can convenientlymodel the behavior of a concurrent system in such a way that SPIN can checkit. Next, we have to show how to define correctness properties for the detailedchecks, and how to design abstraction methods that can be used to renderseemingly complex verification problems tractable. We do all this in the firstpart of this book, Chapters 1 to 5.

The second part, Chapters 6 to 10, provides a treatment of the theory behindsoftware model checking, and a detailed explanation of the fundamental algorithmsthat are used in SPIN.

The third part of the book, Chapters 11 to 15, contains more targeted help ingetting started with the practical application of the tool. In this part of thebook we discuss the command line interface to SPIN, the graphical user interfaceXSPIN, and also a closely related graphical tool that can be used for anintuitive specification of correctness properties, the Timeline editor. This partis concluded with a discussion of the application of SPIN to a range of standardproblems in distributed systems design.

Chapters 16 to 19, the fourth and last part of the book, include a complete setof reference materials for SPIN and its input language, information that was sofar only available in scattered form in books, tutorials, papers, and Web pages.This part contains a full set of manual pages for every language construct andev ery tool option available in the most recent versions of SPIN and XSPIN.The Web site http://spinroot.com/spin/Doc/Book_extras/ contains online versions of all examples used in this book, some lecture materials, and an up to date list of errata.

For courses in model checking techniques, the material included here can provideboth a thorough understanding of the theory of logic model checking andhands-on training with the practical application of a well-known model checkingsystem. For a more targeted use that is focused directly on the practicalapplication of SPIN, the more foundational part of the book can be skipped.A first version of this text was used for several courses in formal verificationtechniques that I taught at Princeton University in New Jersey, at ColumbiaUniversity in New York, and at the Royal Institute of Technology in Stockholm,Sweden, in the early nineties. I am most grateful to everyone who gavefeedback, caught errors, and made suggestions for improvements, as well as toall dedicated SPIN users who have graciously done this throughout the years,and who fortunately continue to do so.

I especially would like to thank Dragan Bosnacki, from Eindhoven Universityin The Netherlands, who read multiple drafts for this book with an unusuallykeen eye for spotting inconsistencies, and intercepting flaws. I would alsolike to thank Al Aho, Rajeev Alur, Jon Bentley, Ramesh Bharadwaj, EdBrinksma, Marsha Chechik, Costas Courcoubetis, Dennis Dams, Matt Dwyer,Vic Du, Kousha Etessami, Michael Ferguson, Rob Gerth, Patrice Godefroid,Jan Hajek, John Hatcliff, Klaus Havelund, Leszek Holenderski, BrianKernighan, Orna Kupferman, Bob Kurshan, Pedro Merino, Alice Miller, DougMcIlroy, Anna Beate Oestreicher, Doron Peled, Rob Pike, Amir Pnueli, AnujPuri, Norman Ramsey, Jim Reeds, Dennis Ritchie, Willem-Paul de Roever,Judi Romijn, Theo Ruys, Ravi Sethi, Margaret Smith, Heikki Tauriainen, KenThompson, Howard Trickey, Moshe Vardi, Phil Winterbottom, Pierre Wolper,Mihalis Yannakakis, and Ozan Yigit, for their often profound influence thathelped to shape the tool, and this book.

Gerard J. Holzmann

gholzmann@acm.org

Read More Show Less

Customer Reviews

Be the first to write a review
( 0 )
Rating Distribution

5 Star

(0)

4 Star

(0)

3 Star

(0)

2 Star

(0)

1 Star

(0)

Your Rating:

Your Name: Create a Pen Name or

Barnes & Noble.com Review Rules

Our reader reviews allow you to share your comments on titles you liked, or didn't, with others. By submitting an online review, you are representing to Barnes & Noble.com that all information contained in your review is original and accurate in all respects, and that the submission of such content by you and the posting of such content by Barnes & Noble.com does not and will not violate the rights of any third party. Please follow the rules below to help ensure that your review can be posted.

Reviews by Our Customers Under the Age of 13

We highly value and respect everyone's opinion concerning the titles we offer. However, we cannot allow persons under the age of 13 to have accounts at BN.com or to post customer reviews. Please see our Terms of Use for more details.

What to exclude from your review:

Please do not write about reviews, commentary, or information posted on the product page. If you see any errors in the information on the product page, please send us an email.

Reviews should not contain any of the following:

  • - HTML tags, profanity, obscenities, vulgarities, or comments that defame anyone
  • - Time-sensitive information such as tour dates, signings, lectures, etc.
  • - Single-word reviews. Other people will read your review to discover why you liked or didn't like the title. Be descriptive.
  • - Comments focusing on the author or that may ruin the ending for others
  • - Phone numbers, addresses, URLs
  • - Pricing and availability information or alternative ordering information
  • - Advertisements or commercial solicitation

Reminder:

  • - By submitting a review, you grant to Barnes & Noble.com and its sublicensees the royalty-free, perpetual, irrevocable right and license to use the review in accordance with the Barnes & Noble.com Terms of Use.
  • - Barnes & Noble.com reserves the right not to post any review -- particularly those that do not follow the terms and conditions of these Rules. Barnes & Noble.com also reserves the right to remove any review at any time without notice.
  • - See Terms of Use for other conditions and disclaimers.
Search for Products You'd Like to Recommend

Recommend other products that relate to your review. Just search for them below and share!

Create a Pen Name

Your Pen Name is your unique identity on BN.com. It will appear on the reviews you write and other website activities. Your Pen Name cannot be edited, changed or deleted once submitted.

 
Your Pen Name can be any combination of alphanumeric characters (plus - and _), and must be at least two characters long.

Continue Anonymously
Sort by: Showing all of 2 Customer Reviews
  • Anonymous

    Posted May 8, 2004

    Best introduction to model checking

    This book is one of the best introductions to logic model checking techniques that I've read so far. It explains clearly how one can build concise verification models for multi-threaded systems applications, and use Spin to find the bugs. In my work, this type of tool is priceless. Highly recommended.

    Was this review helpful? Yes  No   Report this review
  • Anonymous

    Posted November 25, 2003

    worth waiting for

    I've been using the Spin tool for 5 years to find bugs in my designs and software and have been eagerly awaiting this book. The book is great! The one-stop shopping approach works well - the modeling language, some theory, and a lot of practical information; all in one book. I think it would be a good book for those just starting to use Spin and it's the essential reference for an experienced Spin user.

    Was this review helpful? Yes  No   Report this review
Sort by: Showing all of 2 Customer Reviews

If you find inappropriate content, please report it to Barnes & Noble
Why is this product inappropriate?
Comments (optional)