Executing formal specifications

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Executing formal specifications: the ASTRAL to TRIO translation approach

Full text

Pdf (1.05 MB)

Source

International Symposium on Software Testing and Analysis archive
Proceedings of the symposium on Testing, analysis, and verification table of contents

Victoria, British Columbia, Canada

Pages: 112 - 122

Year of Publication: 1991

ISBN:0-89791-449-X

Authors

Carlo Ghezzi	Dipartimento di Elettronica, Politecnico di Milano, Milano, Italia
Richard A. Kennerer	Reliable Software Group, Department of Computer Science, University of California, Santa Barbara, CA

Sponsor

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 10, Citation Count: 6

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/120807.120817 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	AK 85	Auernheimer, B. and R. A. Kemmerer, ASLAN User's Manual, Report No. TRCS84-10, Department of Computer Science, University of California, Santa Barbara, March 1985.
	AK 86	B Auernheimer , R A Kemmerer, RT-ASLAN: A specification language for real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.879-889, Sept. 1986
	BCG 87	Berry, G., Couronne', P., and Gonthier, G. Synchronous Programming of Reactive Systems, an Introduction to ESTEREL, INRIA Report No. 647, 1987.
	CHP 87	P. Caspi , D. Pilaud , N. Halbwachs , J. A. Plaice, LUSTRE: a declarative language for real-time programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.178-188, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41641]
	FP 88	Stuart R. Faulk , David L. Parnas, On synchronization in hard-real-time systems, Communications of the ACM, v.31 n.3, p.274-287, March 1988 [doi>10.1145/42392.42397]
	FM 91	Felder, M. and A. Morzenti, "Specification Testing for Real-Time Systems by Model Checking in TRIO", submitted for publication, 1991.
	GK 91	Carlo Ghezzi , Richard A. Kemmerer, ASTRAL: An Assertion Language for Specifying Realtime Systems, Proceedings of the 3rd European Software Engineering Conference, p.122-146, October 21-24, 1991
	GMM 90	C. Ghezzi , D. Mandrioli , A. Morzenti, TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, v.12 n.2, p.107-123, May 1990 [doi>10.1016/0164-1212(90)90074-V]
	GMM 91	Carlo Ghezzi , Dino Mandrioli , Sandro Morasca , Mauro Pezzè, A Unified High-Level Petri Net Formalism for Time-Critical Systems, IEEE Transactions on Software Engineering, v.17 n.2, p.160-172, February 1991 [doi>10.1109/32.67597]
	HLN 88	D. Harel , H. Lachover , A. Naamad , A. Pnueli , M. Politi , R. Sherman , a. Shtul-Trauring, Statemate: a working environment for the development of complex reactive systems, Proceedings of the 10th international conference on Software engineering, p.396-406, April 11-15, 1988, Singapore
	JL 89	M. S. Jaffe , N. G. Leveson, Completeness, robustness, and safety in real-time software requirements specification, Proceedings of the 11th international conference on Software engineering, p.302-311, May 1989, Pittsburgh, Pennsylvania, United States [doi>10.1145/74587.74628]
	JM 86	F Jahanian , A K Mok, Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.890-904, Sept. 1986
	Kem 85	Kemmerer, R.A., "Testing Software Specifications to Detect Design Errors, IEEE Transactions on Software Engineering, Vol. SE-11, No. 1, January 1985.
	Koy 89	Koymans, R., Specifying Message Passing and Time-Cntical Systems with Temporal Logic, PhD Thesis, Eindhoven University of Technology, 1989.
	KR 85	Koymans, R. and W.P. de Roever, "Examples of a Realtime Temporal Logic Specification, Lecture Notes in Computer Science, No. 207, Springer Verlag, Berlin, 1985.
	MGG 90	Morzenti, A., D. Mandrioli, and C. Ghezzi, A Model Parametric Real-Time Logic, Politecnico di Milano, Dipartimento di Elettronica, Report No. 90.010,1990.
	Smu 68	Smullian, R.M., First Order Logic, Springer Verlag, Berlin, 1968.
	Sta 88	John A. Stankovic, Misconceptions About Real-Time Computing: A Serious Problem for Next-Generation Systems, Computer, v.21 n.10, p.10-19, October 1988 [doi>10.1109/2.7053]
	Suz 90	Ichiro Suzuki, Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets, IEEE Transactions on Software Engineering, v.16 n.11, p.1273-1281, November 1990 [doi>10.1109/32.60315]
	WN 89	Jeannette M. Wing , Mark R. Nixon, Extending Ina Jo with Temporal Logic, IEEE Transactions on Software Engineering, v.15 n.2, p.181-197, February 1989 [doi>10.1109/32.21744]
	Zav 87	Zave, Pamela, PAISLey User Documentation Volume 3: Case Studies, Computer Technology Research Laboratory Report, AT&T Bell Laboratories, Murray Hill, New Jersey, 1987.

CITED BY 6

	Alberto Coen-Porisini , Richard A. Kemmerer, The composability of ASTRAL realtime specifications, ACM SIGSOFT Software Engineering Notes, v.18 n.3, p.128-138, July 1993
	Debra J. Richardson , Stephanie Leif Aha , T. Owen O'Malley, Specification-based test oracles for reactive systems, Proceedings of the 14th international conference on Software engineering, p.105-118, May 11-15, 1992, Melbourne, Australia
	A. Coen-Porisini , R. A. Kemmerer , D. Mandrioli, A Formal Framework for ASTRAL Intralevel Proof Obligations, IEEE Transactions on Software Engineering, v.20 n.8, p.548-561, August 1994
	Paul Z. Kolano, Proof assistance for real-time systems using an interactive theorem prover, Theoretical Computer Science, v.282 n.1, p.53-99, June 7, 2002
	Alberto Coen-Porisini , Carlo Ghezzi , Richard A. Kemmerer, Specification of realtime systems using ASTRAL, IEEE Transactions on Software Engineering, v.23 n.9, p.572-598, September 1997
	Amy W. Apon , Larry W. Dowdy, Specification of Realtime Systems Using ASTRAL, IEEE Transactions on Software Engineering, v.23 n.9, p.572-598, September 1997