Temporal proof methodologies for real-time systems

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Temporal proof methodologies for real-time systems

Full text

Pdf (1.33 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

Orlando, Florida, United States

Pages: 353 - 366

Year of Publication: 1991

ISBN:0-89791-419-8

Authors

Tom Henzinger	Department of Computer Science, Stanford University, Stanford, CA
Zohar Manna	Department of Computer Science, Stanford University, Stanford, CA and Department of Applied Mathematics, The Weizmann Institute of Science, Rehovot, Israel 76100
Amir Pnueli	Department of Applied Mathematics, The Weizmann Institute of Science, Rehovot, Israel 76100

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 27, Citation Count: 14

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/99583.99629 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.

	AH90	R. Alur, T.A. Henzinger, "Real-time logics: complexity and expressiveness," 5th IEEE LICS, 1990.
	EMSS89	E.A. Emerson, A.K. Mok, A.P. Sistla, J. Srinivasan, "Quantitative temporal reasoning," Automatic Verification of Finite-state Systems (J. Sifakis, ed.), Springer LNCS 407, 1989.
	Ha88	E. Hard, Temporal Analysis o} Real-time Systems, M.S. Thesis, Weizmunn Institute, 1988.
	HMP90	Tom Henzinger , Z. Manna , A. Pnueli, An interleaving model for real time, Proceedings of the fifth Jerusalem conference on Information technology, p.717-730, September 1990, Jerusalem, Israel
	HMP91	Thomas A. Henzinger , Z Manna , Amir Pnueli, Temporal proof methodologies for real-time systems, Stanford University, Stanford, CA, 1991
	Ko89	R. Koymans, Specifying Message Passing and Time-critical Systems with Temporal Logic, Ph.D. Thesis, Eindhoven Univ. of Tech., 1989.
	KVdR83	Ron Koymans , Jan Vytopil , Willem P. de Roever, Real-time programming and asynchronous message passing, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.187-197, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806721]
	MP89a	Zohar Manna , Amir Pnueli, The anchored version of the temporal framework, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, p.201-284, May 30-June 03, 1988
	MP89b	Zohar Manna , Amir Pnueli, Completing the temporal picture, Selected papers of the 16th international colloquium on Automata, languages, and programming, p.97-130, June 1991, Stresa, Italy
	OL82	Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
	Os90	Jonathan S. Ostroff, Temporal logic for real time systems, John Wiley & Sons, Inc., New York, NY, 1989
	PdR82	A. Pn~~ll, W.-P. de Roe~e~, "Re~de~-v~ wlth Ada ~ a proof-theoretical view," SigPlan AdaTEC, 1982.
	PH88	Amir Pnueli , Eyal Harel, Applications of temporal logic to the specification of real time systems (extended abstract), Proceedings of a Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.84-98, September 1988, Warwick, United Kingdom
	Ro84	D. Ron, Temporal Verification of Communication Protocols, M.S. Thesis, Weizmann Institute, 1984.

CITED BY 14

	Robyn R. Lutz, Targeting safety-related errors during software requirements analysis, ACM SIGSOFT Software Engineering Notes, v.18 n.5, p.99-106, Dec. 1993
	Zhiming Liu , Mathai Joseph, Specification and verification of fault-tolerance, timing, and scheduling, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.46-89, Jan. 1999
	Miguel Felder , Carlo Ghezzi , Mauro Pezzè, Analyzing refinements of state based specifications: the case of TB nets, ACM SIGSOFT Software Engineering Notes, v.18 n.3, p.28-39, July 1993
	Robyn R. Lutz , Johnny S. K. Wong, Detecting Unsafe Error Recovery Schedules, IEEE Transactions on Software Engineering, v.18 n.8, p.749-760, August 1992
	E. Jane Cameron , Yow-Jian Lin, A real-time transition model for analyzing behavioral compatibility of telecommunications services, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.101-111, Dec. 1991
	M. Felder , D. Mandrioli , A. Morzenti, Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models, IEEE Transactions on Software Engineering, v.20 n.2, p.127-141, February 1994
	Brendan P. Mahony , Ian J. Hayes, A Case-Study in Timed Refinement: A Mine Pump, IEEE Transactions on Software Engineering, v.18 n.9, p.817-826, September 1992
	Richard Gerber , Insup Lee, Guest A Layered Approach to Automating the Verification of Real-Time Systems, IEEE Transactions on Software Engineering, v.18 n.9, p.768-784, September 1992
	Arcot Sowmya , S. Ramesh, Extending Statecharts with Temporal Logic, IEEE Transactions on Software Engineering, v.24 n.3, p.216-231, March 1998
	Riccardo Mattolini , Paolo Nesi, An Interval Logic for Real-Time System Specification, IEEE Transactions on Software Engineering, v.27 n.3, p.208-227, March 2001
	Jia Xu, On Inspection and Verification of Software with Timing Requirements, IEEE Transactions on Software Engineering, v.29 n.8, p.705-720, August 2003
	Mohamed F. Younis , Thomas J. Marlowe , Alexander D. Stoyen , Grace Tsai, Statically Safe Speculative Execution for Real-Time Systems, IEEE Transactions on Software Engineering, v.25 n.5, p.701-721, September 1999
	Nancy A. Lynch , Hagit Attiya, Using mappings to prove timing properties, Distributed Computing, v.6 n.2, p.121-139, September 1992
	Paul Regnier , George Lima , Aline Andrade, A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol, Electronic Notes in Theoretical Computer Science (ENTCS), 240, p.221-238, July, 2009