Synthesis of discrete-event controllers from sequence-based specifications

As recognized by various engineering disciplines, formal models have the potential to support and speed up development of cyber-physical systems. They enable extensive functional and performance analysis of designs, including formal verification, and control code generation. There are two general approaches to application of formal models in engineering processes for the design of discrete-event controllers. Controllers are modeled, e.g. using sequence-based specifications, and, subsequently, verified against relevant system properties, such as the absence of blocking or the compliance to defined interfaces. Alternatively, from formal models of system components and requirements (finite automata and state-based expressions) non-blocking controllers are synthesized satisfying the requirements per definition. In both cases, models used are suitable for automatic code generation. This paper discusses lessons learned from the integrated application of these two approaches to an industrial case study. The experiment shows that they are complementary and that it is possible to combine them in one engineering process to mutual advantage.