Methodologies for Specification of Real-Time Systems Using Timed I/O Automata - Formal Methods for Components and Objects - page 297

Researcher

tea?

Administration2

a) b)

Stuck

A B

Idle

x>15 tea?

grant? z=0 z<=2 cof?

pub?

pub? x>=2

grant?

x<=15 x=0 pub!

pub!

patent! coin!

cof? tea?

pub?

x=0 x=0 pub!

D

x=0

C

z=0 pub?

Coffee Tea

x>=4

z<=2

grant? grant?

x<=4 x<=8

pub

grant patent pub coin

tea cof

Fig. 3. Specificationsforthea) Researcher andb) Administration2

Administration || Machine || Researcher

≤

UniSpec

Stepwise refinement

UniSpec

Administration2 || Machine || Researcher

≤

Fig. 4. One possible step in Top-down development: Modifying a component and
recheckingrefinement

Machine (Figure 1a) will then in turn provide the Researcher (Figure 3a) with
coffeeandteasothattheresearchercanproducepublications.The Administration
componentalsohastheresponsibilityofconvertingpublicationsintopatents.
ThetoplineinFigure4showsasuccessfulrefinementcheckwhichshowsthat
thethreecomponentstogetherrefinetheoverallspecification.
ThebottompartofFigure4showsanadditionalstepintherefinementpro-
cess. Here a single component is updated ( Administration to Administration2 ).
Thisnewversion(Figure3b)differsinasingletransition.Ifitreceivesapubli-
cation(pub?)intheinitial,leftmoststate,thenitwillnotloopbutinsteadshift
to the lower left state indicating that it is ready to output a patent based on
thispublication.Thisnewversionoftheadministrationisthusableto receive
andprocessfreepublicationsthatithasnotpayedfor.
Figure4showsthattherefinementcheckfailsafterthisupdateofthemodel.
Bytheindependentimplementabilitypropertythiscouldalsohavebeendiscov-
ered by checking whether Administration2 refines Administration , which indeed
it does not. This might come as a surprise to the developer as it seems like
a reasonableimprovementto be ableto acceptfreepublications.We defer the
discussionofhowtosolvethisissuetoSection5.
In stepwise refinement this step of decomposing and refining individual
componentsisappliediteratively,untilasuitablelevelofdetailisreached.

Bottom-upSynthesis. Theseconddevelopmentmethodologythatourframework
supportsisabottom-updevelopmentprocessthrough stepwisecomposition .Here
weassumethatactualimplementationsofsomecomponentsalreadyexistand