An EFSM-based Framework for Designing and Verifying Embedded Software (EFFORT)

Starting date
January 1, 2008
Duration (months)
Computer Science, Department of Engineering for Innovation Medicine
Managers or local contacts
Fummi Franco
Information and communication technology, Embedded systems, Simulation

The project aims at developing a methodology, supported by tools, to enhance design and verification of embedded applications for configurable platforms. The methodology will rely on the extended finite state machine (EFSM) model and it will exploit SystemC as the reference language for modeling both the SW application and the HW peripherals included in the target platform.
A tool will be developed to automatically generate SystemC models of the EFSMs representing the embedded application. Such EFSMs will be automatically extracted from UML statecharts, and verified by using semi-formal techniques based on property checking and automatic generation of testbenches.
Then, HW components included in the target platform will be modeled in SystemC and simulated with the SystemC model of the SW application to check the functionality of the whole system by reusing testbenches and properties previously defined. Finally, C code will be semi-automatically generated from the SystemC model of the embedded application and it will be verified by exploiting a timing-accurate architecture simulator.
The effectiveness of the methodology will be demonstrated by modeling and verifying a real embedded application provided by STM Products.

The project aims at defining a design and validation framework for embedded applications. The effort has two main directions: scientific research and technological implementation. The project goals in the scientific research field are:
  1. introduction of the extended finite state machine (EFSM) model for modelling and verification of embedded SW;
  2. introduction of formal models and constraints into the EFSM-based design of embedded SW for the formalization and verification of requirement specification as a set of formal properties;
  3. definition of methodologies for functional verification of embedded SW by exploiting the TLM SystemC features;
  4. definition of methodologies for timing-accurate co-verification of embedded SW with models of the HW peripherals.
The project goal from the point of view of the technological implementation are:
  1. implementation of a front-end tool to extract the EFSM model from the UML design of the embedded SW and automatically generate the corresponding C/SystemC code;
  2. implementation of tools for the verification of the EFSM model against the formal specification;
  3. implementation of tools for functional simulation of the embedded application and automatic generation of a complete and optimized test suite;
  4. implementation of the a SystemC-based simulation model of the application's hardware peripherals;
  5. integration of the functional simulator with a HW architecture simulator (HSN), which models also temporal aspects, to execute and test the binary application software;
  6. execution of the automatically generated test suite on the HW/SW simulation platform, comparing the defect coverage performance against that of the traditional quality assurance process.


Funds: assigned and managed by the department
Syllabus: PROGATENEO - Progetti d'Ateneo
STM Products s.r.l.
Funds: assigned and managed by the department
Syllabus: PROGATENEO - Progetti d'Ateneo

Project participants

Nicola Bombieri
Full Professor
Franco Fummi
Full Professor
Cristina Marconcini
Graziano Pravadelli
Full Professor
Dino Puller
Research areas involved in the project
Sistemi ciberfisici
Embedded and cyber-physical systems


Research facilities