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

Model in CafeOBJ

Nobutoshi Umehara

School of Information Science,

Japan Advanced Institute of Science and Technology

February 13, 1998

keywords:

B-Technology,internalconsistency,hidden algebra, renement,projection

Abstract

We verify the consistency of B Abstract Machine specication in CafeOBJ. We pro-

pose a guideline for descriptions of formal specications of large systems that are based

onalgebraic specication techniques.

Recently, software is getting larger and more complex. Therefore, software engineers

are facedwiththe dicultytodescribethe targetsystemscorrectly. Formalmethodsare

available to solve this problem. The formal methods are based on mathematically tech-

niques for the describing system prop erties. The Z,VDM, B-Technology (hereafter,'B')

are famous as formal specication languages in model-oriented. The OBJ, CafeOBJ are

also famous as in property-oriented. The model oriented formal specication languages

are used to describe sp ecications. They use the concrete primitives, for example, set,

list, and function. In contrast, the property oriented formal specication languages are

used to describe sp ecications. They use axioms that represent required prop erties of

specications. In these formal languages, However,B gainedsupport from develop ers to

adopt techniquesfor the specication, designof software componentsknown suchas Ab-

stractMachine,objectbasedapproach,CaseStudies,etc. Now,thereare varioussystems

that we can treat as the states and their operations. The Abstract Machine consists of

the states and their operations. An object based approachis easy to understand for the

develop ers. The Case Studies on B is useful rather than on the other formal metho ds.

The B-Technology consists ofthe Abstract Machine Notation,the B-Method and the B-

Toolkit 1

. The B-Method is a methodology to pro of internal consistency of the Abstract

Machine and the Renement (which rened Abstract Machine). This method provides

specications which contain no error. The B-To olkit supports this method in various

0

Copyright c

1998byNobutoshiUmehara

1

TheBToolkitisa trademarkofB-Core (UK)Ltd.

techniques of sp ecication development.

The CafeOBJis a formal specication language based on many sorted algebra, order

sorted algebra, hidden algebra and rewriting logic. CafeOBJ can naturallycop e with ab-

stractdatatyp es. Itcopeswithrespectivelydataandoperationsofthedatawithsortand

sorted functions. Therefore,CafeOBJ can copewith an object as a unit of sp ecication.

The concepts of rewriting logic and hidden algebra give the user the ability to describ e

object based sp ecications. CafeOBJ has also a feature as an executable language. We

can prove the sp ecication automatically using CafeOBJ. These features are similar to

B. More over, CafeOBJ has many techniques such as projection and renement. These

points contributeto reduceverication steps.

1 The First Stage

Wemustconsider how toexpress the Abstract Machine toobtain specication has wide

applicability. Some features in the Abstract MachineNotation are the variables, the in-

variant,the constantsandthe setsfor describingthe state. Some featuresareparameters

and pre-condition for describing the operations. Other features are sees, uses, includes

and renement forstructuring specications.

We provide a basic table to convert the Abstract Machine which consists of the above

features to a specication in CafeOBJ. Then we considerthe conversion of import com-

mands of the Abstract Machine in practical sense. Since the operations clauses of B

specication can deal with various internalstates without declaration,we cannot obtain

the accurateinformation ofthe aectionofthe operationsontheinternalstates. Tohan-

dlethisproblem,weproposeaguidelinerecommendstosetanewsorttoaninternalstate.

2 Second Stage

We can use formal methods to describe a sp ecication of safety critical system. This

meansformalmethodsprovideushighreliability. The B-Methodprescribeshowtocheck

the specication for consistency. The pro of for internal consistency is 1)parameter exis-

tence, 2)constants and sets existence, 3)non-emptiness of machine state, 4)initialisation

and 5)invariant preservation. We make an equivalent proof in CafeOBJ with a proof

provided in B-Metho d.

The Renement is the pro cess from high abstract specications to low abstract ones

(concretesp ecications). Usingrenement,wecanpreservethepropertiesofspecications

basedonthebehaviours. Theproofforrenementconsistencyis1)non-emptinessofjoint

state, 2)initialisation renement and 3)operationrenement.

The Renement on CafeOBJ needs signature map and pro of that satisfy equations

dened inabstractspecication. Wemakealso aproof of this in CafeOBJ.

B supp orts Case Studies for training. The following lift system is one of them.

We describeabstract specications of this lift system. The rst specication issingle

liftforpersonaluse. The secondoneisasingleliftfor personalusewith moreoperations.

Weprovideapro ofscoreusingtheexecutablefeatureofCafeOBJ.Thisproofshowsacor-

rectnessof renement usingabovetwosp ecications. The primary pointof this example

isthatoperationrenementisthemapfromoneabstractoperationtocompositionalcon-

creteoperations. Weexplain this comp ositionof operationstouse derivedoperator. The

proof of this renement is to prove that the concrete specication preserves all mapped

equations.

The third one is a multi-lift. We describe a multi-lift specication by comp osing the

above single lift specications. The Projection is a useful methodology for describing

concurrent systems. The projection operator is a map from the multi-lift system to the

singleliftsystems. Thismulti-liftsystemisaconcurrentsystemwithoutsynchronization.

Using projection op erator,wecan givea simple vericationonthe multi-lift system. We

verify that the execution order of two operationsthat generate transitions makes no in-

uence with regard to the behaviour. This verication is based on hidden algebra. By

using hidden algebra, we can specify encapsulated objects, and can handle behavioural

specication.

The above specications are part of the whole specication of the lift system. We

described the whole specication inCafeOBJ actually.

4 Conclusion

Weselected B torefer the techniques describing specication in this research.

We can summarize our work asthe follows.

1) We considered how to describe B Abstract Machine specication in CafeOBJ. 2)

We made a useful reference table to transform B into CafeOBJ. 3) We proposed to use

newsortforrepresentinternalstate,toobtaintheaccurateinformation oftheoperations.

4)Weshowedproofscoresforinternalconsistencyandrenementconsistencyof CafeOBJ

specications. 5)Wealso showedapossibilityofsimple vericationtouse theconcepts of

renementand projection by using examples such aslift systems.

An algebraic specication is a suitablespecication for describing objects whichcon-

sist of state and their operations. Then the abstraction of sp ecications is useful for

vericationin required aspect of behaviours. Weshoweda parallelproperty of operation

onthemulti-liftexample,but this systemhas nosynchronization. CafeOBJis alsobased

on rewrite logic. Thus we can cop e with concurrency and non-deterministic choice by

using rewritelogic. Our future workis to verifythe abovesystems.