Thread View: comp.specification
3 messages
3 total messages
Started by Don Wilcox
Thu, 15 Oct 1992 21:19
Looking for small examples
Author: Don Wilcox
Date: Thu, 15 Oct 1992 21:19
Date: Thu, 15 Oct 1992 21:19
17 lines
1330 bytes
1330 bytes
Almost every paper in formal methods, software engineering, or system specification uses examples, and most of the papers describing new ideas use fairly simple examples. I am trying to collect as many of these small examples as possible. You know, things like the soda machine, stop watch, elevator, alternating bit protocol, etc. Does anyone know of a good place to find a more-or-less exhaustive list? Failing that, would you be interested in telling me about your favorite "toy" example? I am preparing to flip through several tens of thousands of pages of journal articles and conference proceedings, and I would be grateful for any additional pointers. Thanks, Don -- Don Wilcox | "For I am not ashamed of the Gospel of Washington University in St. Louis | Christ, for it is the power of salvation email: wilcox@swarm.wustl.edu | to all who believe."
Re: Looking for small examples
Author: Jeroen van de Lagemaat
Date: Fri, 16 Oct 1992 09:05
Date: Fri, 16 Oct 1992 09:05
33 lines
1628 bytes
1628 bytes
About examples: the guidelines document on the application of formal methods
of ISO describes the use of Estelle, LOTOS and SDL for 3 simple and
one large examples.
The reference: ISO TR 10167 "Information Processing Systems - Open System Inter
connection - Guidelines for the Application of Estelle, LOTOS and SDL.
Furthermore the related book of Prof. Ken Turner will be published soon.
Related to LOTOS only, a LOTOS user group is in the phase of establishment,
please contact me or Prof. Turner for enlisting.
Ken Turner
University of Stirling
Dept. of Computing Science
STIRLING FK9 4LA
UNITED KINGDOM
kjt@ cs.stir.ac.uk
Regards, Jeroen
--
___
__/ \__________ Jeroen van de Lagemaat <lagemaat@cs.utwente.nl>
| \___/ |
|___ __ ___ | University of Twente
| | | / \ (__ | Tele-Informatics & Open Systems
| |__|__\__/____) | P.O. Box 217 NL-7500 AE Enschede The Netherlands
|_________________| tel. +31 53 893684 tfx. +31 53 333815
Humour, you're making me laugh.
- Herman Finkers, Dutch comedian -
Re: Looking for small examples
Author: Jon Jacky
Date: Fri, 16 Oct 1992 16:28
Date: Fri, 16 Oct 1992 16:28
41 lines
2110 bytes
2110 bytes
In article <1992Oct15.211956.22851@wuecl.wustl.edu> wilcox@swarm.wustl.edu
(Don Wilcox) writes:
> Almost every paper in formal methods, software engineering, or system
> specification uses examples, and most of the papers describing new ideas use
> fairly simple examples. ... would you be interested in telling
> me about your favorite "toy" example?
A new one I saw recently was "Cat and Mouse": a mouse runs past a cat,
after a delay the cat begins pursuing the mouse. Can the cat capture the
mouse before the mouse escapes through a hole in the wall? This was posed
to participants in a workshop on real time systems.
This very long paper proposes a Statechart solution (and discusses several
other problems and notations also):
@inproceedings{author = "Oded Mahler and Zohar Manna and Amir Pnueli",
title = "From Timed to Hybrid Systems",
pages = "445 -- 484",
booktitle = "Real-Time: Theory in Practice,
{REX} Workshop Proceedings",
year=1991,
editor="J. W. de Bakker and C. Huizing and W. P. de Roever and
G. Rozenberg",
publisher="Springer-Verlag",
note="Lecture Notes in Computer Science 600"}
This short paper proposes a Z solution:
@inproceedings{author = "William G. Wood",
title = "A Specification of the Cat and Mouse Problem",
pages = 676 -- 686,
... other information as in preceding reference ...
}
- Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads