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

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

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.