Derivation and Hardware-in-the-loop Testing for a Road Tunnel Controller

Developing supervisory controllers for cyber-physical systems is a difficult and error-prone process. The formal method of supervisor synthesis allows engineers to obtain a correct-by-construction supervisor from a model of the plant and a model of the requirements. Validation, however, remains an important step in this design process. Model simulation is often used as a first validation method, but this lacks aspects related to the execution of the supervisor such as the operating semantics and interfaces with external subsystems. To incorporate these aspects, hardware-in-the-loop (HIL) simulation is used. This paper describes the process of deriving an implementable controller from a synthesized supervisor, implementing it in a HIL setup, and validating it using HIL tests. Specifically, the paper focuses on the design of resource controllers, a relaxation in the confluence check for implementable controllers, and the process of automatically generating and optimizing PLC code. Furthermore, a real-life case study is presented in which a supervisory controller is derived and implemented for the Swalmen tunnel.