Abstract
We outline and illustrate a formal concept for the specification and refinement of networks of interactive components. We describe systems by modular, functional specification techniques. We distinguish between black box and glass box views of interactive system components as well as refinements of their black box and glass box views. We identify and discuss several classes of refinements such as behaviour refinement, communication history refinement, interface interaction refinement, state space refinement, distribution refinement, and others. In particular, we demonstrate how these concepts of refinement and their verification are supported by functional specification techniques leading to a general formal refinement calculus. It can be used as the basis for a method for the development of distributed interactive systems.
This work was supported by the Sonderforschungsbereich 342 “Werkzeuge und Methoden für die Nutzung paralleler Architekturen”
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, L. Lamport: The Existence of Refinement Mappings. Digital Systems Research Center, SRC Report 29, August 1988
M. Abadi, L. Lamport: Composing Specifications. Digital Systems Research Center, SRC Report 66, October 1990
L. Aceto, M. Hennessy: Adding Action Refinement to a Finite Process Algebra. Proc. ICALP 91, Lecture Notes in Computer Science 510. Berlin: Springer-Verlag 1991, 506–519
R.J.R. Back: Refinement Calculus, Part I: Sequential Nondeterministic Programs REX Workshop. In: J. W. deBakker, W.-P. de Roever, G. Rozenberg (eds): Stepwise Refinement of Distributed Systems. Lecture Notes in Computer Science 430. Berlin: Springer-Verlag 1988, 42–66
R.J.R. Back: Refinement Calculus, Part II: Parallel and Reactive Programs REX Workshop. In: J. W. de Bakker, W.-P. de Roever, G. Rozenberg (eds): Stepwise Refinement of Distributed Systems. Lecture Notes in Computer Science 430. Berlin: Springer-Verlag 1988, 67–93
M. Broy, B. Möller, P. Pepper, M. Wirsing: Algebraic Implementations Preserve Program Correctness. Science of Computer Programming 8 (1986), 1–19
M. Broy: Functional Specification of Time Sensitive Communicating Systems. REX Workshop. In: J. W. de Bakker, W.-P. de Roever, G. Rozenberg (eds): Stepwise Refinement of Distributed Systems. Lecture Notes in Computer Science 430. Berlin: Springer-Verlag 1990, 153–179
M. Broy: Experiences with Machine Supported Software and System Specification and Verification: Using the Larch Prover. Digital Systems Research Center, SRC Report 93, 1992
M. Broy: Compositional Refinement of Interactive Systems. Digital Systems Research Center, SRC Report 89, July 1992
M. Broy, F. Dederichs, C. Dendorfer, M. Fuchs, T. F. Gritzner, R. Weber: The Design of Distributed Systems - An Introduction to Focus. Technische Universität München, Institut für Informatik, Sonderforschungsbereich 342: Methoden und Werkzeuge für die Nutzung paralleler Architekturen TUM-I9202, January 1992
M. Broy, F. Dederichs, C. Dendorfer, M. Fuchs, T. F. Gritzner, R. Weber: Summary of Case Studies in FOCUS - a Design Method for Distributed Systems. Technische Universität München, Institut für Informatik, Sonderforschungsbereich 342: Methoden und Werkzeuge für die Nutzung paralleler Architekturen TUM-I9203, January 1992
M. Broy: Algebraic Methods for Program Construction: The Project CIP. SOFSEM 82, see also: P. Pepper (ed.): Program Transformation and Programming Environments. NATO ASI Series. Series F 8. Berlin: Springer-Verlag 1984, 199–222
J. Coenen, W.P. de Roever, J. Zwiers: Assertional Data Reification Proofs: Survey and Perspective. Christian-Albrechts-Universität Kiel, Institut für Informatik und Praktische Mathematik, Bericht Nr. 9106, Februar 1991.
C.A.R. Hoare: Proofs of Correctness of Data Representations. Acta Informatica 1, 1972, 271–281
W. Janssen, M. Poel, J. Zwiers: Action Systems and Action Refinement in the Development of Parallel Systems - An Algebraic Approach. Unpublished Manuscript
C.B. Jones: Systematic Program Development Using VDM. Prentice Hall 1986
L. Lamport: Specifying Concurrent Program Modules. ACM Toplas 5: 2, April 1983, 190–222
N. Lynch, E. Stark: A Proof of the Kahn Principle for Input/Output Automata. Information and Computation 82, 1989, 81–92
T. Nipkow: Non-deterministic Data Types: Models and Implementations. Acta Informatica 22, 1986, 629–661
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Broy, M. (1993). (Inter-)Action Refinement: The Easy Way. In: Broy, M. (eds) Program Design Calculi. NATO ASI Series, vol 118. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-02880-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-662-02880-3_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-08164-4
Online ISBN: 978-3-662-02880-3
eBook Packages: Springer Book Archive