Logo - springer
Slogan - springer

Computer Science - Software Engineering | Principles of the Spin Model Checker

Principles of the Spin Model Checker

Ben-Ari, Mordechai


Available Formats:

Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.

You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.

After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.


(net) price for USA

ISBN 978-1-84628-770-1

digitally watermarked, no DRM

Included Format: PDF

download immediately after purchase

learn more about Springer eBooks

add to marked items


Softcover (also known as softback) version.

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.


(net) price for USA

ISBN 978-1-84628-769-5

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days

add to marked items

  • First introductory textbook on Spin
  • Includes complete programs which will demonstrate construct and concept; these programs will also be available on a companion website
  • Promela and Spin are presented in a graduated manner to facilitate easy learning

The Spin model checker is a widely used professional software tool for specifying and verifying concurrent and distributed systems. Models, written in a simple language called Promela, can be simulated randomly or interactively. Spin can generate efficient verifiers that search for a counterexample to correctness specifications applied to a model.

Spin is also a superb tool for teaching important concepts of computer science such as verification, concurrency and nondeterminism. The Promela language is easy to learn, as is the linear temporal logic used for correctness specifications, and the techniques for simulating and verifying models.

Principles of Spin is an introductory book for students and practicing software engineers who wish to learn Promela and Spin. The presentation starts with the verification of sequential programs and proceeds in gradual stages to the verification of concurrent and then distributed programs. Complete programs are used to demonstrate each construct and concept, and the source code of these programs, together with that of longer case studies, are available on the companion website.

The book describes free software that the author has developed: jSpin—an integrated development environment for Spin, SpinSpider—a visualization tool that automatically constructs graphical state diagrams of concurrent programs, and VN—a Spin-based tool for visualizing nondeterminism of finite automata.

Mordechai Ben-Ari is an associate professor in the Department of Science Teaching of the Weizmann Institute of Science. He is the author of numerous textbooks on concurrency, programming languages and logic, and has developed software tools for teaching concurrency. In 2004, Ben-Ari received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education.

Content Level » Graduate

Keywords » Algorithms - Automat - Exception - PROMELA - SPIN - Variable - algorithm - automata - data structure - data structures - distributed systems - modeling - programming - real-time

Related subjects » Software Engineering - Theoretical Computer Science

Table of contents 

Foreword.- Preface.- Sequential Programming in PROMELA.- A First Program in PROMELA.- Random Simulation- Data Types.- Operators and Expressions.- Control Statements.- Repetitive Statements.- Jump Statements.- Verification of Sequential Programs.- Assertions.- Verifying a program in Spin.- Concurrency.- Interleaving.- Atomicity.- Interactive Simulation.- Interference between processes.- Sets of Processes.- Interference revisited.- Deterministic Sequences of Statements.- Verification with Assertions.- The critical section problem.- Synchroniztion.- Synchronization by blocking.- Executability of statements.- State transition diagrams.- Atomic sequences of statements.- Semaphores.- Nondeterminism in models of concurrent systems.- Termination of Processes.- Verification with Temporal Logic.- Beyond Assertions.- Introduction to linear temporal logic.- Safety properties.- Liveness properties.- Fairness.- Duality.- Verifying correctness without ghost variables.- Modeling a non-critical section.- Advanced temporal specifications.- Data and Program Structures.- Arrays.- Type Definitions.- The preprocessor.- Inline.- Channels.- Channels in PROMELA.- Rendezvous channels.- Buffered channels.- Checking the content of a channel.- Random receive*.- Sorted send*.- Copying the value of a message*.- Polling*.- Comparing rendezvous and buffered channels.- Nondeterminism*.- Nondeterministic finite automata.- VN: Visualizing Nondeterminism.- NP problems.- Advanced Topics in PROMELA*.- Specifiers for Variables.- Predefined variables.- Priority.- Modeling Exceptions.- Reading from standard input.- Embedded C code.- Advanced Topics in SPIN*.- How SPIN searches the state space.- Optimizing the performances of verifications.- Never claims.- Non-progress cycles.- Case Studies* .- Channels as data structures.- Nondeterministic algorithms.- Modeling a real-time scheduling algorithm.- Fischer’s algorithm.- Modeling distributed systems.- The Chandy-Lamport algorithm for global snapshots.- TheChandy-Lamport snapshot algorithm in PROMELA.- Verification of the snapshot algorithm.- Appendix A: Software Tools.- Appendix B: Links.- References.- Index

Popular Content within this publication 



Read this Book on Springerlink

Services for this book

New Book Alert

Get alerted on new Springer publications in the subject area of Software Engineering / Programming and Operating Systems.