Integrierte algorithmische und deduktive Verifikation verteilter Steuerungssysteme für hybride Prozesse

• Antragsteller: Professor Dr.-Ing. Stefan Kowalewski
• Fachliche Zuordnung: Automatisierungstechnik, Mechatronik, Regelungssysteme, Intelligente Technische Systeme, Robotik
• Förderung: Förderung von 1999 bis 2002
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5166876

Das Ziel des Projektes ist die Entwicklung einer Methodik zur Verifikation verteilter, diskreter Steuerungssysteme für kontinuierliche oder hybride Prozesse, die die Grenzen der bisher realisierten, nur auf algorithmischen Analyseverfahren beruhenden Ansätzen überwinden soll. Zu diesem Zweck wird die Verifikation in lokale Untersuchungen auf der Teilsteuerungsebene und eine globale Untersuchung des Gesamtsystems aufgeteilt. Im ersten Fall soll weiterhin algorithmisch überprüft werden. Um dies zu erleichtern, wird ein Ansatz zur Reduzierung von Hybriden Automaten durch Diskretisierung entwickelt. Bei der Überprüfung von Anforderungen an das Gesamtsystem soll deduktiv vorgegangen werden. Dazu wird das kompositionale "Assumption/Commitment" - Beweisverfahren auf Hybride Automaten erweitert, die über diskrete und kontinuierliche Signale verkoppelt sind. Beide Ebenen der Verifikation werden in einem Beweis-Manager integriert.

• DFG-Verfahren: Schwerpunktprogramme
• Teilprojekt zu: SPP 1016: Analyse und Synthese kontinuierlich-diskreter technischer Systeme (KONDISK)
• Beteiligte Personen: Professor Dr.-Ing. Sebastian Engell; Professor Dr. Willem-Paul de Roever