Formale und methodische Integration von graphischer Spezifikation und Echtzeitverifikation im Entwurf komplexer Produktionsautomatisierungssysteme

• Applicant: Professor Dr.-Ing. Wilhelm Dangelmaier
• Subject Area: Theoretical Computer Science
• Term: from 1998 to 2003
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5135340

Ziel dieses Projektes ist die Nutzbarmachung von formalen Verifikationstechniken im ingenieursmäßigen Entwurf von Produktionsautomatisierungssystemen (PA-Systemen). Die formale Verifikation von PA-Systemen dient dazu, bereits in frühen Entwurfsphasen und auf hohen Abstraktionsebenen Entwurfsfehler aufzuspüren. Ein besonderer Schwerpunkt liegt auf der Verifikation und Modellierung von Zeiteigenschaften. Zu diesem Zweck sollen formale Methoden wie quantitative temporale Logiken oder zeiterweiterte endliche Automaten, die als Basis der formalen Verifikation dienen, mit Hilfe von graphischen und natürlichsprachlichen Methoden in den Entwurfsablauf integriert werden. Als Ergebnis soll eine prototypische Entwurfsumge-bung implementiert werden, die von der Spezifikation über die Verifikation und Analyse bis hin zur Unterstützung bei der Fehlersuche alle Facetten des Designs von PA-Anlagen abdeckt. 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. Der Antrag hat zum Ziel, die Akzeptanz formaler Verifikationsverfahren in ingenieurwissenschaftlichen Anwendungsfeldern zu erhöhen und sie stärker in Kombination mit der Simulation in den ingenieurwissenschaftlichen Entwurf von PA-Systemen einzubeziehen.

• DFG Programme: Priority Programmes
• Subproject of: SPP 1064: Integration von Techniken der Softwarespezifikation für ingenieurwissenschaftliche Anwendungen
• Participating Person: Professor Dr. Wolfgang Müller