Synthesis of discrete-event controllers from sequence-based specifications

Thijs Janssen, Joanna van de Mortel - Fronczak, Emile van Gerwen, Michel A. Reniers

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)
1 Downloads (Pure)


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.
Original languageEnglish
Title of host publication54th IEEE Conference on Decision and Control (CDC 2015), Osaka, Japan, December 15-18, 2015
Place of PublicationPiscataway
PublisherInstitute of Electrical and Electronics Engineers
Number of pages8
ISBN (Electronic)978-1-4799-7886-1
ISBN (Print)978-1-4799-7884-7
Publication statusPublished - 2015
Event54th IEEE Conference on Decision and Control (CDC 2015) - "Osaka International Convention Center", Osaka, Japan
Duration: 15 Dec 201518 Dec 2015
Conference number: 54


Conference54th IEEE Conference on Decision and Control (CDC 2015)
Abbreviated titleCDC 2015
Internet address


Dive into the research topics of 'Synthesis of discrete-event controllers from sequence-based specifications'. Together they form a unique fingerprint.

Cite this