Design and Analysis of Object-Oriented Programs

Project Overview. The ObjectCheck project defines methods and technologies for systems design that are aimed at avoiding implementation bugs. The key approach of the project is to couple design techniques with system verification. The design techniques propose software systems as executable object-oriented models specified using high-level design description languages (e.g., UML statecharts, etc. ). Verification is conducted by direct application of model checking-based analysis to program designs. The elements of the ObjectCheck approach are:

System designs are represented using an object-oriented executable specification language, xUML , that is in the mainstream of embedded systems development. xUML designs can be tested by execution using a discrete event simulator and translated into conventional programming languages such as C++.

Design methods (e.g., design for verification techniques ) for constructing components which enable the application of compositional reasoning to system designs.

Syntactic program transformation methods (e.g., loop abstraction ) to reduce the complexity of verifiable programs.

COSPAN model checker is applied to verify both liveness and safety specifications of the xUML system designs via automated mapping from xUML to the COSPAN input language.

Integrated space reduction uses both the COSPAN-built in techniques (e.g., partial order reduction, localization reduction, symbolic simulation, etc.) and xUML program partitioning (domain-specific program abstraction).