Game Solving for Industrial Automation and Control

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, 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 into 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 program modification.