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.
This research is supported by NWO under project 016.023.015 “Improving the Quality of Protocol Standards”, URL: http://www.win.tue.nl/oas/iqps/index.html.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Blom, S., Fokkink, W.J., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: mgrCRL: A toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)
Burns, A., Spelberg, R.L., Toetenel, H., Vink, T.: Modeling and verification using XTG and PMC. In: Proc. of the 5th annual conf. of ASCI (1999)
Clarke, E., Grumberg, O., Long, D.: Verification Tools for Finite State Concurrent Systems. In: A Decade of Concurrency-Reflections and Perspectives, vol. 803, pp. 124–175. Springer, Heidelberg (1993)
David, L.D., Andreas, J.D., Alan, J.H., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522–525 (1992)
Garavel, H., Lang, F., Mateescu, R.: An overview of CADP 2001. EASST Newsletter 4, 13–24 (2002); Also available as INRIA Technical Report RT-254
Gunter, E.L., Peled, D.A.: Temporal debugging for concurrent systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 431–444. Springer, Heidelberg (2002)
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: The next generation. In: Proc. of RTSS 1995, pp. 56–65 (1995)
Holzmann, G.J.: The Spin Model Checker–Primer and Reference Manual. Addison-Wesley, Reading (2003), See also URL http://www.spinroot.com/
The Institute of Electrical And Electronics Engineers, Inc. IEEE Standard for a High Performance Serial Bus, IEEE Std 1394-1995 (August 1996)
The Institute of Electrical And Electronics Engineers, Inc. IEEE P1394.1 Draft Standard for High Performance Serial Bus Bridges, Version 1.05 (November 2003)
van Langevelde, I.A., Romijn, J.M.T., Goga, N.: Founding firewire bridges through promela prototyping. In: Proc. of FMPPTA 2003, IEEE Computer Society Press, Los Alamitos (2003)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1(1–2), 134–152 (1997)
Romijn, J.M.T.: Improving the quality of protocol standards: Correcting IEEE 1394.1 firewire net update. Newsletter of the NVTI 8, 23–30 (2004)
Sihman, M., Katz, S.: A calculus of superimpositions for distributed systems. In: Proceedings of AOSD 2002, pp. 28–40. ACM Press, New York (2002)
Sweden Telelogic AB. Telelogic Tau Guide (1998)
Yovine, S.: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1, 123–133 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goga, N., Romijn, J. (2004). Guiding Spin Simulation. In: Davies, J., Schulte, W., Barnett, M. (eds) Formal Methods and Software Engineering. ICFEM 2004. Lecture Notes in Computer Science, vol 3308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30482-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-30482-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23841-6
Online ISBN: 978-3-540-30482-1
eBook Packages: Springer Book Archive