Guiding Spin Simulation

9 years 3 months ago
Guiding Spin Simulation
Abstract. In this paper we present a technique for the Spin tool, inspired by practical experiences with Spin and a FireWire protocol. We show how to guide simulations with Spin, by constructing a special guide process that limits the behaviour of the original system. We set up a theoretical framework in which we prove under some sufficient conditions that the adjusted system (with the added guide process) exhibits a subset of the behaviour of the original system, and has no new deadlocks. We have applied this technique to a Promela specification of the IEEE 1394.1 FireWire net update algorithm. The experiment shows that this technique increases the error detecting power of Spin in the sense that we found errors in the guided specification, which could not be discovered with Spin simulation and validation in the original specification.
Nicolae Goga, Judi Romijn
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Authors Nicolae Goga, Judi Romijn
Comments (0)