More Web Proxy on the site http://driver.im/

research-article

Extending Ina Jo with Temporal Logic

Authors:

Jeannette M. Wing,

Mark R. NixonAuthors Info & Claims

IEEE Transactions on Software Engineering, Volume 15, Issue 2

Pages 181 - 197

https://doi.org/10.1109/32.21744

Published: 01 February 1989 Publication History

Abstract

The authors give both informal and formal descriptions of both the current Ina Jo specification language and Ina Jo enhanced with temporal logic. They include details of a simple example to demonstrate the use of the proof system and details of an extended example to demonstrate the expressiveness of the enhanced language. The authors discuss their language design goals, decisions, and their implications.

References

[1]

{1} J. R. Abrial, "The specification language Z: Syntax and semantics," Programming Res. Group, Oxford Univ., 1980.

[2]

{2} H. Barringer, R. Kuiper, and A. Pnueli, "Now you may compose temporal logic specifications," in Proc. 16th Annu. ACM Symp. Theory of Computing, ACM SIGACT, Washington, DC, 1984, pp. 51- 63.

Digital Library

[3]

{3} M. Ben-Ari and A. Pnueli, "The logic of nexttime," Tel Aviv Univ., Tel Aviv, Israel, Tech. Rep. 80-13, July 1980.

[4]

{4} M. Bidoit and C. Choppy, "ASSPEGIQUE: An integrated environment for algebraic specifications," in Proc. Int. Joint Conf. Theory and Practice of Software Development, Volume 2: Formal Methods and Software Development (Lecture Notes in Computer Science, No. 186). New York: Springer-Verlag, 1985, pp. 246-260.

[5]

{5} D. Bjorner and C. B. Jones, Formal Specification and Software Development . Englewood Cliffs, NJ: Prentice-Hall, 1982.

[6]

{6} D. Britton, "Formal verification of a secure network with end-to-end encryption," in Proc. IEEE Conf. Security and Privacy, 1984, pp. 154-166.

[7]

{7} M. Browne, E. Clarke, D. Dill, and B. Mishra, "Automatic verification of sequential circuits using temporal logic," IEEE Trans. Comput., vol. C-35, no. 12, pp. 1035-1044, Dec. 1986.

Digital Library

[8]

{8} M. Broy, "Specification and top down design of distributed systems," Univ. Passau, Rep. MIP-8401, Dec. 1984.

[9]

{9} R. M. Burstall and J. A. Goguen, "An informal introduction to specifications using CLEAR," in The Correctness Problem in Computer Science, Boyer and Moore, Eds. New York: Academic, 1981.

[10]

{10} F. Cristian, "A rigorous approach to fault-tolerant system development," IBM Res. Rep. RJ 4008 (45056), 1983.

[11]

{11} E. W. Dijkstra, A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.

Digital Library

[12]

{12} I. Durham and M. Shaw, "Specifying reliability as a software attribute," Carnegie-Mellon Univ., Tech. Rep. CS-82-148, Dec. 1982.

[13]

{13} H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification I. New York: Springer-Verlag, 1985.

Digital Library

[14]

{14} E. A. Emerson and J. Y. Halpen, "'Sometimes' and 'not never' revisted: On branching versus linear time," in Proc. Principles of Programming Languages, Austin, TX, 1983, pp. 127-140.

Digital Library

[15]

{15} P. Folkjar and D. Bjorner, "A formal model of a generalized CSP-like language," in Proc. IFIP 1980, Tokyo. Amsterdam, The Netherlands: North-Holland, pp. 95-99.

[16]

{16} J. A. Goguen and J. Tardo, "An introduction to OBJ: A language for writing and testing formal algebraic program specifications," in Proc. Conf. Specifications of Reliable Software, Boston, MA, 1979.

[17]

{17} D. I. Good, "Revised report on Gypsy 2.1--DRAFT-," Inst. Comput. Sci., Univ. Texas, Austin, July 1984.

[18]

{18} D. I. Good, R. M. Cohen, and J. Keeton-Williams, "Principles of proving concurrent programs in Gypsy," in Proc. 6th Symp. Principles of Programming Languages, ACM, Jan. 1979.

Digital Library

[19]

{19} J. V. Guttag, J. J. Horning, and J. M. Wing, "The Larch family of specification languages," IEEE Software, vol. 2, no. 5, pp. 24-36, Sept. 1985.

Digital Library

[20]

{20} B. T. Hailpern, Verifying Concurrent Processes Using Temporal Logic (Lecture Notes in Computer Science 129). New York: Springer-Verlag, 1982.

Digital Library

[21]

{21} M. P. Herlihy and J. M. Wing, "Specifying graceful degradation in distributed systems," in Proc. Principles of Distributed Computing, Vancouver, B.C., Canada, 1987.

Digital Library

[22]

{22} C. A. R. Hoare, "An axiomatic basis for computer programming," Commun. ACM, vol. 12, no. 10, pp. 576-583, Oct. 1969.

Digital Library

[23]

{23} C. A. R. Hoare, Communicating Sequential Processor. Englewood Cliffs, NJ: Prentice-Hall International, 1985.

Digital Library

[24]

{24} S. A. Kripke, "Semantical considerations on modal logics," Acta Philosophica Fennica, Modal and Many-valued Logics, pp. 83-94, 1963.

[25]

{25} L. Lamport, "Specifying concurrent program modules," ACM Trans. Program Lang. Syst., vol. 5, no. 2, pp. 190-222, Apr. 1983.

