Model Checking Support for xUML
The basic model checking support for executable object-oriented software system designs specified in xUML can be summarized as follow:
Integrated State Space Reduction Framework
To alleviate the state space explosion problem, a general framework for integrated state space reduction in model checking executable object-oriented software system designs, has been established. The framework structures the application of state space reduction algorithms into three phases with different algorithms applied in each phase. The interactions between these algorithms are explored to maximize the aggregate effect of state space reduction. Automation support for the framework has been proposed and partially implemented. The framework is presented for system designs modeled in xUML, but can also be used to structure integrated state space reduction for other representations. To further improve the applicability of the framework, domain-specific design patterns can be explored to instantiate the framework for different application domains. An instantiation~\cite{XB:02} of the framework for distributed transaction systems has been defined and its partial implementation has been applied to the design model of an online ticket sale system. The dimension of software system designs that are model checkable was found to be greatly extended.
Verification of Component-based Software Systems
We have proposed an approach to integrating model checking into the
CBD of software systems. In this approach, temporal properties of a
software component are specified, verified, and packaged with the component.
Selection of a component for reuse considers not only its functionality,
but also its temporal properties. When a component is composed from simpler
components, temporal properties of the composed component are model checked
on its abstraction constructed based on the composition and the properties
of its sub-components. Model checking enhances the reliability of software
systems constructed with CBD and the compositional structures of these
systems significantly reduce the complexities of model checking. This approach
has been applied to enhance the reliability of run-time images of TinyOS
[HS:00], a component-based run-time environment for networked sensors.
Future work
The ObjectCheck project provides a testbed for new model translation techniques, state space reduction algorithms, and software development approaches. More state space reduction algorithms will be included to enhance its model checking capabilities and more case studies on developing reliable software systems will be conducted to validate its existing capabilities.
References
[HH:96] R. H. Hardin and Z. Har'El and R. P. Kurshan, COSPAN, Proc. of CAV'96, 1996.
[HS:00] J. Hill and R. Szewczyk and A. Woo and S. Hollar and D. Culler and K. Pister, System Architecture Directions for Networked Sensors, Proc. of ASPLOS-IX, 2000.
[XLB:01] F. Xie, V. Levin and J. C. Browne "Model Checking for an Executable Subset of UML", Proceeding of 16th IEEE International Conference on Automated Software Engineering, November 2001
[XB:02] . Xie and J. C. Browne, "Integrated State Space Reduction for Model Checking Executable Object-Oriented Software Designs", Proceeding of the 5th International Conference on Fundamental Approach to Software Engineering, April 2002.
[XLB:02] F. Xie, V. Levin, and J. C. Browne, "ObjectCheck: A Model Checking Tool for Executable Object-oriented Software System Designs", Proceeding of the 5th International Conference on Fundamental Approach to Software Engineering, April 2002.
Note: A pdf version
of the abstract is available here.