{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:15:39Z","timestamp":1725455739864},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540605898"},{"type":"electronic","value":"9783540478027"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0015474","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T01:32:11Z","timestamp":1131845531000},"page":"417-445","source":"Crossref","is-referenced-by-count":8,"title":["The Korso case study for software engineering with formal methods: A medical information system"],"prefix":"10.1007","author":[{"given":"Felix","family":"Cornelius","sequence":"first","affiliation":[]},{"given":"Heinrich","family":"Hu\u00dfmann","sequence":"additional","affiliation":[]},{"given":"Michael","family":"L\u00f6we","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"22_CR1","unstructured":"M. Abadi, M. Burrows, B. Lampson, and G. Plotkin. A Calculus for Access Control in Distributed Systems. Technical report, Digital Equipment Corporation, 1991."},{"key":"22_CR2","volume-title":"Technical Report A\/05\/93","author":"S. Autexier","year":"1993","unstructured":"S. Autexier. Hdms-A und Obscure in Korso \u2014 Die funktionale Essenz von Hdms-A aus Sicht der algorithmischen Spezifikationsmethode. Teil 2: Schablonen zur \u00dcbersetzung eines E\/R-Schemas in eine Obscure Spezifikation (in German). Technical Report A\/05\/93, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, December 1993."},{"key":"22_CR3","volume-title":"Technical Report A\/06\/93","author":"C. Benzm\u00fcller","year":"1993","unstructured":"C. Benzm\u00fcller. Hdms-A und Obscure in Korso \u2014 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\u00e4t des Saarlandes, Saarbr\u00fccken, December 1993."},{"key":"22_CR4","unstructured":"M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hu\u00dfmann, D. Nazareth, F. Regensbur ger, and K. St\u00f8len. The Requirement and Design Specification Language Spectrum \u2014 An Informal Introduction, Version 1.0. Technical Report TUM-I9311, TUM-I9312, Technische Universit\u00e4t M\u00fcnchen, 1993."},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"J. Bohn and H. Hungar. Traverdi \u2014 Transformation and Verification of Distributed Systems. In Broy, M. and J\u00e4hrlichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.","DOI":"10.1007\/BFb0015470"},{"key":"22_CR6","unstructured":"F. Cornelius, M. Klar, and M. L\u00f6we. Ein Fallbeispiel f\u00fcr Korso: Ist-Analyse Hdms-A (in German). Technical Report 93-28, Technische Universit\u00e4t Berlin, 1993."},{"key":"22_CR7","unstructured":"S. Conrad. Einbindung eines bestehenden Datenbanksystems in einen formalen Software-Entwicklungsproze\u00df \u2014 ein Beitrag zur Hdms-A-Fallstudie (in German). In H.-D. Ehrich, editor, Beitr\u00e4ge zu\nKorso-und\nTroll\nlight-Fallstudien, pages 1\u201314. Technische Universit\u00e4t Braunschweig, Informatik-Bericht 93-11, 1993."},{"key":"22_CR8","unstructured":"S. Conrad. Spezifikation eines vereinfachten Datenbanksystems \u2014 ein Beitrag zur Hdms-A-Fallstudie (in German). In H.-D. Ehrich, editor, Beitr\u00e4ge zu\nKorso-und\nTroll\nlight-Fallstudien, pages 15\u201326. Technische Universit\u00e4t Braunschweig, Informatik-Bericht 93-11, 1993."},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"H.-D. Ehrich et al. KORSO Reference Languages: Concepts and Application Domains. In Broy, M. and J\u00e4hrlichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.","DOI":"10.1007\/BFb0015460"},{"key":"22_CR10","unstructured":"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."},{"key":"22_CR11","unstructured":"E. Fleck, H. Hansen, B. Mahr, and H. Oswald. Systementwicklung f\u00fcr die Integration und Kommunikation von Patientendaten und-dokumenten. Forschungsbericht 02-91, PMI am DHZB, 1991."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"T. Fuch\u00df, W. Reif, G. Schellhorn, and K. Stenzel. Three Selected Case Studies in Verification. In Broy, M. and J\u00e4hrlichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.","DOI":"10.1007\/BFb0015472"},{"key":"22_CR13","unstructured":"T. Fuch\u00df. Translating E\/R-diagrams into Consistent Database Specifications. Technical Report 2\/94, Universit\u00e4t Karlsruhe, January 1994."},{"key":"22_CR14","volume-title":"Technical Report A\/07\/93","author":"M. Grosse","year":"1993","unstructured":"M. Grosse and H. Hufschmidt. SOLL-Spezifikation aus Sicht der Sicherheit (in German). Technical Report A\/07\/93, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, December 1993."},{"key":"22_CR15","volume-title":"Technical Report A\/04\/93","author":"R.A. Heckler","year":"1993","unstructured":"R.A. Heckler. Hdms-A und Obscure in Korso \u2014 Die funktionale Essenz von Hdms-A aus Sicht der algorithmischen Spezifikationsmethode. Teil 1: Einf\u00fchrung und Anmerkungen (in German). Technical Report A\/04\/93, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, December 1993."},{"key":"22_CR16","unstructured":"R. Hettler. Zur \u00dcbersetzung von E\/R-Schemata nach Spectrum (in German). Technical Report TUM-I9333, Technische Universit\u00e4t M\u00fcnchen, 1993."},{"key":"22_CR17","unstructured":"R. Hettler. A Requirement Specification for a Lexical Analyzer. Technical Report TUM-I9409, TU M\u00fcnchen, 1994."},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"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\u2013140. Springer, 1988.","DOI":"10.1007\/BFb0012828"},{"key":"22_CR19","unstructured":"H. Hu\u00dfmann. Zur formalen Beschreibung der funktionalen Anforderungen an ein Informationssystem (in german). Technical Report TUM-I9332, Technische Universit\u00e4t M\u00fcnchen, 1993."},{"key":"22_CR20","unstructured":"B. Krieg-Br\u00fcckner, W. Menzel, et al. System Architecture Framework for Korso. In Broy, M. and J\u00e4hnichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995."},{"key":"22_CR21","unstructured":"M. L\u00f6we, F. Cornelius, J. Faulhaber, and R. Wess\u00e4ly. Ein Fallbeispiel f\u00fcr Korso: Ein Vorschlag (in German). Technical Report 92-45, Technische Universit\u00e4t Berlin, 1992."},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"C. Lewerentz, T. Lindner, A. R\u00fcping, and E. Sekerinski. On Object-Oriented Design and Verification. In Broy, M. and J\u00e4hnichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.","DOI":"10.1007\/BFb0015457"},{"key":"22_CR23","unstructured":"S. McMenamin and J. Palmer. Essential Systems Analysis. Prentice-Hall, 1984."},{"key":"22_CR24","unstructured":"M. Mehlich and W. Zhang. Specifying Interactive Components for Configuratiing Graphical User Interfaces. Technical Report 9401, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, 1994."},{"key":"22_CR25","unstructured":"F. Nickl. Ablaufspezifikation durch Datenflu\u00dfmodellierung und stromverarbeitende Funktionen (in german). Technical Report TUM-I9334, Technische Universit\u00e4t M\u00fcnchen, 1993."},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"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\u00fcnchen.","DOI":"10.1007\/BFb0039717"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"P. Pepper, M. Wirsing, et al. A Method for the Development of Correct Software. In Broy, M. and J\u00e4hnichen, S., editor, Korso, Correct Software by Formal Methods, LNCS. Springer, 1995.","DOI":"10.1007\/BFb0015454"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"W. Reisig. Petri nets. Springer Verlag, 1985.","DOI":"10.1007\/978-3-642-69968-9"},{"key":"22_CR29","unstructured":"K. Renzel. Formale Beschreibung von Sicherheitsaspekten f\u00fcr das Fallbeispiel Hdms-A (in German). Technical Report 9402, Ludwig-Maximilians-Universit\u00e4t Munich, January 1994."},{"key":"22_CR30","unstructured":"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)."},{"key":"22_CR31","unstructured":"H. Shi. Benutzerschnittstelle und-Interaktion f\u00fcr die HK-Untersuchung (in German). Informatik Bericht 1\/94, Universit\u00e4t Bremen, 1994."},{"key":"22_CR32","unstructured":"O. Slotosch, F. Nickl, S. Merz, H. Hu\u00dfmann, and R. Hettler. Die funktionale Essenz von Hdms-A (in German). Technical Report TUM-I9335, Technische Universit\u00e4t M\u00fcnchen, 1993."},{"key":"22_CR33","volume-title":"Technical Report 26\/93","author":"K. Stenzel","year":"1993","unstructured":"K. Stenzel. A Verified Access Control Model. Technical Report 26\/93, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, Germany, December 1993."}],"container-title":["Lecture Notes in Computer Science","KORSO: Methods, Languages, and Tools for the Construction of Correct Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0015474","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,4]],"date-time":"2019-02-04T05:09:38Z","timestamp":1549256978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0015474"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605898","9783540478027"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/bfb0015474","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}