Guiding Spin simulation

N. Goga, J.M.T. Romijn

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

    1 Citation (Scopus)


    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
    ISBN (Print)3-540-23841-7
    Publication statusPublished - 2004

    Publication series

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


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

    Cite this