Abstract
One of the difficulties of using model checkers “in the large” is the management of all (generated) data during the validation trajectory. It is important that the results obtained from the validation are always reproducible. Without tool support, the quality of the validation process depends on the accuracy of the persons who conduct the validation. This paper discusses Xspin/Project, an extension of Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin.
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
Wayne A. Babich. Software Configuration Management: Coordination for team productivity. Addison-Wesley, Reading, MA, 1986.
Brian Berliner. CVS II: Parallelizing Software Development. In Proceedings of the Winter1990 USENIX Conference, January 22-26, 1990, Washington DC, USA, pages 341–352, Berkeley, CA, USA, January 1990. USENIX.
Reidar Conradi and Bernhard Westfechtel. Version Models for Software Configuration Management. ACM Computing Surveys, 30(2):232–282, June 1998.
Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, and G. Jan Tretmans. The Bounded Retransmission Protocol must be on time! In Ed Brinksma, editor, Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97), number 1217 in Lecture Notes in Computer Science (LNCS), pages 416–431, University of Twente, Enschede, The Netherlands, April 1997. Springer Verlag, Berlin.
Susan Dart. Concepts in Configuration Management Systems. In P.H. Feiler, editor, Proceedings of the Third International Workshop on Software Configuration Management (SCM’91), pages 1–18, Trondheim, Norway, June 1997. ACM SIGSOFT, ACM Press, New York.
Stuart I. Feldman. Make A Program for Maintaining Computer Programs. Software Practice and Experience, 9(3):255–265, March 1979.
Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, New Jersey, 1991. Xspin/Project-Integrated Validation Management for Xspin 119
Gerard J. Holzmann. The Theory and Practice of a Formal Method: NewCore. In Proceedings of the IFIP World Congress, Hamburg, Germany, August 1994. Also available from URL: http://cm.bell-labs.com/cm/cs/doc/94/index.html.
Gerard J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997. See also URL: http://netlib.bell-labs.com/netlib/spin/whatispin.html.
IEEE. IEEE Standard Glossary of Software Engineering Terminology: IEEE Standard 729-1983. IEEE, New York, 1983.
IEEE. IEEE Guide to Software Configuration Management: ANSI/IEEE Std1042–1987. IEEE, New York, 1987.
Donald E. Knuth. Literate Programming. The Computer Journal, 27(2):97–111, May 1984.
David B. Leblang and Paul H. Levine. Software Configuration Management: Why is it needed and what should it do? In Jacky Estublier, editor, ICSE SCM-4 and SCM-5 Workshops Selected Papers, number 1005 in Lecture Notes in Computer Science (LNCS), pages 53–60. Springer Verlag, Berlin, 1995.
Josh MacDonald. PRCS Project Revision Control System. Available from URL: http://www.xcf.berkeley.edu/~jmacd/prcs.html.
Josh MacDonald, Paul N. Hilffinger, and Luigi Semenzato. PRCS: The Project Revision Control System. In B. Magnusson, editor, Proceedings of the ECOOP’98 SCM-8 Symposium on Software Configuration Management (SCM’98), number 1439 in Lecture Notes in Computer Science (LNCS), pages 33–45, Brussels, Belgium, July 1998. Springer Verlag, Berlin.
John K. Ousterhout. Tcl and the Tk Toolkit. Addison-Wesley Publishing Company, Reading, Massachusetts, 1994.
Roger S. Pressman. Software Engineering A Practioner’s Approach. McGraw-Hill, New York, third edition, 1992.
Theo C. Ruys and Ed Brinksma. Experience with Literate Programming in the Modelling and Validation of Systems. In Bernhard Steffen, editor, Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), number 1384 in Lecture Notes in Computer Science (LNCS), pages393–408, Lisbon, Portugal, April 1998. Springer Verlag, Berlin.
Theo C. Ruys and Rom Langerak. Validation of Bosch’ Mobile Communication Network Architecture with SPIN. In Proceedings of SPIN97, the Third International Workshop on SPIN,University of Twente, Enschede, The Netherlands, April 1997. Also available from URL:http://netlib.bell_abs.com/netlib/spin/ws97/ruys.ps.Z.
Walter F. Tichy. RCS System for Version Control. Software Practice and Experience, 15(7):637–654, July 1985.
Walter F. Tichy. Tools for Software Configuration Management. In J.F.H. Winkler, editor, Proceedings of the International Workshop on Software Version and http://www.cs.colorado.edu/users/andre/configuration_management.html, 1999. Configuration Control, pages 1–20, Grassau, Germany, January 1988. TeubnerVerlag.
Andr-e van der Hoek. Configuration Management Yellow Pages. Available from: http://www.cs.colorado.edu/users/andre/configuration_management.html, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ruys, T.C. (1999). Xspin/Project - Integrated Validation Management for Xspin. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds) Theoretical and Practical Aspects of SPIN Model Checking. SPIN 1999. Lecture Notes in Computer Science, vol 1680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48234-2_8
Download citation
DOI: https://doi.org/10.1007/3-540-48234-2_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66499-4
Online ISBN: 978-3-540-48234-5
eBook Packages: Springer Book Archive