Prude

The main objective of this project was to define a framework and associated tools for the development of object-oriented software systems in a rigorous and precise way.

Problem

The recent evolution of application areas such as the Internet and mobile communication systems has placed the software community in front of new challenges. Some of the new demands such as the ability to make the World Wide Web more interactive and to turn Web documents into compound documents with active multimedia content, have started to have a good response. Among them, the definition of distributed software architectures such as the Common Object Broker Request Architecture (CORBA) and of compound document frameworks such as the Object Linking and Embedding architecture (OLE).

Some important aspects of object technology such as testing and security issues are still in infancy, and therefore need to be worked out in order to consolidate the use of object technology. Rigor and precision are urgent in the area of object technology since by promoting reusability it may contribute to the propagation of bugs and flaws among several systems.

Solution

Our approach to improve rigor and precision in object technology design consists of using formal methods. Formal methods provide notations for writing precise and rigorous specifications, and mechanisms for checking that the final system corresponds accurately to what was intended in the initial requirements. Their main drawback is their esoterism, which represents a huge barrier for their whole scale utilization. In order to overcome this limitation, we have decided to combine them with existing graphical object-oriented notations, which are easy to learn and use, and for which industrial strength tools are available. More specifically, we use the Unified Modeling Language (UML) as graphical object-oriented notation and the Prototype Verification System – Specification Language (PVS-SL) as formal notation. In order to achieve our main objective, which was to develop a framework that can be used in industry and for large and complex systems, we based ourselves on the following principles:

• Hide the formal “stuff” behind the graphical ones– that is achieved by using the formal notation (PVS-SL) as semantics foundation of the graphical one (UML).
• Automate the framework as much as possible–that is achieved by using existing tools and by providing complementary tools when needed.

The main outcome of the project consists of the formalization of the essential models of the UML such as statecharts and sequence diagrams, and of developing a software verification and validation environment named PruDE. The PrUDE environment provides support for consistency-checking, model-checking, proof-checking, and testing. Model-checking and proof-checking are based on the PVS toolkit. The automation of proof-checking is enhanced by selecting and customizing suitable proof strategies provided by the PVS toolkit. The interface of PrUDE with UML is based on XMI, which provides an explicit interchange format for UML based tools. Since all UML tools export the UML model in XMI format, the PrUDE platform is independent of any tool vendors. The main strength of PrUDE relies on the fact that a typical user will have to deal only with graphical notations, which are friendly, easy to learn and to use. Most of the formal “stuff” (related to PVS) are processed at the back end.

People

• Dr. Issa Traore, Coordinator
• Dr. Demissie Aredo, Investigator
• Mr Michael Yanguo Liu, Investigator
• Mr Hong Ye, Investigator