Semantics of Sequential Function Charts

Typ:	BA
Datum:	2018-03-01
Betreuer:	Alexander Weigl
Aushang:

Background

Automated production systems, such as industrial plants and assembly lines, are usually driven by Programmable Logic Controllers (PLCs). These computing devices are specially tailored to controlling automated production systems in mission- and safety-critical realtime environments. A malfunction may cause severe damage to the system itself or to the payload, or even harm persons within the reach of the system. They are worthy goal for formal verification.

Sequential Function Charts (SFC) are a graphical programming language (see right), that are defined by the IEC 61131-3 norm, and are heavily used to program the behaviour of aPSs. In the tradition of SFC's ancestor, Petri-nets and Grafcets, SFCs uses a similar model to automaton, but enriches by timing, (pseudo-parallel) code execution, transition guards.

Goal

The core of this thesis is to develop an efficient and correct transformation from SFC to the Model Checker. For this formal semantic definition of SFC needs to be recapitulated and clarified to catch up with the latest standard and vendor specifics. Also, SFC classes should be identified for which optimizations are possible.

Task

Your task is to define and implement translation of SFC into SMV model. This translation should (a) support a wide range of the SFC features, (b) be efficient for the verification. Part of the task is the formalization of undefined or unclear behaviour of the IEC 61131-3 or the vendor extensions.

Your Profile

Programming skills in Java are required. Furthermore, you should be interested in programming languages and Model Checking. You should have completed the Formal Methods (Formale Systeme) Course at KIT or equivalent.