research-article

Free access

Rendezvous with ADA: a proof theoretical view

Authors:

Amir Pnueli,

Willem P. DeRoeverAuthors Info & Claims

AdaTEC '82: Proceedings of the AdaTEC Conference on Ada

Pages 129 - 137

https://doi.org/10.1145/3304133.3304152

Published: 06 October 1982 Publication History

PDF eReader

Abstract

A fragment of ADA abstracting the communication and synchronization part is studied. An operational semantics for this fragment is given, emphasizing the justice and fairness aspects of the selection mechanisms. An appropriate notion of fairness is shown to be equivalent to the explicit entry-queues proposed in the reference manual. Proof rules for invariance and liveness properties are given and illustrated on an example. The proof rules are based on temporal logic.

References

[1]

{A} Reference Manual for the ADA Programming Language. United States Department of Defense, July 1981.

Google Scholar

[2]

{AFR} Apt, K.R., Francez, N., de Roever, W.P. - A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems 3 (July 1980) pp. 359--385.

Digital Library

Google Scholar

[3]

{BH} Brinch Hansen, P. - Distributed Processes: A Concurrent Programming Concept - CACM 21, 11 (November 1978) pp. 934--941.

Digital Library

Google Scholar

[4]

{G} Gerth, R. - A Sound and Complete Hoare Axiomization of the ADA Rendezvous. Proc. ICALP July 1982, Aarhus, Denmark.

Digital Library

Google Scholar

[5]

{H} Hoare, C.A.R. - Communicating Sequential Processes. CACM, Vol. 21, No. 8 (1978) pp. 666--677.

Digital Library

Google Scholar

[6]

{L} Lamport, L. - "Sometime" is sometimes "not never". On Temporal logic of programs. 7th Symposium on Principles of Programming Languages, Jan. 1980, pp. 174--186.

Digital Library

Google Scholar

[7]

{LPS} Lehman, D., Pnueli, A., Stavi, J. - Impartiality, Justice and Fairness: The Ethics of Concurrent Termination. Proc. of the 8th Symposium on Automata Languages and Programming, Lecture Notes in Computer Science 115, Springer Verlag (July 1981), pp. 264--277.

Digital Library

Google Scholar

[8]

{M} Milner, R. - A Calculus of Communicating Systems. Lecture Notes in Computer Science 92, Springer Verlag (1980).

Digital Library

Google Scholar

[9]

{MP1} Manna, Z., Pnueli, A. - Verification of Con current Programs: The Temporal Framework - in the Correctness. Problem in Computer Science (R.S. Boyer, J.S. Moore eds.) International Lecture Series in Computer Science Academic Press, London 1981.

Google Scholar

[10]

{MP2} Manna, Z., Pnueli, A. - Verification of Concurrent Programs: Temporal Proof Principles. Proc. of the Workshop on Logics of Programs Yorktown Heights, Springer Verlag, Notes in Computer Science (D. Kozen ed.) 1981.

Digital Library

Google Scholar

[11]

{MP3} Manna, Z. and Pnueli, A. - Verification of Concurrent Programs: The Temporal Proof System. In the Proceeding of the 4th Advanced Course on Programming, Amsterdam, June 1982.

Google Scholar

[12]

{RDKR} Roncken, M., van Diepen, N., Kramer, M., de Roever, W.P. - A Proof System for Brinch Hansen's Distributed Processes. Technical Report CS-81-5 Rijksuniversiteit Utrecht.

Google Scholar

Cited By

View all

Estivill-Castro VHexel R(2018)Deterministic High-Level Executable Models Allowing Efficient Runtime VerificationModel-Driven Engineering and Software Development10.1007/978-3-319-94764-8_6(119-144)Online publication date: 8-Jul-2018
https://doi.org/10.1007/978-3-319-94764-8_6
Alur RHenzinger T(2005)Logics and models of real time: A surveyReal-Time: Theory in Practice10.1007/BFb0031988(74-106)Online publication date: 26-Jun-2005
https://doi.org/10.1007/BFb0031988
Harel DMarelly R(2002)Playing with time: on the specification and execution of time-enriched LSCsProceedings. 10th IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunications Systems10.1109/MASCOT.2002.1167077(193-202)Online publication date: 2002
https://doi.org/10.1109/MASCOT.2002.1167077
Show More Cited By

