PUSSEE Description

Access to the PUSSEE Leaflet

To satisfy a need for products of high reliability with short time-to-market., PUSSEE introduces two key aspects, reusability and formal proof of system properties. Reusability, although popular in the software world, is not yet usual in the domain of embedded systems because few design methods can integrate reusable sub-systems. The PUSSEE approach allows the reuse of existing components at various levels of the design. UML system specifications provide reusable system models through concepts like inheritance. Then virtual components, as defined in VSI Alliance, address reusability during later development stages.

The second important innovation introduced by PUSSEE, is the use of the B language for proving the properties of embedded system on chips (SoC). The formality of B complements the lack of formal semantics, which is the major drawback of UML. The two languages, jointly used to develop complex systems formally proven from the earliest design stage, allow to discover mistakes, inconsistencies or inefficiencies early enough to be fixed at minimum cost. Moreover, the reusability of B abstract machines at any level of refinement, with preservation of the integrity of the proven system specification, introduces a breakthrough in the reusability practice and paves the way to interface based design "a la" VSIA/SLIF.

A set of tools enabling a seamless use of the two languages will support the approach.

PUSSEE goals can be summarized as follows:

• Interface base design allowing sub-systems composition
• Definition of a synergy between UML and B
• Tool support throughout all stages of the system specifications refinement,
• Elaboration of reusable components for both system specification (reusable UML and B models) and system development (reusable virtual components)

The selected applications from the automotive and telecommunication domains will materialize the expectations of the participating system companies whose role is:

• Transferring the know-how and current trends from two highly demanding design domains.
• Learning the use of formal languages required for proven and reliable system development
• Contributing to integrate in the PUSSEE methodology their actual needs very accurately
• Assessing the applicability of this methodology through real industry cases.

The PUSSEE research activities will be guided and constrained by their actual needs.