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

点击翻译按钮获取中文摘要

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.