Paradigm Unifying System Specification Environments for proven Electronic design
The objective of PUSSEE is to introduce the formal proof of system properties throughout a modular system design methodology that integrates sub-systems co-verification with system refinement and reusability of virtual system components. This will be done by combining the UML and B languages to allow the verification of system specifications through the composition of proven sub-systems (in particular interfaces, using the VSIA/SLIF standard). The link of B with C, VHDL and SystemC will extend the correct-by-construction design process to lower system-on-chip (SoC) development stages. Prototype tools will be developed for the code generation from UML and B, and existing B verification tools will be extended to support IP reuse, according to the VSI Alliance work. The methodology and tools will be validated through the development of three industrial applications: a wireless mobile terminal, an IP encryption module for secure data transmission through internet and a network management module for automobiles.
Type: Normal Research Project
Themes: Design, Automation, Simulation and Optimisation, Formal Methods, Systems Engineering
Dates: 1st January 2002 to 31st December 2003
- University of Paderborn
- University of Southampton
You can edit the record for this project by visiting http://secure.ecs.soton.ac.uk/db/projects/editproj.php?project=95