Program Synthesis from Generalised Test Tables
| Forschungsthema: | Improve APS, PLC Verification, Synthesis |
|---|---|
| Typ: | MA / PdF |
| Datum: | 2018-09-03 |
| 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. They are worthy goal for formal methods.
Generalised Test Tables are a table-based specification developed at the chair of Prof. Beckert. They arise from the concrete test table and preserve their comprehensibility although extended expressiveness.
Program synthesis is the generation of software that adheres a given specification. In contrast to formal verification, where a given software is checked for conformance against a specification.
Goal & Task
In this thesis, we want to develop a practicable method for the synthesis of PLC software from a set of Generalised Test Tables.
Your Profile
Programming skills in Java/Kotlin are required. Furthermore, you should be interested in programming languages, formal methods, and theory of infinite games and automaton. You should have completed the Formal Methods (Formale Systeme) Course at KIT or equivalent.
References
Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser and Alexander Weigl. Generalised Test Tables -- A Practical Specification Language for Reactive Systems. iFM 2017.