DAAD-Procope Projekt

Methoden und Werkzeuge zur formalen Entwicklung komplexer Software mit TLA

Die temporale Logik TLA ist ein attraktiver und in mehreren Fallstudien erprobter Formalismus zur Beschreibung und Analyse reaktiver Systeme, für die auch bereits einzelne Werkzeuge wie Editoren, Simulatoren, Model Checker und Theorembeweiser entwickelt wurden. Jedoch mangelt es bisher an einer Integration dieser Werkzeuge durch einheitliche Konzepte und Schnittstellen, die dem Benutzer eine formal abgestützte Entwicklung auf adäquatem Niveau erlauben würden.

In diesem Projekt versuchen wir solche Konzepte zu entwickeln, wobei Abstraktions- und Strukturierungsmethoden eine zentrale Rolle spielen. Dabei interessieren wir uns besonders für diagrammatische Beschreibungstechniken, die in semiformalen Methoden weit verbreitet sind. Für temporallogische Spezifikationen und Beweise können Diagramme einerseits als verständliche Benutzerschnittstelle und andererseits als Schnittstelle zwischen interaktiven und automatischen Verifikationswerkzeugen Verwendung finden. Im einzelnen werden folgende Fragestellungen untersucht:

Anpassung diagrammatischer Notationen etwas aus UML zur Darstellung von TLA-Spezifikationen
Definition eines relativ vollständigen diagrammatischen Beweiskalüls für TLA-Spezifikationen
Einsatz von Techniken der abstrakten Interpretation zur Generierung von Diagrammen zu einer gegebenen Spezifikation, unter Verwendung benutzerdefinierter Regeln
Definition einer Verfeinerungsrelation zwischen Diagrammen und ihre Unterstützung durch Grapheditoren und interaktive Theorembeweiser

Projektpartner

Equipe Model, Laboratoire lorrain de recherche en informatique et ses applications (LORIA), Nancy

Prof. Dominique Méry
Dr. Dominique Cansell, Univ. Metz

LFE Programmierung und Softwaretechnik, Universität München

Projektlaufzeit

Beginn: Januar 1999
voraussichtliches Ende: Dezember 2001

Liste aller Projekte

Lehrstuhl

Institut

Universität

Stephan Merz

Last modified: Mon Mar 13 16:09:26 MET 2000