Guiding Spin simulation

N. Goga; J.M.T. Romijn

doi:10.1007/978-3-540-30482-1_20

Guiding Spin simulation

N. Goga, J.M.T. Romijn

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Formal Methods and Software Engineering (Proceedings 6th International Conference, ICFEM'2004, Seattle WA, USA, November 8-12, 2004)
Editors	J. Davies, W. Schulte, M. Barnett
Place of Publication	Berlin
Publisher	Springer
Pages	176-193
ISBN (Print)	3-540-23841-7
DOIs	https://doi.org/10.1007/978-3-540-30482-1_20
Publication status	Published - 2004

Publication series

Name	Lecture Notes in Computer Science
Volume	3308
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-540-30482-1_20

Cite this

@inproceedings{a240458a50ed413d94aa4060833e523f,

title = "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.",

author = "N. Goga and J.M.T. Romijn",

year = "2004",

doi = "10.1007/978-3-540-30482-1_20",

language = "English",

isbn = "3-540-23841-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "176--193",

editor = "J. Davies and W. Schulte and M. Barnett",

booktitle = "Formal Methods and Software Engineering (Proceedings 6th International Conference, ICFEM'2004, Seattle WA, USA, November 8-12, 2004)",

address = "Germany",

}

Guiding Spin simulation. / Goga, N.; Romijn, J.M.T.
Formal Methods and Software Engineering (Proceedings 6th International Conference, ICFEM'2004, Seattle WA, USA, November 8-12, 2004). ed. / J. Davies; W. Schulte; M. Barnett. Berlin: Springer, 2004. p. 176-193 (Lecture Notes in Computer Science; Vol. 3308).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Guiding Spin simulation

AU - Goga, N.

AU - Romijn, J.M.T.

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-30482-1_20

DO - 10.1007/978-3-540-30482-1_20

M3 - Conference contribution

SN - 3-540-23841-7

T3 - Lecture Notes in Computer Science

SP - 176

EP - 193

BT - Formal Methods and Software Engineering (Proceedings 6th International Conference, ICFEM'2004, Seattle WA, USA, November 8-12, 2004)

A2 - Davies, J.

A2 - Schulte, W.

A2 - Barnett, M.

PB - Springer

CY - Berlin

ER -

Guiding Spin simulation

Abstract

Publication series

Access to Document

Fingerprint

Cite this