Information Technology Reference
In-Depth Information
do so, i.e., a deadlock with respect to the game. In [8], we haveproposedand
implementedane
cientalgorithmforsolvingsuchagame.
Weillustratetheinputlanguageandthefunctionalitiesofthetoolwiththe
universityexamplepresentedinSection3.Wefistconsiderthepartoftheexam-
pleinwhichtheadministrationissplitintwoparts(seeFigure7).Wethushave
four implementations (
Machine, HalfAdm1, HalfAdm2, and Researcher
)andone
specification(
UniSpec
).Allofthesemachinescaneasilybedrawninthespeci-
ficationinterface.Inthequeryinterface,specificationsandimplementationsare
declared as follows:
specification: UniSpec
,and
implementation: HalfAdm1
.The
toolautomaticallyplaysasafety-gamefollowedbyapruninginordertoremove
locally inconsistent states. The tool also makes sure that the implementation
andthespecificationsatisfyDefinitions3and4.Ifthisisnotthecase,orifthe
specificationadmitnoimplementation,thenthetoolstops.
Wecombineimplementationswithcompositionandconjunctionoperatorsas
follows.Theinterfaceoftheadministrationistheconjunctionoftwointerfaces,
onespecifyingwhentooutputcoins(aftergrants)andtheotherwhentodelivera
patent(afterapublication).Thisisabetter(andlessrestrictiveapproach)than
to specify manually the combination of both. Then we compose the interfaces
oftheresearcher,theuniversity,andthemachine.Tocheckifthiscomposition
refinesouroriginalspecificationwecheckthefollowingquery
refinement: (Researcher || (HalfAdm1 && HalfAdm2) || Machine) <= UniSpec.
Figure 10 illustrates the different steps of the verification. The checker ex-
plores each component locally and prunes them from inconsistent states. The
resultsoftheexplorationofthetwo“half-administrations”areconjunctedand
pruned.Thenthethreeautomataarecomposedandpruned.Thesameisdone
forthespecificationandthenthesafety-gamealgorithmisusedtocheckwhether
refinementholds.Ifatanystepanautomatonturnstobeinconsistentthenthe
check stops and the tool reports the error to the user. In this latter case, the
user caninvokethe simulatorof
whichwill playthe gameuntil
itbreaksdown.Thisinformationcanbeusedtoimprove/changethedesignof
thespecificationoroftheimplementation.
Fortheaboveexample,itturnsoutthattherefinementdoesnothold.Thetool
revealsthatthe
UniSpec
interfacedoesnotallowpatentstobeproducedwithout
aprecedinggrant.However,thecompositionallowsresearcherstopublishwith
freetea,which isacceptedbythe conjunctionof the twohalfadministrations,
whichresultsinapatent.Ifwecheckinstead
Uppaal-tiga
refinement: (Researcher || Administration || Machine) <= UniSpec.
withtheadministrationofFigure2bthentherefinementholdsasmentionedin
Section 3 because this administration does not accept patents without grants
first.However,specifyingtheadministrationmanuallyexhibitsarestrictingbe-
haviourthatisnotpresentinthecleanerconjunctionofthetwosmallerspecifi-
cations.Heretherightcorrectionwouldbetoallowforfreepatentsin
UniSpec
.
Theconclusionisthattheusershouldnottrytomaketheconjunctionbyhand
anduseconjunctionstospecifymoreaccuratespecifications.
