Guiding Spin simulation

N. Goga, J.M.T. Romijn

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

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.
Original languageEnglish
Title of host publicationFormal Methods and Software Engineering (Proceedings 6th International Conference, ICFEM'2004, Seattle WA, USA, November 8-12, 2004)
EditorsJ. Davies, W. Schulte, M. Barnett
Place of PublicationBerlin
PublisherSpringer
Pages176-193
ISBN (Print)3-540-23841-7
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
Volume3308
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Guiding Spin simulation'. Together they form a unique fingerprint.

  • Cite this

    Goga, N., & Romijn, J. M. T. (2004). Guiding Spin simulation. In J. Davies, W. Schulte, & M. Barnett (Eds.), Formal Methods and Software Engineering (Proceedings 6th International Conference, ICFEM'2004, Seattle WA, USA, November 8-12, 2004) (pp. 176-193). (Lecture Notes in Computer Science; Vol. 3308). Springer. https://doi.org/10.1007/978-3-540-30482-1_20