Abstract
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 language | English |
---|---|
Title of host publication | 54th IEEE Conference on Decision and Control (CDC 2015), Osaka, Japan, December 15-18, 2015 |
Place of Publication | Piscataway |
Publisher | Institute of Electrical and Electronics Engineers |
Pages | 3534-3541 |
Number of pages | 8 |
ISBN (Electronic) | 978-1-4799-7886-1 |
ISBN (Print) | 978-1-4799-7884-7 |
DOIs | |
Publication status | Published - 2015 |
Event | 54th IEEE Conference on Decision and Control (CDC 2015) - "Osaka International Convention Center", Osaka, Japan Duration: 15 Dec 2015 → 18 Dec 2015 Conference number: 54 http://www.cdc2015.ctrl.titech.ac.jp/ |
Conference
Conference | 54th IEEE Conference on Decision and Control (CDC 2015) |
---|---|
Abbreviated title | CDC 2015 |
Country/Territory | Japan |
City | Osaka |
Period | 15/12/15 → 18/12/15 |
Internet address |