„Specification and Verification of Concurrent Systems by Causality and Realizability“
Theoretical Computer Science, Vol 974(5), August 2023, 114106
DOI: 10.1016/j.tcs.2023.114106
Hinweis: Der Artikel ist über den DOI erreichbar, aber nicht frei zugänglich.
Die erste Arbeit behandelt ein fundamentales Thema der Modellierung nebenläufiger, interaktiver nichtdeterministischer Systeme. Eine logische Theorie für die Schnittstellenspezifikation und -verifizierung verteilter, nebenläufiger, interaktiver, nichtdeterministischer Echtzeitsysteme wird auf Basis eines semantischen Modells erarbeitet, das operative und denotationale Semantik umfasst.
Sie unterstützt einen Kalkül für die Spezifikation und Verifizierung interaktiver Systeme durch Schnittstellenzusicherungen. Systeme werden so zusammengesetzt, dass sie gleichzeitig agieren und über Ströme interagieren, die über ihre Kanäle ausgetauscht werden und Rückkopplungsschleifen bilden. Eine denotationale Semantik wird definiert, die die Rückkopplungskommunikation durch Rekursion und Fixpunkte auf der Grundlage starker Kausalität und Realisierbarkeit anstelle von Monotonie handhabt. Der resultierende Verifizierungskalkül für die Spezifikationslogik wird als korrekt und relativ vollständig in Bezug auf eine operative Semantik in Form verallgemeinerter Moore-Maschinen nachgewiesen. Tatsächlich werden zwei Modelle nebenläufiger Systeme definiert, ein abstrakteres mit Kommunikation und Interaktion, die durch nicht zeitgesteuerte Ströme modelliert werden, und ein konkreteres, das mit zeitgesteuerten Strömen arbeitet. Das nicht zeitgesteuerte Modell ist eine Abstraktion des zeitgesteuerten Modells. Das zeitgesteuerte Modell ermöglicht es, die Gesetze der Kausalität und Realisierbarkeit auszudrücken. Darüber hinaus können mit dem zeitgesteuerten Modell Echtzeiteigenschaften spezifiziert werden.
„A Calculus for the Specification, Design, and Verification of Distributed Concurrent Systems“
Formal Aspects of Computing, Vol 36:3, 2024, 1-54
DOI: 10.1145/3672085
In dieser Publikation stellt Manfred Broy das Ergebnis mehrjähriger Forschungsarbeit vor: einen Kalkül, der die Spezifikation, das Design und die Verifikation verteilter Systeme unterstützt. Der Kalkül basiert auf mathematisch fundierten Konzepten und ermöglicht es, Schnittstellenverhalten formal zu beschreiben, Kausalität und Realisierbarkeit zu analysieren sowie zeitkritische Verhaltensweisen zu modellieren. Darüber hinaus bietet er eine Grundlage für die systematische Konstruktion komplexer Architekturen durch die Zusammensetzung von Teilsystemen.
Ein zentrales operatives Modell dieses Ansatzes sind generalisierte Moore'sche Maschinen. Diese erlauben eine präzise Analyse von Kausalität und Realisierbarkeit, unabhängig davon, ob der Zustandsraum endlich ist oder nicht. Der Kalkül ist sowohl für ungetimte als auch für getimte Systeme geeignet und wird durch Beispiele illustriert.
„The Role of Formal Methods in Computer Science Education“
ACM Inroads, Vol 15:4, 2024, 58-66
DOI: 10.1145/3702231
Diese Publikation entstand im Kontext der von ACM (Association for Computing Machinery) und IEEE (Institute of Electrical and Electronics Engineers) angekündigten Überarbeitung der „Computer Science Curricular Guidelines“, die weltweit Standards für Informatikstudiengänge setzen. Gemeinsam mit Maurice ter Beek und Brijesh Dongol untersucht Manfred Broy die Rolle formaler Methoden in der Informatikausbildung.
Formale Methoden sind mathematisch fundierte Ansätze, die zur präzisen Spezifikation, Analyse und Verifikation von Computersystemen eingesetzt werden. Die Autoren argumentieren, dass formales Denken essenziell ist, um wissenschaftliche Strenge und Präzision in der Softwareentwicklung zu fördern. Darüber hinaus machen sie konkrete Vorschläge, wie formale Methoden in bestehende Curricula integriert werden können, ohne andere Kernaspekte der Informatikausbildung zu verdrängen.
Weitere Informationen zu Prof. Manfred Broy
Weitere aktuelle Publikationen von Prof. Broy
M. Broy, B. Rumpe: „Development Use Cases for Semantics-Driven Modeling Languages“. In Communications of the ACM, Vol. 66, No. 05, 2023, 62-71.
M. Broy: „Logische und methodische Grundlagen der Entwicklung verteilter Systeme - unter Mitarbeit von Alexander Malkis”. Wiesbaden: Springer/Vieweg, 2023
M. Broy: „Specification and Verification of Concurrent Systems by Causality and Realizability”. In Theoretical Computer Science, Vol 974(5), 2023
M. Broy, B. Selić: “Specifying and Composing Layered Architectures”. In Journal of Object Technology, Vol. 23, No. 1, 2024, 1-24.
M. Broy: “Time, causality, and realizability: Engineering interactive, distributed software systems”. In Journal of Systems and Software, Vol. 210, 2024