Please help transcribe this video using our simple transcription tool. You need to be logged in to do so.


An ongoing effort within the community of verification and program analysis is to raise the level of abstraction in programming by automatic synthesis. In this paper, we demonstrate how our synthesis engine GAVS+ achieves this goal by automatically creating control code for the FESTO modular production system. The overall approach is model-driven: we reinterpret planning domain definition language (PDDL) (as a design contract) to model two-player games played between control and environment, such that users can describe (i) basic abilities of hardware components, including sensors (as environment moves) and actuators (as control moves), (ii) topologies how components are interconnected, and (iii) desired specification under a restricted class of linear temporal logic. The model is processed by our game-based synthesis engine, and from which intermediate code is generated. By mapping each behavioral-level action to a sequence of low-level PLC control commands, we transform the intermediate code to an executable program. The efficiency of our engine enables to synthesize every scenario presented in this paper within seconds. When the specification evolves, this implies a huge time-gain compared to manual code modification.

Questions and Answers

You need to be logged in to be able to post here.