Digital Library

[26]

{26} Z. Manna and A. Pnueli, "The modal logic of programs," in Automata, Languages and Programming (Lecture Notes in Computer Science 79). New York: Springer-Verlag, 1979, pp. 385-409.

Digital Library

[27]

{27} Z. Manna and A. Pnueli, "Verification of concurrent programs, Part I: The temporal framework," Dep. Comput. Sci., Stanford Univ., Tech. Rep. STANCS-81-836, June 1981.

Digital Library

[28]

{28} Z. Manna and A. Pnueli, "Proving precedence properties: The temporal way," in Proc. Automata, Languages, and Programming (Lecture Notes in Computer Science 154). New York: Springer-Verlag. 1983, pp. 491- 512.

Digital Library

[29]

{29} P. M. Melliar-Smith and R. L. Schwartz, "Formal specification and mechanical verification of SIFT: A fault-tolerant flight control system," IEEE Trans. Comput., vol. C-31, no. 7, pp. 616-630, July 1982.

[30]

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

Digital Library

[31]

{31} B. Mokowski, "A temporal logic for multi-level reasoning about hardware," Dep. Comput. Sci., Stanford Univ., Rep. STAN-CS-82- 952, Dec. 1982.

[32]

{32} D. R. Musser, "Abstract data type specification in the affirm system," IEEE Trans. Software Eng., vol. SE-6, no. 1, pp. 24-32, Jan. 1980.

Digital Library

[33]

{33} R. Nakajima and T. Yuasa, The IOTA Programming System (Lecture Notes in Computer Science, Vol. 160). New York: Springer-Verlag, 1983.

Digital Library

[34]

{34} S. Owicki and D. Gries, "Verifying properties of parallel programs: An axiomatic approach," Commun. ACM, vol. 19, no. 5, pp. 279- 285, May 1976.

Digital Library

[35]

{35} S. Owicki and L. Lamport, "Proving liveness properties of concurrent programs," ACM Trans. Program. Lang. Syst., vol. 4. no. 3, pp. 455-495, July 1982.

Digital Library

[36]

{36} L. Robinson and O. Roubine, "SPECIAL: A specification and assertion language," SRI Tech. Rep. CSL-46, Melno Park, CA, Jan. 1977.

[37]

{37} J. Scheid and S. Anderson, "The Ina Jo specification language reference manual," System Development Corp., Santa Monica, CA, Tech. Rep. TM-(L)-6021/001/01, Mar. 1985.

[38]

{38} J. M. Wing and M. Nixon, "Adding temporal logic to Ina Jo," Dep. Comput. Sci., Carnegie-Mellon Univ., Pittsburgh, PA, Tech. Rep. CMU-CS-85-146.

[39]

{39} P. Zave, "An operational approach to requirements specification for embedded systems," IEEE Trans. Software Eng., vol. SE-8, no. 3, pp. 250-269, May 1982.

Digital Library

Cited By

Sowmya ARamesh S(1998)Extending Statecharts with Temporal LogicIEEE Transactions on Software Engineering10.1109/32.66788024:3(216-231)Online publication date: 1-Mar-1998
https://dl.acm.org/doi/10.1109/32.667880
Amoroso E(1995)Creating formal specifications from requirements documentsACM SIGSOFT Software Engineering Notes10.1145/225907.22591520:1(67-70)Online publication date: 1-Jan-1995
https://dl.acm.org/doi/10.1145/225907.225915
Ghezzi CKennerer RHowden W(1991)Executing formal specificationsProceedings of the symposium on Testing, analysis, and verification10.1145/120807.120817(112-122)Online publication date: 1-Oct-1991
https://dl.acm.org/doi/10.1145/120807.120817

Index Terms

Recommendations

A Proof System for a Unified Temporal Logic
Computing and Combinatorics
Abstract
Theorem proving is a widely used approach to the verification of computer systems, and its theoretical basis is generally a proof system for formal derivation of logic formulas. In this paper, we propose a proof system for Propositional Projection ...
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 ...
Specification of Synchronizing Processes

The formalism of temporal logic has been suggested to be an appropriate tool for expressing the semantics of concurrent programs. This paper is concerned with the application of temporal logic to the specification of factors affecting the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image IEEE Transactions on Software Engineering

IEEE Transactions on Software Engineering Volume 15, Issue 2

February 1989

130 pages

ISSN:0098-5589

Editor:
Victor R. Basili
Univ. Maryland, College Park

Issue’s Table of Contents

Copyright © Copyright © 1989 IEEE. All Rights Reserved.

Publisher

IEEE Press

Publication History

Published: 01 February 1989

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sowmya ARamesh S(1998)Extending Statecharts with Temporal LogicIEEE Transactions on Software Engineering10.1109/32.66788024:3(216-231)Online publication date: 1-Mar-1998
https://dl.acm.org/doi/10.1109/32.667880
Amoroso E(1995)Creating formal specifications from requirements documentsACM SIGSOFT Software Engineering Notes10.1145/225907.22591520:1(67-70)Online publication date: 1-Jan-1995
https://dl.acm.org/doi/10.1145/225907.225915
Ghezzi CKennerer RHowden W(1991)Executing formal specificationsProceedings of the symposium on Testing, analysis, and verification10.1145/120807.120817(112-122)Online publication date: 1-Oct-1991
https://dl.acm.org/doi/10.1145/120807.120817

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents