Semantic Assistance for Industrial Automation Based on Contracts and Verification

Dominik Hurnaus

Abstract

In the field of industrial automation end users often have the task of making changes and small adaptations to control programs of their machines. These end users (machine operators) usually lack software engineering expertise, yet they have to intervene in safety-critical, highly dependable systems where it is not possible to run any offline tests.

Verification is used to proof that specific properties of software systems hold in every possible execution of the system. This is in contrast to testing, which can only show that a property holds in a given situation with a defined input. For software verification it is necessary to formally describe these properties in contracts, containing possible call sequences and constraints on system states. Information of the intermediate steps of the verification process are stored with the software implementation to be reused later.

Semantic Assistance - a new concept introduced in this thesis - uses the results of a verification process to give guidance to end-user programmers. This guidance ranges from interactive assistance on valid routine calls to visualization of program states in form of a schematic view of the machine. In case of a contract violation, it is possible to automatically generate program repair proposals to eliminate the violation.

Verification and Semantic Assistance are integrated into the Monaco IDE, a system for creating control programs with the domain-specific language Monaco.

Case studies and evaluation results show that this approach is feasible for different types of control programs. Furthermore, we experienced that finding constraints of systems is not complex and checking these constraints statically removes substantial runtime overhead.

Kurzfassung

In der Industrieautomation müssen Endbenutzer oft kleinere Änderungen an Steuerungsprogrammen der Maschinen vornehmen. Diese Endbenutzer sind meist Maschinenbediener, die wenig bis gar keine Programmierkompetenz haben. Dennoch müssen sie in sicherheitskritsche Steuerungsprogramme eingreifen, bei denen Testläufe nicht möglich sind.

Der in dieser Arbeit beschriebene Ansatz wird basiert auf Verifikation von Steuerungsprogrammen. Mittels Verifikation wird bewiesen, dass ein Softwaresystem bestimmte Eigenschaften in jeder möglichen Ausführung einhält. Für die Verifikation von Software ist es notwendig, die gewünschten Eigenschaften der Software in Kontrakten zu beschreiben. Die Kontrakte, die in dieser Arbeit verwendet werden, beschreiben gültige Aufruffolgen und Einschränkungen.

Semantic Assistance - ein neues Konzept, das in dieser Arbeit vorgestellt wird - verwendet die Ergebnisse der Verifikation, um Endbenutzern bei der Programmierung zu helfen.Diese Hilfe umfasst interaktive Unterstützung bei Programmänderungen, Vorschläge gültiger Programmteile sowie Visualisierung von Zuständen von Maschinenkomponenten. Im Falle einer Verletzung der Kontrakte können automatische Programmänderungen vorgeschlagen werden, die die Programmfehler korrigieren.

Verifikation und Semantic Assistance wurden in die Entwicklungsumgebung der domänenspezifischen Sprache Monaco integriert.

Fallstudien zeigen, dass der Ansatz von Kontrakten und Semantic Assistance praktikabel ist. Darüber hinaus wurde festgestellt, dass Einschränkungen auf Monaco Systemen unkompliziert gefunden werden können und die statische Überprüfung dieser Einschränkungen die Laufzeitressource der Steuerungshardware entlasten.

PhD thesis, Johannes Kepler University Linz, Oktober 2009