Proving the power of Synthesis Based Engineering on the TNO-ESI Demo system

This project investigates the application of Synthesis-Based Engineering (SBE) to the TNO Embedded Systems Innovation (TNO-ESI) demo system, a modular cyber-physical training factory. The objective is to demonstrate the power of SBE in the development of industrial control software by automatically synthesizing correct-by-construction supervisory controllers from formal specifications. To evaluate the applicability and expressive power of SBE, four demonstration scenarios are developed. These demonstrations focus on system functionality: a single-product workflow scenario, coordinated two-product handling, a step-by-step scenario that swaps two products, and a demonstration that again swaps two products, but only the desired outcome is specified, while the synthesis algorithm autonomously determines how this action happens. These demonstrations validate the correctness of the synthesized controller under increasing system complexity and illustrate how SBE supports systematic extension of system behavior by modifying specifications rather than control code. They also demonstrate how SBE enables the realization of complex behavior with minimal engineering effort while preserving correctness guarantees by construction. The project consists of work across the SBE workflow, including system and requirements modeling using formal specification languages, synthesis of supervisory controllers, visualization of system behavior and synthesized controllers and code generation for deployment on the physical TNO-ESI demo system. This application demonstrates SBE as a viable approach for developing reliable industrial control systems with reduced manual programming effort and built-in correctness guarantees.