research-article

Open access

Reasoning about dynamically evolving process structures

Authors:

Pierre America,

Frank de BoerAuthors Info & Claims

Formal Aspects of Computing, Volume 6, Issue 3

Pages 269 - 316

https://doi.org/10.1007/BF01215408

Published: 01 May 1994 Publication History

PDF eReader

Abstract

We develop a Hoare-style proof system for reasoning about the behaviour of processes that interact via a dynamically evolving communication structure.

References

[1]

America P. H. M Issues in the Design of a Parallel Object-Oriented Language Formal Aspects of Computing 1989 1 366-411

Digital Library

Google Scholar

[2]

America, P. H. M., de Bakker, J. W., Kok, J. N. and Rutten, J. J. M. M.: Operational Semantics of a Parallel Object-Oriented Language.Conference Record of the 13th Symposium on Principles of Programming Languages, St. Petersburg, Florida, pp. 194–208, 1986.

Google Scholar

[3]

Apt K. R., Francez N., and de Roever W. P. A Proof System for Communicating Sequential Processes ACM Transactions on Programming Languages and Systems 1980 2 359-385

Digital Library

Google Scholar

[4]

Apt K. R. Ten Years of Hoare logic: A Survey—Part I ACM Transactions on Programming Languages and Systems 1981 3 431-483

Digital Library

Google Scholar

[5]

Apt K. R. Formal Justification of a Proof System for Communicating Sequential Processes Journal of the ACM 1983 30 197-216

Digital Library

Google Scholar

[6]

de Bakker, J. W.:Mathematical Theory of Program Correctness. Prentice-Hall International, 1980.

Google Scholar

[7]

Goldberg, A. and Robson, D.:Smalltalk-80, The Language and its Implementation. Addison-Wesley, 1984.

Google Scholar

[8]

Hoare C. A. R. An Axiomatic Basis for Computer Programming Communications of the ACM 1969 12 567-580

Digital Library

Google Scholar

[9]

Hoare C. A. R. Communicating Sequential Processes Communications of the ACM 1978 21 666-677

Digital Library

Google Scholar

[10]

Hooman, J. and de Roever, W. P.: The Quest Goes On: Towards Compositional Proof Systems for CSP. In J.W. de Bakker, W.P. de Roever, G. Rozenberg (eds.):Current Trends in Concurrency, Springer LNCS 224, pp. 343–395, 1986.

Google Scholar

[11]

Meldal S. Axiomatic Semantics of Access Type Tasks in Ada Report No. 100 1986 Norway Institute of Informatics, University of Oslo

Google Scholar

[12]

Meyer, B.:Object-Oriented Software Construction. Prentice-Hall, 1988.

Google Scholar

[13]

Tucker, J. V. and Zucker, J. I.:Program Correctness over Abstract Data Types, with Error-State Semantics. CWI Monographs 6, North-Holland, 1988.

Google Scholar

[14]

Zwiers J., de Roever W. P., and van Emde Boas P. Compositionality and concurrent networks: soundness and completeness of a proof system Proceedings of the 12th ICALP 1985 Nafplion, Greece Springer 509-519

Google Scholar

Cited By

View all

Angelov PIglesias J(2017)Evolving Systems: ReviewWiley Encyclopedia of Electrical and Electronics Engineering10.1002/047134608X.W8361(1-24)Online publication date: 14-Nov-2017
https://doi.org/10.1002/047134608X.W8361
Mei HLü JMei HLü J(2016)rCOS: A Refinement Calculus of Internetware SystemsInternetware10.1007/978-981-10-2546-4_14(301-333)Online publication date: 3-Dec-2016
https://doi.org/10.1007/978-981-10-2546-4_14
Zhao LLiu XLiu ZQiu Z(2009)Graph transformations for object-oriented refinementFormal Aspects of Computing10.1007/s00165-007-0067-y21:1-2(103-131)Online publication date: 1-Feb-2009
https://dl.acm.org/doi/10.1007/s00165-007-0067-y
Show More Cited By

