Rapide-0.2

Rapide-0.2 was an early version of the full Rapide-1.0 language that allowed experimentation with the design and implementation of a language for prototyping distributed, time sensitive systems.

A preliminary language definition and a toolset was developed, which are described in the following papers.

Rapide-0.2 Publications

Rapide-0.2 Language and Tool-Set Overview, February 1992, 64 page technical note.
Abstract: Rapide is an executable language for prototyping distributed, time sensitive systems. Rapide-0.2 is a preliminary language whose main purpose was to facilitate experimentation with language constructs and language implementations. This report presents a short, readable overview of Rapide-0.2.
This report also contains manuals for the Rapide-0.2 tool-set we have developed. The tools include a transformer which rewrites Rapide-0.2 source into Ada, a graphical browsers for viewing and printing partially ordered event traces generated by Rapide-0.2 computations, and an illustrated run-time system for graphically viewing Rapide-0.2 computations as they occur.
Rapide-0.2 Examples, February 1992, 91 page technical report.
Abstract: Rapide-0.2 is an executable language for prototyping distributed, time sensitive systems. We present in this report a series of simple, working example programs in the language.
In each example we present one or more new concepts or constructs of the Rapide-0.2 language with later examples drawing on previously presented material.
The examples are written for both those who wish to use the Rapide-0.2 language to do serious prototyping and for those who just wish to be familiar with it. The examples were not written for someone who wishes to learn prototyping in general.

Anna: A Language for Specifying Ada Programs

Anna is a language extension of Ada to include facilities for formally specifying the intended behavior of Ada programs. It was designed to meet a perceived need to augment Ada with precise machine-processable annotations so that well-established formal methods of specification and documentation could be applied to Ada programs. The tools are available via FTP. Start with the introduction to Anna, and if you are interested in acquiring the tools, check out the README file.

Anna Toolset Documentation

The Anna-I User's Guide and Installation Manual, 75 pages.
This manual introduces the Anna-I environment. It includes detailed instructions for installing the Anna tools, and an introduction to how the tools are used.
The Anna AST User's Guide and Reference Manual, 92 pages.
Anna defines an extension of the DIANA notation in order to represent Anna language constructs. This manual is a user guide for the DIANA-based tools of the Anna environment.

An Anna Bibliography

D. C. Luckham, S. Sankar, W. Mann, and A. Goyal. Anna - a language for specifying Ada. In Proceedings of the DARPA Software Technology Conference, pages 498-501, Los Angeles, California, April 1992. DARPA.
D. C. Luckham, S. Sankar, and S. Takahashi. Two dimensional pinpointing: An application of formal specification to debugging packages. IEEE Software, 8(1):74-84, January 1991. (Also Stanford University Technical Report No. CSL-TR-89-379.).
David C. Luckham. Programming with Specifications: An Introduction to ANNA, A Language for Specifying Ada Programs. Texts and Monographs in Computer Science. Springer-Verlag, October, 1990.
D. C. Luckham and F. W. von Henke. An overview of Anna, a specification language for Ada. IEEE Software, 2(2):9-23, March 1985.
David C. Luckham, Friedrich W. von Henke, Bernd Krieg-Brückner, and Olaf Owe. ANNA, A Language for Annotating Ada Programs, volume 260 of Lecture Notes in Computer Science. Springer-Verlag, 1987.
Walter Mann. The Anna package specification analyzer user's guide. Technical Note CSL-TN-93-390, Computer Systems Lab, Stanford University, January 1993.
N. Madhav and W. R. Mann. A methodology for formal specification and implementation of Ada packages using Anna. In Proceedings of the Computer Software and Applications Conference, 1990, pages 491-496. IEEE Computer Society Press, 1990. (Also Stanford University Computer Systems Laboratory Technical Report No. 90-438).
R. Neff. Ada/Anna Package Specification Analysis. PhD thesis, Stanford University, December 1989. Also Stanford University Computer Systems Laboratory Technical Report No. CSL-TR-89-406.
P. R. H. Place, W. G. Wood, D. C. Luckham, W. Mann, and S. Sankar. Formal development of Ada programs using Z and Anna: A case study. Technical Report CMU/SEI-91-TR-1, Software Engineering Institute, Carnegie-Mellon University, February 1991.
D. S. Rosenblum, S. Sankar, and D. C. Luckham. Concurrent runtime checking of annotated Ada programs. In Proceedings of the 6th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 10-35. Springer-Verlag - Lecture Notes in Computer Science No. 241, December 1986. (Also Stanford University Computer Systems Laboratory Technical Report No. 86-312).
S. Sankar. Automatic Runtime Consistency Checking and Debugging of Formally Specified Programs. PhD thesis, Stanford University, August 1989. Also Stanford University Department of Computer Science Technical Report No. STAN-CS-89-1282, and Computer Systems Laboratory Technical Report No. CSL-TR-89-391.
S. Sankar. A note on the detection of an Ada compiler bug while debugging an Anna program. ACM SIGPLAN Notices, 24(6):23-31, 1989.
Sriram Sankar. Run-time consistency checking of algebraic specifications. In Proceedings of the Symposium on Testing, Analysis, and Verification (TAV4), pages 123-129, Victoria, Canada, October 1991. ACM Press.
S. Sankar and M. Mandal. Concurrent runtime monitoring of formally specified programs. Technical Report 90-425, Computer Systems Laboratory, Stanford University, 1990. Also in IEEE Computer, March 1993.
S. Sankar and D. S. Rosenblum. The complete transformation methodology for sequential runtime checking of an Anna subset. Technical Report 86-301, Computer Systems Laboratory, Stanford University, June 1986. (Program Analysis and Verification Group Report 30).
F. W. von Henke, D. C. Luckham, B. Krieg-Brückner, and O. Owe. Semantic specification of Ada packages. In Ada in Use: Proceedings of the Ada International Conference, pages 185-196. Cambridge University Press, May 1985.
M. Walicki, J. U. Skakkebaek, and S. Sankar. The stanford Ada style checker: An application of the Anna tools and methodology. Technical Report 91-488, Computer Systems Laboratory, Stanford University, August 1991. (Program Analysis and Verification Group Report 55).

