Zustandsbasierte Systeme und versteckte Datentypen


	Zustandsbasierte Systeme und versteckte Datentypen (ZSVD)

	Wahlveranstaltung im SS 07 2 SWS Schwerpunktgebiete 1 (Software-Konstruktion), 4 (Algorithmen, Komplexität und formale Modelle) und 5 (Sicherheit und Verifikation) Inhalt: Die LV behandelt mathematische Modelle und Verifikationsmethoden für zustandsbasierte Systeme. Man spricht auch von versteckten, destruktorbasierten Datentypen im Unterschied zu den sichtbaren, konstruktorbasierten, die zur Modellierung nicht-zustandsbasierter statischer Systeme verwendet und z.B. in der Wahlpflicht-LV Formale Methoden des Systementwurfs ausführlich diskutiert werden. Das Rechnen mit versteckten Datentypen, ihre Verifikation und Anwendungsbereiche bilden zur Zeit einen Forschungsschwerpunkt im Bereich formaler Methoden, und zwar in modelltheoretischer Hinsicht (Stichwort Coalgebren), bei der semantischen Fundierung von Sprachkonzepten (Stichwort Objektorientierung) und der Verifikationsmethodik (Stichwort Coinduktion). Endliche, in ihrem Aufbau bekannte sichtbare Strukturen lassen sich fast immer als Termbäume modellieren. Der hierarchische Aufbau erlaubt es, Eigenschaften solcher Strukturen induktiv zu beweisen (oder zu widerlegen). Die Informatik arbeitet aber auch mit zahlreichen Modellen, die keine hierarchische Struktur aufweisen: Automaten, Transitionssysteme, Ströme, alle Arten von black-box-Modellen, die sich dadurch auszeichnen, dass man mit ihnen rechnen kann, ohne den genauen Aufbau der Objekte zu kennen. Stattdessen spricht man von Objekt-Zuständen, die sich nicht anhand ihrer Struktur, sondern anhand von Experimenten, Beobachtungen, Messungen voneinander unterscheiden lassen, während die Objekte selbst unsichtbar bleiben. Schon diese anschauliche Gegenüberstellung lässt vermuten, dass hinter black-box-Modellen mathematische Konzepte stehen, die zu den o.g. konstruktorbasierten dual sind. Die mathematische Theorie, in der Dualitäten eine zentrale Stellung einnehmen, ist die Kategorientheorie. Ausgehend von den zentralen Konstruktionen der Kategorientheorie wird in der LV eine Spezifikations- und Verifikationsmethodik entwickelt, die auf diesen Dualitäten aufsetzt und daher für black- und white-box-Modellierung gleichermaßen geeignet ist und alle üblichen Ansätze subsumiert. Kompetenzen: Es werden Kenntnisse der grundlegenden kategorien- und typtheoretischen Konstruktionen zur Modellierung und Verifikation konstruktor- wie destruktorbasierter Systeme mit sichtbaren wie versteckten Komponenten vermittelt. Darüberhinaus sollen die Studierenden lernen einzuschätzen, welche dieser Konstruktionen und darauf aufbauenden Werkzeuge für welche Anwendungen geeignet bzw. nicht geeignet sind und wie man sie ggf. an spezielle Anforderungen anpassen kann. In der LV verwendete Literatur: Peter Padawitz, Dialgebraic Specification and Modeling + Folien Peter Padawitz, Swinging Types at Work Peter Padawitz, Formale Methoden des Systementwurfs Literatur über Coalgebren, coalgebraische Logik und coalgebraische Spezifikation: Jiri Adamek, Introduction to Coalgebra Michel Bidoit, Rolf Hennicker, Alexander Kurz, Observational logic, constructor-based logic, and their duality, Theoretical Computer Science 298 (2003) 471-510 Corina Cirstea, A Coalgebraic Equational Approach to Specifying Observational Structures Andrew D. Gordon, Bisimilarity as a Theory of Functional Programming, Theoretical Computer Science 228 (1999) 5-47 Heinz Peter Gumm, Universelle Coalgebra Heinz Peter Gumm, State Based Systems are Coalgebras Heinz Peter Gumm, Universal Coalgebras and their Logics Ichiro Hasuo, Modal Logic for Coalgebras - A Survey Bart Jacobs, Jan Rutten, A Tutorial on (Co)Algebras and (Co)Induction, EATCS Bulletin 62 (1997) 222-259. Bart Jacobs, Exercises in Coalgebraic Specification, Springer LNCS 2297 (2002) 237-280 Bart Jacobs, Introduction to Coalgebra. Towards Mathematics of States and Observations, book draft (2005) Alexander Kurz, Coalgebras and Modal Logic Till Mossakowski, Horst Reichel, Markus Roggenbach, Lutz Schröder, Algebraic-coalgebraic specification in CoCASL Jan Rutten, D. Turi, Initial algebra and final coalgebra semantics for concurrency (1994) Jan Rutten, Universal Coalgebra: A Theory of Systems (1996), Theoretical Computer Science 249 (2000) 3-80 (Weitere) Einführungen in Kategorientheorie und Universelle Algebra: wiki1 wiki2 wiki3 Michael Barr, Charles Wells, Category Theory, Lecture Notes (1999) R.F.C. Walters, Categories and Computer Science, Cambridge University Press 1992 Michael Arbib, Ernest Manes, Arrows, Structures, and Functors, Academic Press (1975) Benjamin C. Pierce, Basic Category Theory for Computer Scientists, MIT Press (1991) J.A. Goguen, A Categorical Manifesto, Mathematical Structures in Computer Science 1 (1991) 49–67 Goguen, Thatcher, Wagner, Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM 24 (1977) 68-95 Ehrig, Mahr, Cornelius, Große-Rhode, Zeitz, Mathematisch-strukturelle Grundlagen der Informatik, 2. Auflage, Springer (2001) Hartmut Ehrig et al., Category Theory for Computer Scientists, Folien (2005) George M. Bergman, An Invitation to General Algebra and Universal Constructions (1998) Stanley N. Burris, H.P. Sankappanavar, A Course in Universal Algebra (1981)