Abstract
Action systems provide a general description of reactive systems, capable of modeling terminating, aborting and infinitely repeating systems. Arbitrary sequential program statements can be used to describe the behavior of atomic actions. Action systems are used to extend program refinement methods for sequential programs to parallel and reactive system refinement. We give here a behavioral semantics of action systems in terms of execution traces, and define refinement of action systems in terms of this semantics. We give a simulation based proof rule for action system refinement in a reactive context, and illustrate the use of this rule with an example. The proof rule is complete under certain restrictions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82: 253–284, 1991.
R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980.
R. Back. Refinement calculus, part II: Parallel and reactive programs. In REX Workshop for Refinement of Distributed Systems volume 430 of Lecture Notes in Computer Science Nijmegen, The Netherlands, 1989. Springer-Verlag.
R. Back. Refining atomicity in parallel algorithms. In PARLE Conference on Parallel Architectures and Languages Europe Eindhoven, the Netherlands, June 1989. Springer Verlag.
R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142. ACM, 1983.
R. Back and R. Kurki-Suonio. Distributed co-operation with action systems. ACM Transactions on Programming Languages and Systems, 10: 513–554, October 1988.
R. Back and K. Sere. Stepwise refinement of action systems. Structured Programming, 12: 17–30, 1991.
R. Back and K. Sere. Superposition refinement of parallel algorithms. In K. Parker and G. Rose, editors, Formal Description Techniques IV, pages 475–493. Elsevier Science Publishers (North-Holland), 1992.
R. Back and J. von Wright. Refinement calculus, part I: Sequential programs. In REX Workshop for Refinement of Distributed Systems volume 430 of Lecture Notes in Computer Science Nijmegen, The Netherlands, 1989. Springer-Verlag.
M. Butler. Refinement and Decomposition of Value-Passing Action Systems. In E. Best, editor, CONCUR’93, volume LNCS 715. Springer-Verlag, 1993.
K. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
E. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.
B. Jonsson. Simulations between specifications of distributed systems. In Proceedings of 2nd International Conference on Concurrency Theory (CONCUR ‘81) volume 527 of Lecture Notes in Computer Science Amsterdam, The Netherlands, 1991. Springer-Verlag.
L. Lamport. A Temporal Logic of Actions. Src report 57, Digital SRC, 1990.
C. Morgan. Programming from Specifications. Prentice-Hall, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Back, R.J.R., von Wright, J. (1994). Trace Refinement of Action Systems. In: Jonsson, B., Parrow, J. (eds) CONCUR ’94: Concurrency Theory. CONCUR 1994. Lecture Notes in Computer Science, vol 836. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-48654-1_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-48654-1_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58329-5
Online ISBN: 978-3-540-48654-1
eBook Packages: Springer Book Archive