Japan Advanced Institute of Science and Technology

Japan Advanced Institute of Science and Technology

JAIST Repository

https://dspace.jaist.ac.jp/

Title

Author(s)

Citation

Issue Date

Type

Text version

URL

Rights

Description

for Object-Oriented Methodology

Itaru Ishida

Scho ol of Information Science,

Japan Advanced Institute of Science and Technology

February 13, 1998

Keywords: Object-oriented, Formal Model, Verication.

Recently,manydevelopmentmethodologiesareproposedfordevelopmentofhighqual-

ity software. Among them, object-oriented developmentis focused, and applied to many

practical system development. OMT is a typical example of Object-oriented methodolo-

gies. It prop oses an approach for analysing the system from the following three views:

(1) Object model for showing the system structure, (2) Dynamicmo del for specingbe-

havier of the system and (3) Functional model for describing data and control ows of

the system. Theseare analysismodel whichismodeloftargetsystem insystemanalizing

phaze of object-oriented develp oment. But, traditioanl Object-oriented methodologies

including OMT are not formal for system modeling. Thereforeit makesfor development

to b edicult for supp orting by computer.

As for these requirements, Aoki prop osed FO8M (Formal model for Object-oriented

Analysis Model). It provides theoretical basis for object-oriented methodology. FO8M

consists of Basic Models and Unied Model. Basic Models consist of models from three

viewsproposed inOMT, anddenedindependentlyeachother. Andthen,Unied Model

isdenedbyUniedMapping. UniedMappingisusedtodenethemapping correspons

to elements among each Basic Models. It helps us to support checking consistencies in

models, and to support using computer.

Inthispaper,forthepurposeofconstructingofVericationEnvironmentforanalysing

the model is dened by FO8M . This Verication Environment supports syntax checker

and prop erty vericationability for analysis model by FO8M.

Forthis reason, weimplementVericationFrameworkwhichallowsustoverifyprop-

erty of analysis model using FO8Mtheory, First, we re-struct FO8M theory implements

onVericationFrameworkanddecideitsimplementationpolicy. FO8Mtheory isdened

plural models. Eachmodel consists of data structure (identiersor expressionsetc,) and

Copyright c

1998byItaruIshida

policy ,we will dene the data structure for FO8M theory and property. Then We de-

ne to classify these denition to each model of FO8M model for distinction between a

denition inone model toin anothermo del.

HOL is used to implement Verication Framework. HOL is a verication system

implemented on ML language, which has exible data structure since it is based on

higher-order logic, treat theory mo dularly and allows external operating written in ML

languageifnecessary. Fromtheseabilities,wecandenecomplexdatastructureofFO8M

theoryandFO8Mmodelsindep endentlyusingmodularizedtheory,anddenesupporting

environmentinML language. Forthis reasonHOLhas go odproperty forconstructionof

Verication Framework foranalysis model inFO8M.

WewillmapdatastructuresofFO8Mtodatatyp einHOL,anditspropertytoaxiom

or theorem in HOL. For the purpose of modularization of each model of FO8M, these

denition of FO8M are classied and organized according to category of FO8Mmodels.

Asaresult ofthis, eachmo del theorycan beused asmodule. When weverify themodel,

we can use these theory asmodule.

Verication Framework has ability as follows: Syntax checking by mapping data s-

turucture of FO8M to typ e in HOL, checking. Consistency checkingby mapping model

propertyofittoaxiom andtheoreminHOL,Propertyoftargetsystemverication. Mo d-

el information is analysis model for target system written in FO8M theory in HOL. We

can show property verication using mo del information as assumption and verication

property written by logical term and FO8M theory. We will understand and inspect of

target system properties showingfrom it.

Forsystemanalysis using object-oriented development,itis veryimportantto under-

stand target system, and to construct analysis model correctly. Verication Framework

proposed in this paper provides mo del verication by syntax and consistency checking

for analysis model and supp orts us to understand the model property and consistency

guarantees by proofs.