Modellierung und Analyse diskret-kontinuierlicher Systeme , SoSe 2007

Aktuelles

Inhalt dieser Seite

• Termine
• Überblick
• Veranstaltungsinhalte
• Leistungsnachweise
• Literatur

Termine

Überblick

Veranstaltungsinhalte

Grundlagen

• Modellierung diskreter Systeme: Transitionssysteme
• Nebenläufigkeit durch shared variables bzw. Kanalkommunikation
• Reaktive Systeme, CSP
• Zeitbehaftete Systeme,Timed CSP, Timed Automata

Hybride Automaten

• Hybride Automaten
• Semantik
• Blockierende Berechnungen, Zeno-Berechnungen
• Wassertanks, Bahnübergang, Steam Boiler
• Hybrid Process Algebra - HyPA

Model Checking

• Computation Tree Logic CTL
• Grundalgorithmus CTL Model Checking
• Übersicht Tools

Aktuelle Themen der Arbeitsgruppe

• Modellierung mit HybridUML
• Echtzeitausführung mit HL³
• Generierung von Testdaten
• Deduktive Verifikation

Leistungsnachweise

Literatur

• B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucchi, Ph. Schnoebelen with P. McKenzie: Systems and Software Verification. Springer Verlag.
  Gute Einführung in die Modellierung diskreter Modelle und Model-Checking.
• Rajeev Alur, David L. Dill: A Theory of Timed Automata. Theoretical Computer Science 126(2), pp. 183 - 235, 1994.
• Thomas A.Henzinger: The Theory of Hybrid Automata
• Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Oliviero, Joseph Sifakis, and Sergio Yovine: The Algorithmic Analysis of Hybrid Systems
• Cuijpers, P.J.L., Reniers, M.A.: Hybrid process algebra The Journal of Logic and Algebraic Programming, 62-2, 191-245, 2005.

• K. H. Johansson, J. Lygeros, S. Sastry, and M. Egerstedt, "Simulation of Zeno hybrid automata" in IEEE Conference on Decision and Control, pp. 3538--3543, Phoenix, Arizona, U.S.A., December 7-10 1999.
• J. Lygeros, K.H. Johansson, S. Sastry and M. Egerstedt, On the existence of executions of hybrid automata in IEEE Conference on Decision and Control, Phoenix, AZ

• J.-R. Abrial, "The steam boiler case study project, an introduction". Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, Springer 1996.
• Thomas A. Henzinger and Howard Wong-Toi. Using HyTech to synthesize control parameters for a steam boiler. Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS 1165, Springer.
• J. Lygeros, C. Tomlin, and S. S. Sastry, "Controllers for reachability specifications for hybrid systems," Automatica, vol. 35, no. 3, March 1999.

• NuSMV
• SPIN
• KRONOS
• UPPAAL
• HyTech

• Kirsten Berkenkötter, Stefan Bisanz, Ulrich Hannemann, Jan Peleska,
  The HybridUML profile for UML 2.0,
  International Journal on Software Tools for Technology Transfer (STTT),
  volume 8, number 2, 4/2006, Springer Verlag, Berlin, Heidelberg, New York,
  
• Kirsten Berkenkötter, Stefan Bisanz, Ulrich Hannemann, Jan Peleska,
  Executable HybridUML and its Application to Train Control Systems,
  in Ehrig, Damm, Desel, Große-Rhode, Reif, Schnieder, Westkämper (editors):
  Integration of Software Specification Techniques for Applications in Engineering,
  number 3147 in Lecture Notes in Computer Science, Springer Verlag, Berlin, Heidelberg, New York, 2004
• Bahareh Badban, Martin Fränzle, Jan Peleska and Tino Teige:
  Test Automation for Hybrid Systems.
  Neelam Gupta, Yves Ledru, Johannes Mayer (eds.): Proceedings of the Third International Workshop on Software Quality Assurance (SOQUA 2006), co-located with the Fourteenth ACM SIGSOFT Symposium on Foundations of Software Engineering (ACM SIGSOFT 2006 / FSE 14), November 6, 2006, Portland, OR, USA.
• Erika Ábrahám-Mumm, Ulrich Hannemann, and Martin Steffen.
  Verification of Hybrid Systems: Formalization and Proof Rules in PVS.
  ICECCS 2001, Skövde, June 11-13, 2001.