Skip to main content
SpringerLink
Log in

The Korso case study for software engineering with formal methods: A medical information system

  • Case Studies
  • Chapter
  • First Online:
KORSO: Methods, Languages, and Tools for the Construction of Correct Software

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

Abstract

This article summarizes the experiences and results which have been achieved within one of the central case studies of the Korso project. It has been set up as the formal, size-reduced, and slightly abstracted counterpart of an actual project which has been running for several years now at a Berlin hospital. It aims at providing an open distributed information system which is able to digitally record, store and communicate all administrative and medical data occurring in the hospital. This very large project includes all of the typical aspects of contemporary software engineering in the large: systems analysis, requirements engineering, integration of semi-formal and formal specifications, integration of standard systems like databases or user interfaces, and safety and security issues. The requirements definition of the Korso case study preserves these problem fields of a representative development process. Thus it serves as an important experience on how to use formal methods in a realistic scenario.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, M. Burrows, B. Lampson, and G. Plotkin. A Calculus for Access Control in Distributed Systems. Technical report, Digital Equipment Corporation, 1991.

    Google Scholar 

  2. S. Autexier. Hdms-A und Obscure in Korso — Die funktionale Essenz von Hdms-A aus Sicht der algorithmischen Spezifikationsmethode. Teil 2: Schablonen zur Übersetzung eines E/R-Schemas in eine Obscure Spezifikation (in German). Technical Report A/05/93, Universität des Saarlandes, Saarbrücken, December 1993.

    Google Scholar 

  3. C. Benzmüller. Hdms-A und Obscure in Korso — Die funktionale Essenz von Hdms-A aus Sicht der algorithmischen Spezifikationsmethode. Teil 3: Die Spezifikation der atomaren Funktionen (in German). Technical Report A/06/93, Universität des Saarlandes, Saarbrücken, December 1993.

    Google Scholar 

  4. M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hußmann, D. Nazareth, F. Regensbur ger, and K. Stølen. The Requirement and Design Specification Language Spectrum — An Informal Introduction, Version 1.0. Technical Report TUM-I9311, TUM-I9312, Technische Universität München, 1993.

    Google Scholar 

  5. J. Bohn and H. Hungar. Traverdi — Transformation and Verification of Distributed Systems. In Broy, M. and Jährlichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.

    Google Scholar 

  6. F. Cornelius, M. Klar, and M. Löwe. Ein Fallbeispiel für Korso: Ist-Analyse Hdms-A (in German). Technical Report 93-28, Technische Universität Berlin, 1993.

    Google Scholar 

  7. S. Conrad. Einbindung eines bestehenden Datenbanksystems in einen formalen Software-Entwicklungsprozeß — ein Beitrag zur Hdms-A-Fallstudie (in German). In H.-D. Ehrich, editor, Beiträge zu Korso-und Troll light-Fallstudien, pages 1–14. Technische Universität Braunschweig, Informatik-Bericht 93-11, 1993.

    Google Scholar 

  8. S. Conrad. Spezifikation eines vereinfachten Datenbanksystems — ein Beitrag zur Hdms-A-Fallstudie (in German). In H.-D. Ehrich, editor, Beiträge zu Korso-und Troll light-Fallstudien, pages 15–26. Technische Universität Braunschweig, Informatik-Bericht 93-11, 1993.

    Google Scholar 

  9. H.-D. Ehrich et al. KORSO Reference Languages: Concepts and Application Domains. In Broy, M. and Jährlichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.

    Google Scholar 

  10. M. Eimermacher, H. Hansen, R.D. Kutsche, H. Ogrodowczyk, C. Ohm, D. Paparoditis, C. Rost, and C. Strzyz. Auswertung der Systemanalyse. Interner Arbeitsbericht 17-89, PMI am DHZB, 1989.

    Google Scholar 

  11. E. Fleck, H. Hansen, B. Mahr, and H. Oswald. Systementwicklung für die Integration und Kommunikation von Patientendaten und-dokumenten. Forschungsbericht 02-91, PMI am DHZB, 1991.

    Google Scholar 

  12. T. Fuchß, W. Reif, G. Schellhorn, and K. Stenzel. Three Selected Case Studies in Verification. In Broy, M. and Jährlichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.

    Google Scholar 

  13. T. Fuchß. Translating E/R-diagrams into Consistent Database Specifications. Technical Report 2/94, Universität Karlsruhe, January 1994.

    Google Scholar 

  14. M. Grosse and H. Hufschmidt. SOLL-Spezifikation aus Sicht der Sicherheit (in German). Technical Report A/07/93, Universität des Saarlandes, Saarbrücken, December 1993.

    Google Scholar 

  15. R.A. Heckler. Hdms-A und Obscure in Korso — Die funktionale Essenz von Hdms-A aus Sicht der algorithmischen Spezifikationsmethode. Teil 1: Einführung und Anmerkungen (in German). Technical Report A/04/93, Universität des Saarlandes, Saarbrücken, December 1993.

    Google Scholar 

  16. R. Hettler. Zur Übersetzung von E/R-Schemata nach Spectrum (in German). Technical Report TUM-I9333, Technische Universität München, 1993.

    Google Scholar 

  17. R. Hettler. A Requirement Specification for a Lexical Analyzer. Technical Report TUM-I9409, TU München, 1994.

    Google Scholar 

  18. M. Heisel, W. Reif, and W. Stephan. Implementing Verification Strategies in the Kiv-System. In E. Lusk and R. Overbeek, editors, Proc. 9th International Conference on Automated Deduction, volume 310 of LNCS, pages 131–140. Springer, 1988.

    Google Scholar 

  19. H. Hußmann. Zur formalen Beschreibung der funktionalen Anforderungen an ein Informationssystem (in german). Technical Report TUM-I9332, Technische Universität München, 1993.

    Google Scholar 

  20. B. Krieg-Brückner, W. Menzel, et al. System Architecture Framework for Korso. In Broy, M. and Jähnichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.

    Google Scholar 

  21. M. Löwe, F. Cornelius, J. Faulhaber, and R. Wessäly. Ein Fallbeispiel für Korso: Ein Vorschlag (in German). Technical Report 92-45, Technische Universität Berlin, 1992.

    Google Scholar 

  22. C. Lewerentz, T. Lindner, A. Rüping, and E. Sekerinski. On Object-Oriented Design and Verification. In Broy, M. and Jähnichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.

    Google Scholar 

  23. S. McMenamin and J. Palmer. Essential Systems Analysis. Prentice-Hall, 1984.

    Google Scholar 

  24. M. Mehlich and W. Zhang. Specifying Interactive Components for Configuratiing Graphical User Interfaces. Technical Report 9401, Ludwig-Maximilians-Universität München, 1994.

    Google Scholar 

  25. F. Nickl. Ablaufspezifikation durch Datenflußmodellierung und stromverarbeitende Funktionen (in german). Technical Report TUM-I9334, Technische Universität München, 1993.

    Google Scholar 

  26. F. Nickl and M. Wirsing. A Formal Approach to Requirements Engineering. In Proceedings of the International Symposium on Formal Methods in Programming and their Applications, Novosibirsk. Springer LNCS, July 1993. Also appeared as technical report no. 9314 at the Ludwig-Maximilians-University München.

    Google Scholar 

  27. P. Pepper, M. Wirsing, et al. A Method for the Development of Correct Software. In Broy, M. and Jähnichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.

    Google Scholar 

  28. W. Reisig. Petri nets. Springer Verlag, 1985.

    Google Scholar 

  29. K. Renzel. Formale Beschreibung von Sicherheitsaspekten für das Fallbeispiel Hdms-A (in German). Technical Report 9402, Ludwig-Maximilians-Universität Munich, January 1994.

    Google Scholar 

  30. M. Schulte. Spezifikation und Verifikation von kommunizierenden Objekten in einem verteilten System (in German). Master's thesis, University of Oldenburg, Computer Science Department, March 1994. (in German).

    Google Scholar 

  31. H. Shi. Benutzerschnittstelle und-Interaktion für die HK-Untersuchung (in German). Informatik Bericht 1/94, Universität Bremen, 1994.

    Google Scholar 

  32. O. Slotosch, F. Nickl, S. Merz, H. Hußmann, and R. Hettler. Die funktionale Essenz von Hdms-A (in German). Technical Report TUM-I9335, Technische Universität München, 1993.

    Google Scholar 

  33. K. Stenzel. A Verified Access Control Model. Technical Report 26/93, Fakultät für Informatik, Universität Karlsruhe, Germany, December 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität Berlin, Deutschland

    Felix Cornelius & Michael Löwe

  2. Technische Universität München, Deutschland

    Heinrich Hußmann

Authors
  1. Felix Cornelius
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Heinrich Hußmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Löwe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Manfred Broy Stefan Jähnichen

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Cornelius, F., Hußmann, H., Löwe, M. (1995). The Korso case study for software engineering with formal methods: A medical information system. In: Broy, M., Jähnichen, S. (eds) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Lecture Notes in Computer Science, vol 1009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015474

Download citation

  • DOI: https://doi.org/10.1007/BFb0015474

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60589-8

  • Online ISBN: 978-3-540-47802-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation