Article

Free access

Functional specification of synchronized processes based on modal logic

Authors:

Naoki Yonezaki,

Takao KatayamaAuthors Info & Claims

ICSE '82: Proceedings of the 6th international conference on Software engineering

Pages 208 - 217

Published: 13 September 1982 Publication History

Abstract

We present in this paper a pseudo functional language and a specification language both of which are designed to describe systems of synchronized processes with shared resources. The semantics of the pseudo functional language is defined by translating its statements to the set of formulas of intensional logic. The specification language contains formulas of the logic, hence its semantics can be treated by the model theory as usual. A proof method for the program written in the language is proposed. Time dependent aspects of processes are described in terms of intensional logic. Specification of parallel systems can be described in a well structured manner in our specification language, more precisely, they are described hierarchically according to the function decomposition of the system, and at each level of the hierarchy the configuration of processes and resources and time dependent properties are separately described. Resources are defined as an abstract data type with synchronization specification. We give an example of specification and a proof of a program written in the parallel pseudo functional programming language.

References

[1]

A.C. Shaw: Software Specification Languages Based on Regular Expressions, Technical Report, ETH Zurich, June 1979.

[2]

A.N. Habermann: Path Expressions. Carnegie-Mellon University Report, 1975.

[3]

R.L.Schwartz and P.M. Melliar-Smith: Temporal Logic Specification of Distributed Systems, The Proceedings of the Second International Conference on Distributed Systems, April 8-10, 1981, Paris, France

[4]

K.Ranamritham, R.M. Keller: On Synchronization and its Specification: CONPAR 81 (1981)

Digital Library

[5]

D.Harel: First Order Dynamic Logic, Lecture Notes in Computer Science 68, Springer-Verlag, Berlin, 1979

Digital Library

[6]

S. Owicki: Axiomatic Proof Techniques for Parallel Programs, Ph. D. Th., Cornell University, August 1975.

Digital Library

[7]

A.Pnueli, The Temporal Logic of Programs. 19th Annual Symposium on Foundations of Computer Science. Nov, 1977

[8]

Z.Manna, A. Pnueli: The Modal Logic of Programs: pp386-408

Digital Library

[9]

A.Pnueli: The Temporal Semantics of Concurrent Programs. In Khan, Ed., Semantics of Concurrent Computation, Springer Lecture Notes in Computer Science, Springer-Verlog, (1979), pp.1-20

Digital Library

[10]

D.Gabbay, A.Pnueli, S.Sheloh, J.Stave: The Temporal Analysis of Fairness: Seventh ACM Symposium on Principles of Programming Languages. Las Vegas, NV, January 1980.

Digital Library

[11]

Z.Manna: Logics of Programs: Information Processing 80, S.H. Lavington(ed.) North-Holland Publishing Company 1980. pp41-51

[12]

B.Hailpern and S. Owicki: Verifying Network Protocols Using Temporal Logic In Tends and Applications 1980: Computer Network Protocols. IEEE computer Society, May 1980 pp18-28

[13]

B.Hailpern: Verifying Concurrent Processes Using Temporal Logic. Technical Report 195. Computer Systems Laboratory, Stanford University. August 1980.

[14]

R.M. Keller: Formal Verification of Parallel Programs, CACM 19 (7) 1976.

Digital Library

[15]

L. Lamport: Proving the Correctness of Multiprocess Programs, IEEE Transaction on Software Engineering 3(2) 1977, pp.125-143.

[16]

L. Lamport: 'Sometime' is Sometimes 'Not Never' On the Temporal Logic of Programs, Seventh ACM Symposium on Principles of Programming Languages. Les Vegas, NV. January 1980, PP174-185.

Digital Library

[17]

K.Ramamritham and R.M. Keller: Specifying and Proving Properties of Sentinel Processes The proceedings of 5th International Conference on Software Engineering (March 1981) pp374-382

Digital Library

[18]

R.Montague: The Proper Treatment of Quantification in Ordinary English, Approaches to Natural Language, Reidel Dordrecht.

[19]

N.Yonezaki, H.Enomoto: Database System based on Intensional Logic, The Proceedings of the 8th International Conference on Computational Linguistics, Sept. 1980

Digital Library

[20]

T.M.V. Janssen: The Expressive Power of Intensional Logic in the Semantics of Programming Language, Lecture Notes in Computer Science 53, Springer-Verlag, Berlin, 1977

[21]

J.V. Guttag: The Specification and Application to Programming of Abstract Data Types, Ph.D. thesis, Computer Science, University of Toronto, Sept. 1975.

Digital Library

Cited By

Dierl SFiterau-Brostean PHowar FJonsson BSagonas KTåquist F(2024)Scalable Tree-based Register Automata LearningTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_5(87-108)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57249-4_5
Abdulla PAtig MGanjei ZRezine AZhu YKaivola RWahl T(2015)Verification of cache coherence protocols wrt. trace filtersProceedings of the 15th Conference on Formal Methods in Computer-Aided Design10.5555/2893529.2893538(9-16)Online publication date: 27-Sep-2015
https://dl.acm.org/doi/10.5555/2893529.2893538

Index Terms

Functional specification of synchronized processes based on modal logic
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Strengthening Brady's Paraconsistent 4-Valued Logic BN4 with Truth-Functional Modal Operators

ukasiewicz presented two different analyses of modal notions by means of many-valued logics: (1) the linearly ordered systems 3,..., [InlineEquation not available: see fulltext.] ,..., $$\hbox {L}_{\omega }$$L ; (2) the 4-valued logic he defined in the ...
On Modal Grzegorczyk Logic
Topics in Logic, Philosophy and Foundations of Mathematics and Computer Science. In Recognition of Professor Andrzej Grzegorczyk

In 1964-68 Andrzej Grzegorczyk investigated relational and topological semantics for the intuitionistic logic [15]-[18] . In this connection, following to McKinsey and Tarski, he also considered a semantics for modal logics. It is well known that there ...
On Modal Grzegorczyk Logic
Topics in Logic, Philosophy and Foundations of Mathematics and Computer Science. In Recognition of Professor Andrzej Grzegorczyk

In 1964-68 Andrzej Grzegorczyk investigated relational and topological semantics for the intuitionistic logic [15]-[18] . In this connection, following to McKinsey and Tarski, he also considered a semantics for modal logics. It is well known that there ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '82: Proceedings of the 6th international conference on Software engineering

September 1982

439 pages

Sponsors

NBS: National Bureau of Standards
IPSJ: Information Processing Society of Japan
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS: Computer Society

Publisher

IEEE Computer Society Press

Washington, DC, United States

Publication History

Published: 13 September 1982

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
257
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)2

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dierl SFiterau-Brostean PHowar FJonsson BSagonas KTåquist F(2024)Scalable Tree-based Register Automata LearningTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_5(87-108)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57249-4_5
Abdulla PAtig MGanjei ZRezine AZhu YKaivola RWahl T(2015)Verification of cache coherence protocols wrt. trace filtersProceedings of the 15th Conference on Formal Methods in Computer-Aided Design10.5555/2893529.2893538(9-16)Online publication date: 27-Sep-2015
https://dl.acm.org/doi/10.5555/2893529.2893538

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents