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

research-article

Open access

Superposition refinement of reactive systems

Authors:

K. SereAuthors Info & Claims

Formal Aspects of Computing, Volume 8, Issue 3

Pages 324 - 346

https://doi.org/10.1007/BF01214918

Published: 01 May 1996 Publication History

Abstract

Superposition refinement enhances an algorithm by superposing one computation mechanism onto another mechanism, in a way that preserves the behavior of the original mechanism. Superposition seems to be particularly well suited to the development of parallel and distributed programs: an originally simple sequential algorithm can be extended with mechanisms that distribute control and state information to many processes, thus permitting efficient parallel execution of the algorithm. We will show in this paper how superposition of reactive systems is expressed in the refinement calculus. We illustrate the power of this method by a case study, showing how a distributed broadcasting system is derived through a sequence of superposition refinements.

References

References

[1]

Back R. J. R. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts 1980 Amsterdam Mathematical Centre

[2]

Back R. J. R. A calculus of refinements for program derivations Acta Informatica 1988 25 593-624

Digital Library

[3]

Back. R. J. R.: Refinement calculus, part II: Parallel and reactive programs. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings. 1989, volume 430 ofLecture Notes in Computer Science, pages 67–93. Springer-Verlag, 1990.

[4]

Back, R. J. R. and Kurki-Suonio, R.: Decentralization of process nets with centralized control. InProc. of the 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983.

[5]

Back, R. J. R. and Sere, K.: Deriving an occam implementation of action systems. InProc. of the 3rd Refinement Workshop BCS FACS/IBM UK Laboratories/Oxford University, Hursley Park, England, January 1990.Workshops in Computing, Springer-Verlag, 1991.

[6]

Back R. J. R. and Sere K. Stepwise refinement of parallel algorithms Science of Computer Programming 1990 1 1 133-180

Digital Library

[7]

Back, R. J. R. and Sere, K.: Superposition refinement of parallel algorithms. In K. R. Parker, and G. A. Rose, editors,Formal Description Techniques, IV, IFIP Transactions C-2, pages 475–494. North-Holland, 1992.

[8]

Back, R. J. R. and Wright, J. von: Refinement calculus, part I: Sequential nondeterministic programs. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings. 1989, volume 430 ofLecture Notes in Computer Science, pages 42–66. Springer-Verlag, 1990.

[9]

Bougé, L. and Francez, N.: A compositional approach to superposition. InProc. of the 14th ACM Conference on Principles of Programming Languages, pages 240–249, San Diego, California, USA, January 13–15 1988.

[10]

Chandy, K. and Misra, J.:Parallel Program Design: A Foundation. Addison-Wesley, 1988.

[11]

Dijkstra, E. W.:A Discipline of Programming. Prentice-Hall International, 1976.

[12]

Dijkstra E. W., Lamport L., Martin A. J., Scholten C. S., and Steffen E. F. M. Onthe-fly garbage collection: An exercise in cooperation Communications of the ACM 1978 21 966-975

Digital Library

[13]

Francez N. and Forman I. R. Baeten J. C. M. and Klop J. W. Superimposition for interacting processes CONCUR '90 Theories of Concurrency: Unification and Extension. Proceedings, volume 458 of Lecture Notes in Computer Science 1990 Amsterdam, the Netherlands Springer London 230-245

[14]

Katz S. M. A superimposition control construct for distributed systems ACM Transactions on Programming Languages and Systems 1993 15 2 337-356

Digital Library

[15]

Kurki-Suonio, R. and Järvinen. H.-M.: Action system approach to the specification and design of distributed systems. InProc. of the 5th International Workshop on Software Specification and Design, pages 34–40. ACM Software Engineering Notes 14(3), May 1989.

[16]

Morgani C. C. The specification statement ACM Transactions on Programming Languages and Systems 1988 10 3 403-419

Digital Library

[17]

Morris J. M. A theoretical basis for stepwise refinement and the programming calculus Science of Computer Programming 1987 9 287-306

Digital Library

[18]

Ramesh S. and Mehndiratta S. L. A methodology for developing distributed programs IEEE Transactions on Software Engineering 1987 SE-13 8 967-976

Digital Library

[19]

Sere K. Stepwise Derivation of Parallel Algorithms PhD thesis 1990 Turku, Finland Department of Computer Science, Åbo Akademi University

Cited By

Toman SLahouij AKotel SHamel LToman ZGraiet M(2024)Service to service communication based on CBPS system: refinement and verificationSoft Computing - A Fusion of Foundations, Methodologies and Applications10.1007/s00500-024-09902-w28:19(10943-10963)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/s00500-024-09902-w
Hussein Toman SHamel LLahouij AHussein Toman ZGraiet M(2024)Ensuring the Correctness and Reliability of CBPS System Using Event‐BSoftware Testing, Verification and Reliability10.1002/stvr.190435:1Online publication date: Nov-2024
https://doi.org/10.1002/stvr.1904
Sanwal UHoang TPetre LPetre I(2022)Scalable reaction network modeling with automatic validation of consistency in Event-BScientific Reports10.1038/s41598-022-05308-612:1Online publication date: 25-Jan-2022
https://doi.org/10.1038/s41598-022-05308-6
Show More Cited By

Index Terms

Superposition refinement of reactive systems

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

Recommendations

Automated verification of refinement laws

Demonic refinement algebras are variants of Kleene algebras. Introduced by von Wright as a light-weight variant of the refinement calculus, their intended semantics are positively disjunctive predicate transformers, and their calculus is entirely within ...
Superposition, entanglement and quantum computation

The paper examines the roles played by superposition and entanglement in quantum computing. The analysis is illustrated by discussion of a 'classical' electronic implementation of Grover's quantum search algorithm. It is shown explicitly that the ...
Can Refinement be Automated?

We automatically verify Back's atomicity refinement law and a classical data refinement law for action systems. Our novel approach mechanises a refinement calculus based on Kleene algebras in an off the shelf resolution and paramodulation theorem prover ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 8, Issue 3

May 1996

132 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© BCS 1996.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 May 1996

Accepted: 15 August 1995

Received: 15 January 1993

Published in FAC Volume 8, Issue 3

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

85
Total Citations
View Citations
57
Total Downloads

Downloads (Last 12 months)33
Downloads (Last 6 weeks)5

Reflects downloads up to 20 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Toman SLahouij AKotel SHamel LToman ZGraiet M(2024)Service to service communication based on CBPS system: refinement and verificationSoft Computing - A Fusion of Foundations, Methodologies and Applications10.1007/s00500-024-09902-w28:19(10943-10963)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/s00500-024-09902-w
Hussein Toman SHamel LLahouij AHussein Toman ZGraiet M(2024)Ensuring the Correctness and Reliability of CBPS System Using Event‐BSoftware Testing, Verification and Reliability10.1002/stvr.190435:1Online publication date: Nov-2024
https://doi.org/10.1002/stvr.1904
Sanwal UHoang TPetre LPetre I(2022)Scalable reaction network modeling with automatic validation of consistency in Event-BScientific Reports10.1038/s41598-022-05308-612:1Online publication date: 25-Jan-2022
https://doi.org/10.1038/s41598-022-05308-6
Dihego JSampaio AOliveira M(2020)A refinement checking based strategy for component-based systems evolutionJournal of Systems and Software10.1016/j.jss.2020.110598167(110598)Online publication date: Sep-2020
https://doi.org/10.1016/j.jss.2020.110598
Nakajima S(2020)Constructing Rigorous Sketches for Refinement-Based Formal Development: An Application to AndroidImplicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems10.1007/978-981-15-5054-6_15(331-346)Online publication date: 28-Jul-2020
https://doi.org/10.1007/978-981-15-5054-6_15
Banach R(2020)Verification-Led Smart ContractsFinancial Cryptography and Data Security10.1007/978-3-030-43725-1_9(106-121)Online publication date: 13-Mar-2020
https://doi.org/10.1007/978-3-030-43725-1_9
Zhao YSanan DZhang FLiu Y(2019)Refinement-Based Specification and Security Analysis of Separation KernelsIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2017.267298316:1(127-141)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1109/TDSC.2017.2672983
Zhao YSanán DZhang FLiu Y(2019)A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive SystemsFormal Methods – The Next 30 Years10.1007/978-3-030-30942-8_11(161-178)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-30942-8_11
Reich JSchneider D(2018)Towards (Semi-)Automated Synthesis of Runtime Safety Models: A Safety-Oriented Design Approach for Service Architectures of Cooperative Autonomous SystemsDevelopments in Language Theory10.1007/978-3-319-99229-7_13(139-150)Online publication date: 21-Aug-2018
https://doi.org/10.1007/978-3-319-99229-7_13
Derrick JBoiten EDerrick JBoiten E(2018)Perspicuity, Divergence, and Internal OperationsRefinement10.1007/978-3-319-92711-4_5(69-81)Online publication date: 4-Sep-2018
https://doi.org/10.1007/978-3-319-92711-4_5
Show More Cited By

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents