Skip to main content
SpringerLink
Log in
Book cover

International Conference on Current Trends in Theory and Practice of Computer Science

SOFSEM 1998: SOFSEM’ 98: Theory and Practice of Informatics pp 19–35Cite as

A Logical Basis for Modular Software and Systems Engineering

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1521))

Abstract

We introduce a logical and mathematical theory for the specification of system components and the typical steps of the development process. In particular, we identify three patterns of development

  • refinement within one level of abstraction,

  • transition from one level of abstraction to the other,

  • implementation by glass box refinement.

We introduce refinement relations to capture these three dimensions of the development space. We give verification conditions for these refinement steps. In this way, a logical basis for the development of systems is described.

This work was carried out within the Forschungsverbund ForSoft, sponsored by the Bayerische Forschungsstiftung and the project SysLab sponsored by Siemens-Nixdorf and partially supported by the Deutsche Forschungsgemeinschaft under the Leibniz program.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, L. Lamport: The Existence of Refinement Mappings. Digital Systems Research Center, SRC Report 29, August 1988

    Google Scholar 

  2. M. Abadi, L. Lamport: Composing Specifications. Digital Systems Research Center, SRC Report66, October1990

    Google Scholar 

  3. L. Aceto, M. Hennessy: Adding Action Refinement to a Finite Process Algebra. Proc. ICALP 91, Lecture Notes in Computer Science 510, (1991), 506–519

    Google Scholar 

  4. F. Huber, B. SchÄtz, G. Einert: Consistent Graphical Specification of Distributed Systems. In: J. Fitzgerald, C. B. Jones, P. Lucas (ed.): FME’ 97: 4th International Symposium of Formal Methods Europe, Lecture Notes in Computer Science 1313, 1997, 122–141

    Google Scholar 

  5. RJ.R. Back: Refinement Calculus, Part I: Sequential Nondeterministic Programs. REX Workshop. In: J. W. deBakker, W.-P. deRoever, G. Rozenberg (eds): Stepwise Refinement of Distributed Systems. Lecture Notes in Computer Science 430, 42–66

    Google Scholar 

  6. 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 Science430, 67–93

    Google Scholar 

  7. R. Breu, R. Grosu, Franz Huber, B. Rumpe, W. Schwerin: Towards a Precise Semantics for Object-Oriented Modeling Techniques. In: H. Kilov, B. Rumpe (eds.): Proceedings ECOOP’97 Workshop on Precise Semantics for Object-Oriented Modeling Techniques, 1997, Also: Technische UniversitÄt München, Institut für Informatik, TUM-I9725, 1997

    Google Scholar 

  8. M. Broy, B. Möller, P. Pepper, M. Wirsing: Algebraic Implementations Preserve Program Correctness. Science of Computer Programming 8(1986), 1–19

    Google Scholar 

  9. 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, 153–179

    Google Scholar 

  10. M. Broy: Compositional Refinement of Interactive Systems. Digital Systems Research Center, SRC Report 89, July 1992, To appear in JACM

    Google Scholar 

  11. 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

    Google Scholar 

  12. 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

    Google Scholar 

  13. M. Broy: Interaction Refinement-The Easy Way. In:M. Broy (ed.): Program Design Calculi. Springer NATO ASI Series, Series F: Computer and System Sciences, Vol. 118, 1993

    Google Scholar 

  14. M. Broy: Algebraic Specification of Reactive Systems. M. Nivat, M. Wirsing (eds): Algebraic Methodology and Software Technology. 5th International Conference, AMAST’96, Lecture Notes of Computer Science1101, Heidelberg: Springer 1996, 487–503

    Chapter  Google Scholar 

  15. M. Broy: Towards a Mathematical Concept of a Component and its Use. First Components’ User Conference, Munich 1996. Revised version in: Software-Concepts and Tools18, 1997, 137–148

    Google Scholar 

  16. M. Broy: Refinement of Time. M. Bertran, Th. Rus(eds.): Transformation-Based Reactive System Development. ARTS’97, Mallorca 1997. Lecture Notes in Computer Science 1231, 1997, 44–63, To appear in TCS

    Google Scholar 

  17. J. Coenen, W.P. deRoever, J. Zwiers: Assertional Data Reification Proofs: Survey and Perspective. Christian-Albrechts-UniversitÄt Kiel, Institut für Informatik und praktische Mathematik, Bericht Nr. 9106, Februar1991.

    Google Scholar 

  18. C.A.R. Hoare: Proofs of Correctness of Data Representations. Acta Informatica1, 1972, 271–281

    Article  MATH  Google Scholar 

  19. N. Lynch, E. Stark: A Proof of the Kahn Principle for Input/Output Automata. Information and Computation82, 1989, 81–92

    Article  MATH  MathSciNet  Google Scholar 

  20. M. Broy: Mathematical System Models as a Basis of Software Engineering. J. van Leeuwen (ed.): Computer Science Today. Lecture Notes of Computer Science 1000, 1995, 292–306

    Google Scholar 

  21. M. Broy: A Functional Rephrasing of the Assumption/Commitment Specification Style. Technische UniversitÄt München, Institut für Informatik, TUM-I9417, June 1994, Revised and Extended Version to appear in: Formal Methods in System Design

    Google Scholar 

  22. C. Klein: Anforderungsspezifikation durch Transitionssysteme und Szenarien. Promotion, FakultÄt für Informatik, Technische UniversitÄt München, Dezember 1997

    Google Scholar 

  23. M. Broy, K. StØlen: Focus on System Development. Springer 1999 (to appear)

    Google Scholar 

  24. B. Möller: Algebraic Structures for Program Calculation. Marktoberdorf Summer School 1998

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische UniversitÄt München, D-80290, München, Germany

    Manfred Broy

Authors
  1. Manfred Broy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Comenius University, SK-84215, Bratislava, Slovakia

    Branislav Rovan

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Broy, M. (1998). A Logical Basis for Modular Software and Systems Engineering. In: Rovan, B. (eds) SOFSEM’ 98: Theory and Practice of Informatics. SOFSEM 1998. Lecture Notes in Computer Science, vol 1521. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49477-4_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-49477-4_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65260-1

  • Online ISBN: 978-3-540-49477-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation