Automatic Synthesis of Reactive Programs From Formal Specifications

Details
Category: Research
Last Updated on Monday, 26 November 2012 16:20

Given a formal model of the environment with which a reactive system will interact it is possible to use model checking techniques to automatically synthesize the C code implementing the reactive system itself. This can be done by looking at the reactive program as a universal plan. This, besides the advantage of correct-by-construction automatic code generation, also allows early validation and verification of requirements. Our work on this subject can be found in [ICINCO-ICSO 2006, Informatics in Control Automation and Robotics 2008, ICAS 2007, HASE 1999, ASE 1999, ICFEM 1998, CDC 1997, CDC 1996].