Thema mit Kurzbeschreibung der Thematik
In diesem Projekt werden die in der Praxis der Produktionsautomatisierung (PA) verwendete
Spezifikationssprache MFERT und visuelle Verhaltensbeschreibungen mit
formalen Mitteln der Spezifikation integriert. Hierdurch werden neue Techniken und
Methoden verfügbar, um PA-Systeme beim Entwurf und während der Laufzeit quantitativ und
qualitativ zu analysieren sowie Durchsatz, Sicherheit und Zuverlässigkeit solcher Systeme
zu steigern. Im Bereich Analyse konzentrieren sich die Aktivitäten auf die
Echtzeitverifikation mittels Modellprüfung. Der Antrag hat zum Ziel, die Akzeptanz
formaler Verifikationsverfahren zu erhöhen und sie stärker in den
ingenierwissenschaftlichen Entwurf von PA-Systemen einzubeziehen. Um dies zu erreichen, sollen automatisierte
und effiziente Beweisverfahren bereitgestellt werden. Der Spezifikationsprozess soll
dadurch erleichtert werden, dass die Formulierung nachzuweisender
Korrektheitseigenschaften statt mit komplexen temporallogischen Formeln durch intuitivere
Mittel erfolgt.
In den ersten zwei Jahren beschränkt sich das Projekt auf die Generierung einer
zentralen Steuerung und deren Spezifikation mittels zustandsorientierter Beschreibung.
In den weiteren Phasen wird der Ansatz zur Spezifikation autonomer Agenten zur
Generierung sich selbst konfigurierender, verteilter Steuerungen erweitert und aus den
Beispielen eine generelle Methodik entwickelt.