Controller Synthesis: From Modelling to Enactment

Víctor Braberman, Nicolás D'Ippolito, Nir Piterman, Daniel Sykes, and Sebastián Uchitel

Universidad de Buenos Aires, Argentina; Imperial College London, UK; University of Leicester, UK

Track: Formal Tool Demonstrations
Session: Formal Demonstrations 2
Controller synthesis provides an automated means to produce architecture-level behaviour models that are enacted by a composition of lower-level software components, ensuring correct behaviour. Such controllers ensure that goals are satisfied for any model-consistent environment behaviour. This paper presents a tool for developing environment models, synthesising controllers efficiently, and enacting those controllers using a composition of existing third-party components. Video: