Development of Verifiable Programs - Application of an Approach Based on Executable Object-Oriented Specifications

Natasha Sharygina, James C. Browne and Delbert Tesar .

This paper presents the first phase of a two phase approach for development of object-oriented software systems which combines validation of OOA models formulated in xUML (an executable subset of UML) with formal verification through model checking.

Published as a Technical Report TR-02-16 of the Computer Science Department of the University of Texas at Austin.