Index Terms

Reasoning about dynamically evolving process structures
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Index terms have been assigned to the content through auto-classification.

Recommendations

Symbolic model checking composite Web services using operational and control behaviors

This paper addresses the issue of verifying if composite Web services design meets some desirable properties in terms of deadlock freedom, safety (something bad never happens), and reachability (something good will eventually happen). Composite Web ...
Complete symbolic reachability analysis using back-and-forth narrowing
Algebra and coalgebra in computer science

We propose a method called back-and-forth narrowing for solving reachability goals of the form (∃x^→).t₁ → ^*t'₁...∧t_n→^*t'_n in general term rewrite systems. The method is a complete semi-decision procedure in the sense that it is guaranteed to find a ...
Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process

Many real-life critical systems are described with large models and exhibit both probabilistic and non-deterministic behaviour. Verification of such systems requires techniques to avoid the state space explosion problem. Symbolic model checking and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 6, Issue 3

May 1994

112 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 May 1994

Accepted: 15 January 1993

Received: 15 February 1992

Published in FAC Volume 6, Issue 3

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
45
Total Downloads

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

Reflects downloads up to 13 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Angelov PIglesias J(2017)Evolving Systems: ReviewWiley Encyclopedia of Electrical and Electronics Engineering10.1002/047134608X.W8361(1-24)Online publication date: 14-Nov-2017
https://doi.org/10.1002/047134608X.W8361
Mei HLü JMei HLü J(2016)rCOS: A Refinement Calculus of Internetware SystemsInternetware10.1007/978-981-10-2546-4_14(301-333)Online publication date: 3-Dec-2016
https://doi.org/10.1007/978-981-10-2546-4_14
Zhao LLiu XLiu ZQiu Z(2009)Graph transformations for object-oriented refinementFormal Aspects of Computing10.1007/s00165-007-0067-y21:1-2(103-131)Online publication date: 1-Feb-2009
https://dl.acm.org/doi/10.1007/s00165-007-0067-y
Ahrendt WBoer FGrabe I(2009)Abstract Object Creation in Dynamic LogicProceedings of the 2nd World Congress on Formal Methods10.1007/978-3-642-05089-3_39(612-627)Online publication date: 4-Nov-2009
https://dl.acm.org/doi/10.1007/978-3-642-05089-3_39
Liu XLiu ZZhao L(2007)Object-Oriented Structure Refinement -- A Graph Transformational ApproachElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2006.08.049187(145-159)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.1016/j.entcs.2006.08.049
Jifeng HLi XLiu Z(2006)rCOSTheoretical Computer Science10.1016/j.tcs.2006.07.034365:1(109-142)Online publication date: 10-Nov-2006
https://dl.acm.org/doi/10.1016/j.tcs.2006.07.034
de Boer F(2006)Reasoning about asynchronous communication in dynamically evolving object structuresCONCUR'98 Concurrency Theory10.1007/BFb0055629(285-300)Online publication date: 28-May-2006
https://doi.org/10.1007/BFb0055629
Rustan KLeino M(2006)Recursive object types in a logic of object-oriented programsProgramming Languages and Systems10.1007/BFb0053570(170-184)Online publication date: 23-May-2006
https://doi.org/10.1007/BFb0053570
Honda KVasconcelos VKubo M(2006)Language primitives and type discipline for structured communication-based programmingProgramming Languages and Systems10.1007/BFb0053567(122-138)Online publication date: 23-May-2006
https://doi.org/10.1007/BFb0053567
Sekerinski E(2005)Verification and refinement with fine-grained action-based concurrent objectsTheoretical Computer Science10.1016/j.tcs.2004.09.024331:2-3(429-455)Online publication date: 25-Feb-2005
https://dl.acm.org/doi/10.1016/j.tcs.2004.09.024
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Abstract

References

References

Cited By

Index Terms

Recommendations

Symbolic model checking composite Web services using operational and control behaviors

Complete symbolic reachability analysis using back-and-forth narrowing

Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations