The KORSO Case Study for software engineering with formal methods: A medical information system

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 re alistic scenario.