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.

Partners

• Volvo
• Nokia
• Intracom
• KeesDA
• University of Paderborn
• ClearSy
• University of Southampton

Funding

• EU

Principal Investigators

• Professor Michael J Butler

Other Investigators

• Dr Colin F Snook