COCONUT - A correct-by Construction Workbench for Design and Verification of Embedded Systems

Starting date
January 1, 2008
Duration (months)
30
Departments
Computer Science, Department of Engineering for Innovation Medicine
Managers or local contacts
Fummi Franco
URL
http://coconut-project.edalab.it/

Design and verification of modern embedded platforms are two highly related problems which are still mainly addressed by using unrelated methodologies. This effectively reduces development productivity and complicates achieving predictable system properties.

The COCONUT project thus focuses on the definition of a formal framework based on a tight integration of design and verification through all refinement steps of an embedded platform design flow, from specifications to logic synthesis and software compilation. In particular, it is intended to propose a modelling and verification flow to enhance and speed-up embedded platform design and configuration with particular regard to application fields related to mixed continuous/discrete models, like for example networked multimedia and sensor network managing.
In this context, the main activities of COCONUT will be related to the definition of innovative methodologies and tools to:

* define and validate properties that represent the design specification;
* automatically synthesize properties into code;
* map models between hybrid and discrete domains;
* provide correct-by-construction abstraction/refinement processes;
* perform post-refinement verification.

Such activities will be implemented in a set of tools working on more that one abstraction level whose correctness will be formally proved.

Sponsors:

Unione Europea
Funds: assigned and managed by the department
Syllabus: EUROPA - Progetti Europei

Project participants

Luca Geretti
Temporary Assistant Professor
Valerio Guarnieri
Graziano Pravadelli
Full Professor
Tiziano Villa
Professore onorario
Sara Vinco

Activities

Research facilities

Share