Recommendations

Formal Verification of Ada Programs

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification ...
Intuitionistic Trilattice Logics

We take up a suggestion by Odintsov (2009, Studia Logica, 91, 407–428) and define intuitionistic variants of certain logics arising from the trilattice SIXTEEN₃ introduced in Shramko and Wansing (2005, Journal of Philosophical Logic, 34, 121–153 and ...
Temporal Logic-Based Deadlock Analysis for Ada

A temporal logic-based specification language and deadlock analyzer for Ada is described. The deadlock analyzer is intended for use within Timebench, a concurrent system-design environment with support for Ada. The specification language, COL, uses ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

AdaTEC '82: Proceedings of the AdaTEC Conference on Ada

October 1982

279 pages

ISBN:0897910877

DOI:10.1145/3304133

Conference Chair:
Gerald Fisher
TeleSoft, San Diego, California

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 October 1982

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

AdaTEC '82

AdaTEC '82: Ada

October 6 - 8, 1982

Virginia, Arlington

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
85
Total Downloads

Downloads (Last 12 months)49
Downloads (Last 6 weeks)9

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Estivill-Castro VHexel R(2018)Deterministic High-Level Executable Models Allowing Efficient Runtime VerificationModel-Driven Engineering and Software Development10.1007/978-3-319-94764-8_6(119-144)Online publication date: 8-Jul-2018
https://doi.org/10.1007/978-3-319-94764-8_6
Alur RHenzinger T(2005)Logics and models of real time: A surveyReal-Time: Theory in Practice10.1007/BFb0031988(74-106)Online publication date: 26-Jun-2005
https://doi.org/10.1007/BFb0031988
Harel DMarelly R(2002)Playing with time: on the specification and execution of time-enriched LSCsProceedings. 10th IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunications Systems10.1109/MASCOT.2002.1167077(193-202)Online publication date: 2002
https://doi.org/10.1109/MASCOT.2002.1167077
Karam GBuhr R(1991)Temporal Logic-Based Deadlock Analysis for AdaIEEE Transactions on Software Engineering10.1109/32.9919717:10(1109-1125)Online publication date: 1-Oct-1991
https://dl.acm.org/doi/10.1109/32.99197
Harel ELichtenstein OPnueli A(1990)Explicit clock temporal logic[1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science10.1109/LICS.1990.113765(402-413)Online publication date: 1990
https://doi.org/10.1109/LICS.1990.113765
Hankley WPeters J(1990)Temporal specification of Ada tasksTwenty-Third Annual Hawaii International Conference on System Sciences10.1109/HICSS.1990.205212(410-419)Online publication date: 1990
https://doi.org/10.1109/HICSS.1990.205212
Karam GBuhr R(1990)Starvation and Critical Race Analyzers for AdaIEEE Transactions on Software Engineering10.1109/32.5762216:8(829-843)Online publication date: 1-Aug-1990
https://dl.acm.org/doi/10.1109/32.57622
Buhr RKaram GHayes CWoodside C(1989)Software CADIEEE Transactions on Software Engineering10.1109/32.2175215:3(235-249)Online publication date: 1-Mar-1989
https://dl.acm.org/doi/10.1109/32.21752
Apt KFrancez NKatz S(1988)Appraising fairness in languages for distributed programmingDistributed Computing10.1007/BF018728482:4(226-241)Online publication date: 1-Dec-1988
https://dl.acm.org/doi/10.1007/BF01872848
de Roever W(1985)The Cooperation Test : a syntax-directed verification methodLogics and Models of Concurrent Systems10.1007/978-3-642-82453-1_8(213-257)Online publication date: 1985
https://doi.org/10.1007/978-3-642-82453-1_8
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Recommendations

Formal Verification of Ada Programs

Intuitionistic Trilattice Logics

Temporal Logic-Based Deadlock Analysis for Ada

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations