Suche

Modellierung, Spezifikation und Verifikation reaktiver Systeme


Reaktive Systeme verarbeiten Informationen unter Reaktion auf und in Interaktion mit einer Umgebung. Typische Vertreter sind Betriebssysteme und Software für Steuergeräte; häufig finden sich reaktive Systeme in sicherheitskritischen Bereichen, etwa medizinischen Anwendungen, Zahlungssystemen oder Zugangskontrollsystemen, in denen hohe Zuverlässigkeitsanforderungen gestellt werden. Die prägenden Eigenschaften reaktiver Systeme sind ebenläufigkeit, Kommunikation und Nichtterminierung. Die Vorlesung stellt Ansätze zur Modellierung und Spezifikation reaktiver Systeme vor und gibt eine Einführung in Verfeinerungs- und Verifikationstechniken für zuverlässige, reaktive Systeme.

Schlagwörter: Transitionssysteme, Sicherheits- und Lebendigkeitseigenschaften; strombasierte Spezifikationen; nebenläufige Termersetzungssysteme (z. B. Maude); Prozeßalgebren (z. B. Calculus of Communicating Systems, Communicating Sequential Processes, pi-Kalkül), Simulation und Bisimulation; Temporallogik, symbolisches Model checking, automatenbasiertes Model checking, Abstraktion; Temporal Logic of Actions, Verfeinerung

Literatur:

  • Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, Jiří Srba. Reactive Systems: Modelling, Specification and Verification. Cambride University Press, 2007.
  • Christel Baier, Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.
  • Klaus Schneider. Verification of Reactive Systems. Springer, 2003.
  • Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott. All About Maude - A High-Performance Logical Framework.How to Specify, Program, and Verify Systems in Rewriting Logic. Lect. Notes Comp. Sci. 4350, Springer, 2007.
  • Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
  • Robin Milner. Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, 1999.
  • Fred Kröger, Stephan Merz. Temporal Logic and State Systems. Springer, 2008.
  • Edmund M. Clarke, Jr., Orna Grumberg, Doron A. Peled. Model Checking. MIT Press, 1999.
  • Leslie Lamport. Specifying Systems. Addison-Wesley, 2003.

Folien