First SPIN Workshop, October 16, 1995, Verdun, Quebec, Canada
Spin is a general verification tool for proving correctness properties of concurrent/distributed systems specified in the CSP-like modeling language Promela. We extended Promela's syntax to differentiate between external and internal transitions in a given model and the Spin tool with the ability to verify a particular class of semantic relations between two Promela models. This document describes this extension and gives an overview of the relevant theoretical foundations.
INRS-Telecommunications: Proceedings of the First SPIN Workshop (1995).