Interoperabilität von Kalkülen zur Systemmodellierung
Zusammenfassung der Projektergebnisse
In praktisch allen Ansätzen der Softwaretechnik zur Beschreibung von komplexen informationsverarbeitenden Systemen werden komplementäre Sichten benutzt. Für alle relevanten Aspekte von Systemen, wie zum Beispiel Daten, Zustandsübergänge, rekursive Definitionen, etc, existieren Modelle zu deren Beschreibung. Viele dieser Modelle sind jedoch fundamental unterschiedHch. Für nahezu alle dieser Aspekte wurden in der Informatik logische und algebraische Theorien und Kalküle entwickelt, die die Verifikation, d.h. das Sicherstellen bestimmter Sicherheitskritischer Eigenschaften, ermöglichen. Jedoch sind die meisten davon auf einen bestimmten Aspekt beschränkt. Für die Verifikation von Systemen (z.B. Programmen) wird in der Informatik häufig Temporallogik verwendet. Damit können Eigenschaften, die während des Ablaufes eines Systems gelten beschrieben werden. Ziel des Projekts war es interoperable Kalküle für die Temporallogik zu entwickeln. Dies enthält den Wechsel verschiedener Sichten bei der Modellierung verteilter Systeme, die Integration verschiedener Temporallogiken, sowie die Entwicklung deduktionsfreundücher Beweistechniken. Dazu wurde ein semantischer Rahmen geschaffen, der eine große Zahl unterschiedlicher Temporallogiken integriert. Auf dieser Grundlage wurde ein Kalkül entwickelt, definiert, der u.E. einen signifikanten Fortschritt für die interaktive Verifikation temporallogischer Systeme darstellt. Dieser Kalkül wurde prototypisch in das KIV System implementiert. Ein wesentlicher Bestandteil des Projekts war auch die Entwicklung moduleirer Beweistechniken für Temporallogik. Dies verbessert die Anwendung des Kalküls bei praktisch relevanten Fallstudien. Weiter wurden einige Erweiterungen in den Kalkül integriert (z.B. Pfadquantoren, strong fairness, activity charts). Der entwickelte Kalkül wurde erfolgreich an mehreren Fallstudien getestet, aus der Fallstudie zu medizinischen Behandlungsprotokollen ist ein eigenes (von der EU gefördertes) Projekt entstanden, so dass wir uns innerhalb dieses Projekt auf andere Fallstudien, insbesondere lock-freie Algorithmen konzentriert, und diese erfolgreich bearbeitet haben. Zusammenfassend ist ein interaktive Kalkül für Anwendungssysteme entstanden, in denen mehrere Techniken und Facetten gebraucht werden, und die im allgemeinen zustandsunendlich sind, so dass sie nicht einfach mit effizienten Modelcheckern behandelt werden können. Für derartige Systeme wird bei der Verifikation auch in Zukunft die Interaktion mit dem Menschen eine erfolgsbestimmende Rolle spielen, und wir denken, dem Ziel der ingenieurmäßige Beherrschbarkeit der Verifikation solcher Anwendungssysteme einen wichtigen Schritt näher gekommen zu sein.
Projektbezogene Publikationen (Auswahl)
-
A. Thums, F. Ortmeier, W.Reif, and G. Schellhorn. Interactive verification of Statecharts. In H. Ehrig, editor, Integration of Software Specification Techniques for Applications in Engineering, pages 355 - 373. Springer LNCS 3147, 2004.
-
Andreas Thums. Formale Fehlerbaumanalyse. PhD thesis, Universität Augsburg, Augsburg, Germany, 2004.
-
Frank Ortmeier, Michael Baiser, Andriy Dunets, and Simon Bäumler. Embedding ctl* in an extension to interval temporal logic (itl). Technical Report 2008-16, University of Augsburg, 2008. (Siehe online unter: http://www.informatik.uniaugsburg. de/lelirstuehle/swt/se/publicatious/ )
-
J. Derrick, G. Schellhorn, and H. Wehrheim. Mechanising a correctness proof for a lock-free concurrent stack. In Prooceedings of FMOODS 2008, Oslo, LNCS, 2008.
-
J. Derrick, G. Schellhorn, and H. Wehrheim. Proving linearizabilty via non-atomic refinement. In J. Gibbons J. Davies, editor, Proceedings of the Intemational Conference on integrated formal methods (iFM) 2007, volume 4591 of LNCS, pages 195-214. Springer, 2007.
-
J. Schmitt, A. Hoffmann, M. Baiser, W. Reif, and M. Marcos. Interactive verification of medical guidelines. In J. Misra, T. Nipkow, and E. Sekerinski, editors. Formal Methods 2006, Proceedings, volume 4085 of LNCS, pages 32^7. Springer, 2006.
-
J. Schmitt, M. Baiser, and W. Reif Interactive verification of Asbru - a tutorial. Technical Report 2006-3, University of Augsburg, February 2006. (Siehe online unter: http://www.informatik.uniaugsburg. de/lehrstuehle/swt/se/pubUcations/ )
-
J. Schmitt, M. Baiser, and W. Reif. Interactive verification of Asbru - a tutorial. Technical Report 2006-3, University of Augsburg, February 2006. (Siehe online unter: http://www.informatik.uniaugsburg. de/lehrstuehle/swt/se/publications/ )
-
M. Baiser and A. Thums. Interactive verification of Statecharts. In Integration of Soßware Specification Techniques (INT'02), 2002.
-
M. Baiser, C. Duelli, W. Reif, and G. Schellhorn. Verifying concurrent systems with symboHc execution. Joumal of Logic and Computation, 12(4):549-560, 2002.
-
M. Baiser, C. DueUi, and W. Reif. Formal semantics of Asbru - An Overview. In Proceedings of IDPT 2002. Society for Design and Process Science, 2002.
-
M. Baiser, S. Bäumler, and W. Reif. An interval temporal logic with compositional interleaving. Technical Report 2008-20, University of Augsburg, 2008.
-
M. Baiser. Verifying (Concurrent System with Symbolic Execution - Temporal Reasoning is Symbolic Execution with a Little Induction. PhD thesis, University of Augsburg, Augsburg, Germany, 2005.
-
S. Bäumler, G. Schellhorn, M. Baiser, and W. Reif. Proving linearizability with temporal logic. Technical Report 2008- 19, Universität Augsburg, 2008. (Siehe online unter: http://www.informatik.uniaugsburg. de/lehrstuehle/swt/se/publicatious/ )
-
S. Bäumler, M. Baiser, A. Knapp, W. Reif, and A. Thums. Interactive verification of uml state machines. In Formal Methods and Soßware Engineering, number 3308 in LNCS. Springer, 2004.
-
S. Bäumler, M. Baiser, W. Reif, and J. Schmitt. Synchronous Parallelism in the Asbru Language. Technical Report 2008-11, University of Augsburg, 2008. (Siehe online unter: http://www.informatik.uniaugsburg. de/lehrstuehle/swt/se/publications/ )
-
Simon Bäumler, Florian Nafz, Michael Baiser, and Wolfgang Reif. Compositional proofs with symbolic execution. In Bemhard Beckert and Gerwin Klein, editors. Proceedings of the 5th Intemational Verification Workshop, volume 372 of Ceur Workshop Proceedings, 2008.
