Unvollständige automatische Verifikation von Software-Designmodellen für nebenläufige objektorientierte eingebettete Echtzeitsysteme basierend auf dem Paradigma der erweiterten kommunizierenden Zustandsautomaten

Description

Das korrekte Funktionieren von Softwaresystemen ist ein zentrales Anliegen in informationstechnologisch orietierten Gesellschaften. Dies bezieht sich besonders auf die sich ständig weiter verbreitenden eingebetteten technischen Systemen, wie sie z.B. in Automobilen, Flugzeugen oder medizin-technischen Systemen enthalten sind. Dies sind häufig als asynchrone nebenläufige Systeme konzipiert in denen autonome Software-Akteure mit Hilfe asynchronen Nachrichtenaustauschs miteinander kommunizieren und sich synchronisieren. Durch den hohen Grad an Nichtdeterminismus, der diese Systeme auszeichnet, ist es unmöglich, die Korrektheit der Synchronisation und des Gesamtverhaltens manuell zu ermitteln, weswegen automatisierte und durch Computer unterstützte Analysemethoden für die dem System zugrunde liegenden Entwurfsmodelle essentiell sind. Das vielen dieser Systeme zugrunde liegende Berechnungsmodell ist das der kommunizierenden erweiterten hierarchischen Zustandsmaschinen für welche viele Eigenschaften unentscheidbar sind. Dies bedeutet, dass es für sie kein allgemeines Lösungsverfahren gibt. Dennoch kann es für spezielle gegebene Modelle unvollständige Entscheidungsmechanismen geben. Das Ziel dieses Projekts ist es, solch unvollständige, automatische Entscheidungsverfahren für die o.g. Modelle zu entwickeln. Im Mittelpunkt des Projekts steht die Entwicklung von Abstraktionstechniken, die es erlauben, eine Übersetzung in ganzzahlige lineare Programmierungsmodelle durchzuführen, die dann zur Definition unvollständiger Eigenschaftsüberprüfungen verwendet werden können.

Institutions
  • FB Informatik und Informationswissenschaft
Funding sources
Name Project no. Description Period
Deutsche Forschungsgemeinschaft609/07no information
Further information
Period: 01.04.2007 – 31.03.2009