TSL: A Language for Specifying Concurrent Ada Programs

TSL (Task Sequencing Language) is a language for specifying sequences of tasking events occurring in the execution of distributed Ada programs. TSL-1 specifications are included in Ada programs as formal comments. They express constraints to be satisfied by the sequences of actual tasking events.

A preliminary translator and run-time monitor for TSL were developed as a feasibility study for checking the run-time behavior of distributed Ada programs. Sorry, this toolset is not publically available; papers on the construction and results of using this toolset are available below.

Many elements of TSL were incorporated into the PAVG's later work on Rapide.

TSL Toolset Documentation

The Prototype Implementation of the TSL-1 Run-Time System, October 1987, 27 page internal document.
Implementation of a Run-Time Monitor for Concurrent Programs, October 1989, 24 page internal document.

A TSL Bibliography

Douglas L. Bryan. Run-time monitoring of tasking behavior using a specification language. In Second Workshop on Large Grain Parallelism, Pittsburgh, Pennsylvania, 11-14 October 1987. Software Engineering Institute, Carnegie Mellon University. An extended abstract.
Douglas L. Bryan. An algebraic specification of the partial orders generated by concurrent Ada computations. In Proceedings of Tri-Ada '89, pages 225-241. ACM Press, October 1989.
David P. Helmbold and Douglas L. Bryan. Design of run time monitors for concurrent programs. Technical Report CSL-TR-89-395, Computer Systems Laboratory, Stanford University, October 1989.
David P. Helmbold, Douglas L. Bryan, and David C. Luckham. Principles of monitoring specifications for distributed systems. In Workshop on Parallel and Distributed Debugging, pages 313-315, Madison, Wisconsin, May 5-6, 1988. ACM SIGPLAN/SIGOPS. an extended abstract.
D. P. Helmbold. The meaning of TSL: An abstract implementation of TSL-1. Technical Report CSL-TR-88-353, Computer Systems Laboratory, Stanford University, March 1988. Also published by Computer Information Sciences Board, UC Santa Cruz as UCSC-CRL-87-29.
D. P. Helmbold and D. C. Luckham. Runtime detection and description of deadness errors in Ada tasking. Technical Report 83-249, Computer Systems Laboratory, Stanford University, November 1983. (Program Analysis and Verification Group Report 22).
D. P. Helmbold and D. C. Luckham. Debugging Ada tasking programs. IEEE Software, 2(2):47-57, March 1985. (Also Stanford University Computer Systems Laboratory Technical Report No. 84-262).
D. P. Helmbold and D. C. Luckham. TSL: Task sequencing language. In Ada in Use: Proceedings of the Ada International Conference, pages 255-274. Cambridge University Press, May 1985.
D. C. Luckham, D. P. Helmbold, S. Meldal, D. L. Bryan, and M. A. Haberler. Task sequencing language for specifying distributed Ada systems: TSL-1. In Habermann and Montanari, editors, System Development and Ada, proceedings of the CRAI workshop on Software Factories and Ada. Lecture Notes in Computer Science. Number 275, pages 249-305. Springer-Verlag, May 1986.
David C. Luckham, David P. Helmbold, Sigurd Meldal, Douglas L. Bryan, and Michael A. Haberler. Task sequencing language for specifying distributed Ada systems: TSL-1. In Proceedings of PARLE: Conference on Parallel Architectures and Languages Europe. Lecture Notes in Computer Science. Number 259, Volume II: Parallel Languages, pages 444-463, Eindhoven, The Netherlands, 15-19 June 1987. Springer-Verlag.
D.C. Luckham, S. Meldal, D.P. Helmbold, D.L. Bryan, and W. Mann. An introduction to Task Sequencing Language, TSL 1.5. Technical Report 38, Department of Informatics, University of Bergen, Bergen, Norway, August 1989. Preliminary version.
David S. Rosenblum. Specifying concurrent systems with TSL. IEEE Software, 8(3):52-61, May 1991.

7/97/25/lp