Full Title: Correct-by-Construction Design of Embedded and Cyber-Physical Systems

ForSyDe (Formal System Design) is a design methodology targeting the design of heterogeneous embed- ded and cyber-physical systems, envisioning a correct-by-construction design flow. The idea of ForSyDe is to combine a formal base in form of analyzable models of computation (MoCs) with predictable platforms that can give service guarantees. ForSyDe supports several MoCs in form of modeling libraries and also provides tools for design space exploration and hardware synthesis.

Although ForSyDe has from the beginning been designed to facilitate formal verification, so far ForSyDe has made only very limited use of formal verification techniques to support a correct-by-construction de- sign process. This project is a pre-study aiming to identify how formal verification techniques can be integrated into ForSyDe to further support a correct-by-construction design process.

The project is a pre-study, which shall give preliminary answers to several research questions. Based on the result of this seed project, the goal is to formulate a larger project that integrates suitable verification techniques into ForSyDe.



Scope: Design Methodology for Embedded Systems
Funding: CASTOR
Timeline: 2019
Main KTH Staff Involved: Ingo Sander, Dilian Gurov
Other Partners: SAAB