article

Free access

Compositional refinement of interactive systems

Author:

Manfred BroyAuthors Info & Claims

Journal of the ACM (JACM), Volume 44, Issue 6

Pages 850 - 891

https://doi.org/10.1145/268999.269004

Published: 01 November 1997 Publication History

Abstract

We introduce a method to describe systems and their components by functional specification techniques. We define notions of interface and interaction refinement for interactive systems and their components. These notions of refinement allow us to change both the syntactic (the number of channels and sorts of messages at the channels) and the semantic interface (causality flow between messages and interaction granularity) of an interactive system component. We prove that these notions of refinement are compositional with respect to sequential and parallel composition of system components, communication feedback and recursive declarations of system components. According to these proofs, refinements of networks can be accomplished in a modular way by refining their compponents. We generalize the notions of refinement to refining contexts. Finally, full abstraction for specifications is defined, and compositionality with respect to this abstraction is shown, too.

References

[1]

ABADI, M., AND LAMPORT, L. 1993. Composing specifications. ACM Trans. Prog. Lang. Syst. 15, 1 (Jan.), 73-132.

[2]

ABADI, M., AND PLOTKIN, G. 1991. A logical view of composition and refinement. In Proceedings of the 18th ACM Symposium on Principles of Programming Languages (Orlando, Fla., Jan. 21-23). ACM, New York, pp. 323-332.

[3]

ACETO, L., AND HENNESSY, M. 1991. Adding action refinement to a finite process algebra. In Proceedings oflCALP91. Lecture Notes in Computer Science, vol. 510. Springer-Verlag, New York, pp. 506 -519.

[4]

BACK, R. J.R. 1990a. Refinement calculus. Part I : Sequential nondeterministic programs. REX Workshop. In Stepwise Refinement of Distributed Systems. J. W. de Bakker, W.-P. de Roever, G. Rozenberg, eds. Lecture Notes in Computer Science, vol. 430. Springer-Verlag, New York, pp. 42-66.

[5]

BACK, R. J. R. 1990b. Refinement calculus. Part II : Parallel and reactive programs. REX Workshop. In Stepwise Refinement of Distributed Systems. J. W. de Bakker, W.-P. de Roever, G. Rozenberg, eds. Lecture Notes in Computer Science, vol. 430. Springer-Verlag, New York, pp. 67-93.

[6]

BACK, R. J. R. 1993a. Refinement calculus, lattices and higher-order logic. In Program Design Calculi. M. Broy, ed. Springer NATO ASI Series, Series F : Computer and System Sciences, vol. 118. Springer-Verlag, New York, pp. 53-72.

[7]

BACK, R. J.R. 1993b. Refinement of parallel and reactive programs. In Program Design Calculi. M. Broy, ed. Springer NATO ASI Series, Series F : Computer and System Sciences, vol. 118. Springer-Verlag, New York, pp. 53-72.

[8]

BROCK, J. D., AND ACKERMANN, W.B. 1981. Scenarios : A model of nondeterminate computation. In Lecture Notes in Computer Science, vol. 107. J. Diaz and I. Ramos, eds. Springer-Verlag, New York, pp. 225-259.

[9]

BaoY, M. 1982/1984. Algebraic methods for program construction : The project CIP. SOFSEM 82. Also in Program Transformation and Programming Environments, P. Pepper, ed. NATO ASI Series, Series F : 8. Springer-Verlag, New York, 1984, pp. 199-222.

[10]

BaoY, M. 1990. Functional specification of time sensitive communicating systems. REX Workshop. In Stepwise Refinement of Distributed Systems. J. W. de Bakker, W.-P. de Roever, G. Rozenberg, eds. Lecture Notes in Computer Science, vol. 430. Springer-Verlag, New York, pp. 153-179.

[11]

BaoY, M. 1993. (Inter-)action refinement : The easy way. In Program Design Calculi. M. Broy, ed. Springer NATO ASI Series, Series F : Computer and System Sciences, vol. 118. Springer-Verlag, New York, pp. 121-158.

[12]

BROY, M., MOLLER, B., PEPPER, P., AND WIRSING, M. 1986. Algebraic implementations preserve program correctness. Sci. Comput. Prog. 8, 1-19.

[13]

CHANDY, K. M., AND MISRA, J. 1988. Parallel Program Design ~ A Foundation. Addison-Wesley, Reading, Mass.

[14]

COENEN, J., DE ROEVER, W. P., AND ZWIERS, J. 1991. Assertional data reification proofs : Survey and perspective. Christian-Albrechts-Universitat Kiel, Institut ftir Informatik und praktische Mathematik. Bericht Nr. 9106.

[15]

HOARE, C. A.R. 1972. Proofs of correctness of data representations. Acta Inf. 1, 271-281.

