Advertisement

(Inter-)Action Refinement: The Easy Way

  • Manfred Broy
Part of the NATO ASI Series book series (NATO ASI F, volume 118)

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.

Keywords

Representation Specification Parallel Composition Concrete Level State Transition System Communication History 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Abadi, Lamport 88]
    M. Abadi, L. Lamport: The Existence of Refinement Mappings. Digital Systems Research Center, SRC Report 29, August 1988Google Scholar
  2. [Abadi, Lamport 90]
    M. Abadi, L. Lamport: Composing Specifications. Digital Systems Research Center, SRC Report 66, October 1990Google Scholar
  3. [Aceto, Hennessy 91]
    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–519Google Scholar
  4. [Back 88a]
    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–66Google Scholar
  5. [Back 88b]
    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–93Google Scholar
  6. [Broy et al. 86]
    M. Broy, B. Möller, P. Pepper, M. Wirsing: Algebraic Implementations Preserve Program Correctness. Science of Computer Programming 8 (1986), 1–19Google Scholar
  7. [Broy 90]
    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–179Google Scholar
  8. [Broy 92a]
    M. Broy: Experiences with Machine Supported Software and System Specification and Verification: Using the Larch Prover. Digital Systems Research Center, SRC Report 93, 1992Google Scholar
  9. [Broy 92b]
    M. Broy: Compositional Refinement of Interactive Systems. Digital Systems Research Center, SRC Report 89, July 1992Google Scholar
  10. [Broy et al. 92a]
    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 1992Google Scholar
  11. [Broy et al. 92b]
    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 1992Google Scholar
  12. [CIP 84]
    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–222Google Scholar
  13. [Coenen et al. 91]
    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.Google Scholar
  14. [Hoare 72]
    C.A.R. Hoare: Proofs of Correctness of Data Representations. Acta Informatica 1, 1972, 271–281CrossRefMATHGoogle Scholar
  15. [Janssen et al. 91]
    W. Janssen, M. Poel, J. Zwiers: Action Systems and Action Refinement in the Development of Parallel Systems - An Algebraic Approach. Unpublished ManuscriptGoogle Scholar
  16. [Jones 86]
    C.B. Jones: Systematic Program Development Using VDM. Prentice Hall 1986Google Scholar
  17. [Lamport 83]
    L. Lamport: Specifying Concurrent Program Modules. ACM Toplas 5: 2, April 1983, 190–222CrossRefMATHGoogle Scholar
  18. [Lynch, Stark 89]
    N. Lynch, E. Stark: A Proof of the Kahn Principle for Input/Output Automata. Information and Computation 82, 1989, 81–92MathSciNetCrossRefMATHGoogle Scholar
  19. [Nipkow 86]
    T. Nipkow: Non-deterministic Data Types: Models and Implementations. Acta Informatica 22, 1986, 629–661MathSciNetCrossRefMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Manfred Broy
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchenGermany

Personalised recommendations