The scale of software products is becoming lager as a result of the rapid progress and increasing use of computer systems. Object-oriented methodologies have been proposed for the development of such systems [1-4]. In an object-oriented development method, a target system is organized into its abstract image consisting of its constituent atoms called objects. These methodologies reduce the complexity of the system drastically. However, even with the use of such methodologies it is still difficult to validate the system and to ensure high reliability. In the past, developers relied on careful development using formal methods [9,10]. Formal methods are too complex and not enough mature to be directly applied to large-scale system development. We proposed a formal model [12,13] based on OMT which is applied to many practical system developments. Using the proposed model, we can formally verify detailed properties of the target system. However, complex steps must be followed in order to prove the system properties. These complex steps could generate errors due to human imperfections and misunderstanding resulting in lower system reliability. Computer support to mechanically prove properties without human intervention is needed. In this paper, we show how to support such verifications using the HOL theorem prover [11].
