Abstract
This paper discusses our experience with literate programming tools in the realm of the modelling and validation of systems. We propose the use of literate programming techniques to structure and control the validation trajectory. The use of literate programming is illustrated by means of a running example using Promela and Spin. The paper can also be read as a tutorial on the application of literate programming to formal methods.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Don Bolinger and Tan Bronson. Applying RCS and SCCS. O'Reilly & Associates, Inc., Sebastopol, 1995.
Pedro R. D'Argenio, Joost-Pieter Katoen, Theo C. Ruys, and G. Jan Tretmans. The Bounded Retransmission Protocol must be on time! (Full Version). CTIT Technical Report Series 97-03, Centre for Telematics and Information Technology, University of Twente, Enschede, The Netherlands, 1997. Also available from URL: http://wwwtios.cs.utwente.nl/~dargenio/brp/.
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 (TAGAS'97), number 1217 in Lecture Notes in Computer Science (LNCS), pages 416–431, University of Twente, Enschede, The Netherlands, April 1997. Springer Verlag, Berlin.
Christopher W. Fraser and David R. Hanson. A Retargetable G Compiler: Design and Implementation. Addison-Wesley, 1995.
Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, New Jersey, 1991.
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/indez.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/vhatispin.html.
Johan Jeuring and Erik Meijer, editors. Advanced Functional Programming — Tutorial Text of the First International Spring School on Advanced Functional Programming Techniques, number 925 in Lecture Notes in Computer Science (LNCS), Bastad, Sweden, May 1995. Springer Verlag, Berlin.
Andrew L. Johnson and Brad C. Johnson. Literate Programming using noveb. Linux Journal, pages 64–69, October 1997.
Pirn Kars. The Application of Promela and Spin in the Bos Project. In Jean-Charles Grégoire, Gerard J. Holzmann, and Doron A. Peled, editors, Proceedings of SPIN96, the Second International Workshop on SPIN (published as “The Spin Verification System), volume 32 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Rutgers University, New Jersey, August 1996. American Mathematical Society. Also available from URL: http://netlib.bell-labs.com/netlib/spin/ws96/Ka.ps.Z.
Donald E. Knuth. Literate Programming. The Computer Journal, 27(2):97–111, May 1984.
Donald E. Knuth. Literate Programming. Number 27 in CSLI Lecture Notes. Center for the Study of Language and Information (CSLI), Stanford University, California, 1992.
Kim G. Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a Nutshell. Springer International Journal of Software Tools for Technology Transfer (STTT), 1(1/2), October 1997.
Josh MacDonald. PRCS — Project Revision Control System. Available from URL: http://vw.xcf.berkeley.edu/~jmacd/prcs.html.
Roger S. Pressman. Software Engineering — A Practioner's Approach. McGraw-Hill, New York, third edition, 1992.
Norman Ramsey, noveb — homepage. Available from URL: http://www.cs.virginia.edu/~nr/noweb/.
Norman Ramsey. Literate Programming Simplified. IEEE Software, 11(5):97–105, September 1994.
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-labs.com/netlib/spin/ws97/ruys.ps.Z.
J.M. Spivey. The Z Notation — A Reference Manual Prentice Hall, New York, second edition, 1992.
Walter F. Tichy. RCS — A System for Version Control. Software, Practice & Experience, 15(7):637–654, July 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ruys, T.C., Brinksma, E. (1998). Experience with literate programming in the modelling and validation of systems. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054185
Download citation
DOI: https://doi.org/10.1007/BFb0054185
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive