VOLUME Thirty Two
TITLE: "The Spin Verification System"
EDITORS: Jean-Charles Grégoire, Gerard J. Holzmann and Doron A. Peled.

Ordering Information

To order through AMS contact the AMS Customer Services Department, P.O. Box 6248, Providence, Rhode Island 02940-6248 USA. For Visa, Mastercard, Discover, and American Express orders call 1-800-321-4AMS.

You may also visit the AMS Bookstore and order directly from there. DIMACS does not distribute or sell these books.

• 1. Preface
• 2. Table of Contents

PREFACE

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.

TABLE OF CONTENTS

• J. Grégoire -- State space compression with graph encoded sets
• G. J. Holzmann and O. Kupferman -- Not checking for closure under stuttering
• J. G., D. Peled, and M. Yannakakis -- On nested depth first search
• H. E. Jensen, K. G. Larsen, and A. Skou -- Modelling and analysis of a collision avoidance protocol using Spin and Uppaal
• P. Kars -- The application of Promela and Spin in the BOS project
• S. Leue and P. B. Ladkin -- Implementing and verifying MSC specifications using Promela/XSpin
• S. Löffler and A. Serhrouchni -- Creating implementations from Promela models
• P. Merino and J. Troya -- Modelling and verification of the MCS layer with Spin
• E. Najm and F. Olsen -- Protocol verification with reactive Promela/Rspin
• V. Natarajan and J. G. -- Outline for an operational semantics of Promela
• S. K. Shukla, D. J. Rosenkrantz, and S. S. Ravi -- A simulation and validation tool for self-stabilizing protocols
• J. Tuya, J. R. de Diego, C. de la Riva, and J. A. Corrales -- Dynamic analysis of SA/RT models using Spin and modular verification
• W. Visser and H. Barringer -- Memory efficient state storage in Spin

Index of Volumes

DIMACS Homepage