Project Oveview:

The ObjectCheck project is developing methods and technologies to enable effective and practical model checking on substantial software systems. The significant elements of the ObjectCheck approach which enable model checking to be both effective and practical for substantial software systems are:

• The representation for the software systems is an object-oriented executable specification language, xUML, which is in the mainstream of software development for embedded systems.  xUML can be tested by execution using a discrete event simulator and translated into conventional procedural programming systems such as C+++.  xUML is supported by standard commercial software systems.
• Design methods for constructing components which enable the application of compositional reasoning to software systems.
• The design-level specifications of software system in xUML, together with the properties to be modeled, are translated into the S/R language and model checking is conducted by COSPAN.  The error track is translated back to the software representation.
• We have developed procedures for integration of model checking into component-oriented development of software systems.
• We have established compositional reasoning rules on xUML semantics which enable effective model checking through compositional development.

	Introduction		People
	Publications		Useful Addresses
	Presentations and Demos		New Additions to This Page

You are the No.  visitor to the ObjectCheck project website since the last counter reset on Oct. 22, 2002.

Maintained by Fei Xie. Last modification on Nov 12, 2003.