Modellprüfung für den Entwurf von Fertigungssteuerungssystemen

In diesem Artikel stellen wir die Anwendung von Modellprüfung für ein Fertigungssystem mit freifahrenden Transportfahrzeugen vor. Dabei konzentrieren wir uns darauf, den Materialfluss in einem Systemmodell auf die Einhaltung quantitativer und zeitlicher Bedingungen hin zu überprüfen. Zur Modellentwicklung setzen wir die graphische Beschreibungsmethode MFERT ein, die sich bereits mehrfach in Industrieprojekten bewährt hat. Wir präsentieren eine Abbildung von MFERT in zeitannotierte Zustandsübergangssysteme, die für ein bereits existierendes Werkzeug zur Modellprüfung als Eingabe einer Modellbeschreibung dienen. Bei der Modellprüfung wird diese Beschreibung auf die Einhaltung von Eigenschaften überprüft, die in einer temporalen Logik oder einer davon abstrahierten Form spezifiziert werden.