[16]

JANSSEN, W., POEL, M., AND ZWIERS, J. 1991. Action systems and action refinement in the development of parallel systems-An algebraic approach. Unpublished manuscript.

[17]

JONES, C.B. 1986. Systematic Program Development Using VDM. Prentice-Hall, Cliffside Park, N.J.

[18]

KOZEN, D. 1983. Results on the propositional/#-calculus. Theoret. Comput. Sci. 27, 3, 333 ft.

[19]

LAMPORT, L. 1983. Specifying concurrent program modules. ACM Trans. Prog. Lang. Syst. 5, 2 (Apr.), 190-222.

[20]

SANNELLA, D. 1988. A survey of formal software development methods. Dept. Computer Sci. Univ. Edinburgh. ECS-LFCS-88-56.

[21]

VOGLER, W. 1991. Bisimulation and action refinement. In Proceedings of STACS91. Lecture Notes in Computer Science, vol. 480. Springer-Verlag, New York, pp. 309-321.

Cited By

Lamport LSchneider F(2021)Verifying Hyperproperties With TLA2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00012(1-16)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00012
Broy MKuhrmann MBroy MKuhrmann M(2021)Modelle in der Softwareentwicklung und ihre BeschreibungEinführung in die Softwaretechnik10.1007/978-3-662-50263-1_4(125-195)Online publication date: 1-Jul-2021
https://doi.org/10.1007/978-3-662-50263-1_4
Vakil Ghahani SKandemir MKotra J(2020)DSMProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/33921514:2(1-26)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3392151
Show More Cited By

Index Terms

Compositional refinement of interactive systems

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
Refinement and state machine abstraction

Precise module interface specifications are essential in modular software development. The role of state in these specifications has been the issue of some debate and is central to the notion of data refinement. In previous work, Hoffman and Strooper ...
Refinement-Based Verification of Interactive Real-Time Systems

Formal specification provides a system description that is much more precise than the natural language one and it can help to solve a lot of specification problems. But even a formal specification of a system can contain mistakes or can disagree with ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 44, Issue 6

Nov. 1997

115 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/268999

Issue’s Table of Contents

Copyright © 1997 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 1997

Published in JACM Volume 44, Issue 6

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

66
Total Citations
View Citations
961
Total Downloads

Downloads (Last 12 months)113
Downloads (Last 6 weeks)16

Reflects downloads up to 28 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lamport LSchneider F(2021)Verifying Hyperproperties With TLA2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00012(1-16)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00012
Broy MKuhrmann MBroy MKuhrmann M(2021)Modelle in der Softwareentwicklung und ihre BeschreibungEinführung in die Softwaretechnik10.1007/978-3-662-50263-1_4(125-195)Online publication date: 1-Jul-2021
https://doi.org/10.1007/978-3-662-50263-1_4
Vakil Ghahani SKandemir MKotra J(2020)DSMProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/33921514:2(1-26)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3392151
Pi YJamin SDanzig PQian F(2020)Latency Imbalance Among Internet Load-Balanced PathsProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/33921504:2(1-29)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3392150
Lin FMuzumdar KLaptev NCurelea MLee SSankar S(2020)Fast Dimensional Analysis for Root Cause Investigation in a Large-Scale Service EnvironmentProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/33921494:2(1-23)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3392149
Stolterman EWiberg M(2020)Compositional interaction design—changes in design practice and its implications for teaching and researchDigital Creativity10.1080/14626268.2020.1722708(1-20)Online publication date: 7-Feb-2020
https://doi.org/10.1080/14626268.2020.1722708
Graics BMolnár VVörös AMajzik IVarró D(2020)Mixed-semantics composition of statecharts for the component-based design of reactive systemsSoftware and Systems Modeling (SoSyM)10.1007/s10270-020-00806-519:6(1483-1517)Online publication date: 1-Nov-2020
https://dl.acm.org/doi/10.1007/s10270-020-00806-5
Beckert BMund JUlbrich MWeigl A(2019)Formal Verification of Evolutionary ChangesManaged Software Evolution10.1007/978-3-030-13499-0_11(309-332)Online publication date: 27-Jun-2019
https://doi.org/10.1007/978-3-030-13499-0_11
Westman JNyberg M(2018)Conditions of contracts for separating responsibilities in heterogeneous systemsFormal Methods in System Design10.1007/s10703-017-0294-752:2(147-192)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10703-017-0294-7
Rayana SAkoglu L(2016)Less is MoreACM Transactions on Knowledge Discovery from Data10.1145/289050810:4(1-33)Online publication date: 24-May-2016
https://dl.acm.org/doi/10.1145/2890508
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

Figures

Tables

Media

View Issue’s Table of Contents