Verifikation von Funktionsbausteinadaptern durch Modelchecking

摘要

Die Unified Modeling Language (UMt) gewinnt in der Automatisierungstechnik immer mehr an Bedeutung. In der Version 2.0 enthalt die UML so genannte "Ports", die unter anderem eine Integration der UML in ein stark heterogenes automatisierungstechnisches Umfeld erleichtern. Speziell zur Integration mit Sprachen fur speicherprogrammierbare Steuerungen wurden Ports der UML als Schnittstelle zu Funktionsbausteinen der IEC 61131 -3 eingesetzt. Die Umsetzung der unterschiedlichen Protokollarten erfolgt hierbei durch Funktionsbausteinadapter (FBAs). In diesem Artikel wird das logische, plattformunabhangige Verhalten von FBAs mit Hilfe kommunizierender endlicher Automaten beschrieben. Durch symbolisches Modelchecking wird dieses Automatenmodell anschliessend auf haufige Spezifikationsfehler uberpruft.