Abstract
Action systems are used to extend program refinement methods for sequential programs, as described in the refinement calculus, to parallel and reactive system refinement. They provide a general description of reactive systems, capable of modeling terminating, possibly aborting and infinitely repeating systems. We show how to extend the action system model to refinement of modular systems. A module may export and import variables, it may provide access procedures for other modules, and it may itself access procedures of other modules. Modules may have autonomous internal activity and may execute in parallel or in sequence. Modules may be nested within each other. They may communicate by shared variables, shared actions, a generalized form of remote procedure calls and by persistent data structures. Both synchronous and asynchronous communication between modules is supported. The paper shows how a single framework can be used for both the specification of large systems, the modular decomposition of the system into smaller units and the refinement of the modules into program modules that can be described in a standard programming language and executed on standard hardware.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980.
R. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593–624, 1988.
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. J. R. Back, A. J. Martin and K. Sere. Specification of a Microprocessor. Department of Computer Science, Åbo Akademi University, Turku, Finland, 1993.
R. Back and K. Sere. Stepwise refinement of action systems. Structured Programming, 12:17–30, 1991.
R. J. R. Back and K. Sere. Action Systems with Synchronous Communication. To appear in E.-R. Olderog, editor, IFIP TC 2 Working Conference, on Programming Concepts, Methods and Calculi (PROCOMET '94), pages 107–126. Elsevier, 1994.
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.
R. Back and J. von Wright. Trace refinement of action systems. To appear in Proc. of CONCUR '94, Uppsala, Sweden, Augusti 1994.
K. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
E. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.
N. Francez. Cooperating proofs for distributed programs with multiparty interaction. Information Processing Letters, 32:235–242, September 1989, North-Holland.
N. Francez, B. T. Hailpern and G. Taubenfeld. SCRIPT-A communication abstraction mechanism and its verification. Science of Computer Programming, 6:35–88, 1986.
C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, August 1978.
INMOS Ltd. occam Programming Manual. Prentice-Hall International, 1984.
C. C. Morgan. Data Refinement by Miracles. Information Processing Letters 26:243–246, January 1988.
C. Morgan. Programming from Specifications. Prentice-Hall, 1990.
J. M. Morris. A Theoretical Basis for Stepwise Refinement and the Programming Calculus. Science of Computer Programming, 9:287–306, 1987.
G. Nelson. A Generalization of Dijkstra's Calculus. ACM Transactions on Programming Languages and Systems, 11(4):517–562, October 1989.
United States Department of Defence. Reference manual for the Ada programming language. ANSI/MIL-STD-1815A-1983, American National Standards Institute, New York, 1983.
N. Wirth. The programming language Oberon. Software — Practice and Experience, 18(7), 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Back, R.J.R., Sere, K. (1994). From action systems to modular systems. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_83
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_83
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive