The identicationof the deadlocks and attribute corruptionin the two initial
design proposals naturally leads to the suggestion of a third design proposal
whichresolvestheidentiedproblems. Inthissection wepresentsucha design
proposal based on the PWP approach which overcomes the problem with
at-tribute corruption. State space analysis of the rst two design proposals had
shownthatthestate spaceexplosionproblemprohibitedanalysisoflarger
con-gurations. It was therefore decidedto attempt to usea state space reduction
method in order to alleviate the state explosion problem when analysing the
third design proposal. It was decided to use the symmetry method [47,48]
since the owmeter system is made up of a number of identical components
(the modules, drivers, and CANAPPs) whose behaviour are identical.
More-over, the symmetry method is supported by the Design/CPN OE/OS Graph
Tool(OE/OS Tool) [26], and aswe willsee, themethod preservesthe
proper-tieswhich we want to verify. In this section we briey present the idea in the
modied design, and we then explain how it was analysed using state spaces
reducedbytaking advantage of thesymmetriesintheowmetersystem.
Thebasicideainthenewdesignproposalistointroduceapossibilityforthe
CANAPPs to send a negative response to a request message if the CANAPP
is currently waiting for a response to a previously sent request. Therefore, if
theCANAPPisnotintheprocessof performinga request whenthe incoming
requestarrives, itwillaccessthe attributeandsend apositive response. If the
CANAPPis intheprocess ofperforminga request, thenit willnotaccess the
attribute but instead send a negative response. This can be reected in the
CPN model by adding a place modelling a shared variable between the two
threadsof theCANAPP (see Fig. 7.5). Thisvariable can thenbe usedby the
threadhandlingtheincomingrequeststo decidewhetheritissafeto accessthe
attributes.
7.6.1 Symmetry Specication
Forcapturingthesymmetriesintheowmetersystemstatespaces with
permu-tationsymmetries (OS-graphsin[47])wereapplied. TheOE/OSToolsupports
state spaces with permutation symmetries based on user supplied symmetry
specications. This means that the user of the toolis requiredto provide the
permutation symmetries, and the tool then uses these as a basis for the
re-duction. A symmetry specication consists of assigning symmetry groups of
permutations to the atomic colour sets of the CPN model. An atomic colour
setisacoloursetdenedwithoutreferencetoothercoloursets. Thesymmetry
group determineshow the colours of the atomic colour sets are allowed to be
permuted, and in turn induces permutation symmetries on the markings and
the binding elements of the CPN model. The idea of state spaces with
per-mutationsymmetriesis to construct equivalenceclassesof markingswhichare
symmetric in the sense that they can be obtained from each other by one of
thepermutationsymmetries. Insteadof representingall markingsitsuÆces to
A similar remark applies to binding elements. In this way a condensed state
space is obtained which is typicallyorders of magnitudesmaller than the full
state space.
For the owmeter system the symmetry specication should capture the
symmetryintheCANAPPsaswellasinthemodules. Toillustratethe
symme-try specicationappliedfortheowmetersystem considerFig. 7.9. Figure 7.9
showstheinitialpartofthestatespaceforaowmetersystemconsistingoftwo
moduleseach containing two CANAPPs. CommunicationbetweenCANAPPs
in the same modulehas beendisabled forpresentation purposes. Node 1
cor-responds to the initial marking and has eight immediate successor nodes
cor-responding to thepossiblerequestswhichcan be initiatedinthe system(each
CANAPP can initiate a request to the two CANAPPs on the other module).
For node nwe willdenote thecorrespondingmarking M
n .
For the nodes 2, 3, 7, and 9 we have indicated in the associated dashed
box what communication has been initiated, e.g., node 9 corresponds to a
state of the system in which CANAPP
(1;1)
has initiated a request towards
CANAPP
(2;1)
. ThesymmetryspecicationisbasedontheobservationthatM
9
is symmetric to M
7
exceptfor a permutation which swaps thetwo CANAPPs
inModule
2
,Ina similarwayitcan beobserved thatM
2
can beobtained from
M
9
bya permutation which swaps thetwo modules, and M
3
can be obtained
from M
9
byapermutationwhich swapsthetwo modulesandwhichswapsthe
two CANAPPs inModule
2
. Furthermore,itis possibleto obtainM
4
by permutation of the CANAPPs and the modules. If such
symmetric markings aregrouped into equivalenceclasses, itis possibleto
rep-resent thisinitialfragment ofthefullstate space bythecondensed statespace
shown in Fig. 7.10. Here node 1 represents the equivalence class containing
theinitialmarkingonly,andnode2representstheequivalenceclasscontaining
the markings M
can be chosen as a representative
for this equivalence class. The successors of M
9
are grouped into equivalence
classes in a similar way. Altogether this means that the 65 markings which
can be reachedintwo steps from theinitial markingcan be representedusing
only8 nodesinthecondensed state space. In summary,the symmetry
speci-cation usedfor theowmeter systemallows permutationof CANAPPs within
the same module, and it allows permutation of modules containing the same
numberof CANAPPs.
Figure7.9: Initialfragment of thefullstate space.
9
2 1
1 2
1 2 1
3 4 5 6 7 8
2
Figure 7.10: Initialfragmentof thecondensed state space.
7.6.2 Consistency Check
Since theOE/OS Toolsupports user suppliedsymmetry specications,a
con-sistencycheck isneededtoensurethatthesymmetriessuppliedaresymmetries
which are actuallypresent inthe CPN model. This amountsto checkingthat
theinitialmarking, theguards, and thearcexpressions of theCPN modelare
symmetricin away preciselydenedin [47]. The currentlyreleasedversion of
theOE/OS Tool does notsupportan automatic check for consistency, but as
partof theproject we have developed an extensionof thetool which supports
a semi-automatic check for consistency. It is based on a combination of
syn-tacticaland semantical checks. The semantic checkis based on evaluating net
inscriptions in all possible bindings. As a consequence the semantic check is
time-consuming,buttogetherwith thesyntacticalcheckit ispossibleto make
a fully automatic check for consistency for the CPN model of the owmeter
system.
7.6.3 Analysis Results
The analysisfocuseson the same three properties asforthe two initial design
proposals. Forinvestigatingtheabsenceofdeadmarkingsabuilt-inquery
func-tionoftheOE/OSToolwasusedwhichliststheequivalenceclassescontaining
thereachable deadmarkings (if such equivalenceclasses exist). The query
re-lated to the absence of attribute corruption has to be modied to take into
account that the transition Indication corresponding to the reception of an
in-comingrequestcan nowoccurintwo modesdependingon whethertherequest
isaccepted orrejected. The modied query isshownbelowand is identical to
the original query except that it is onlyrequired that the Indication transition
doesnotoccurinabindingwheretherequestisaccepted,i.e.,thevariablemode
isboundto accept.
AG((Request;hcanapp=CANAPP
(i;j) i))
A((:(Indication;hcanapp=CANAPP
(i;j)
;mode=accepti)) U
(Conrm;hcanapp=CANAPP
(i;j) i))
Anotherproblemwhichhastoberesolvedwiththeabovequeryisthatitrefers
to occurrence sequences relatedto aspecic CANAPP.Since we allow
permu-tations of CANAPPs thisproperty is not a prioripreserved bythe symmetry
reduction. However, it was shown in [23,28] that symmetry reduction
pre-Table 7.3: Generationstatistics forfulland condensed state spaces.
Conguration FullStateSpace CondensedStateSpace Ratio Sym
Nodes Arcs Time T/N Nodes Arcs Time T/N
19,970 74,941 223 0.011 3,410 12,478 121 0.035 5.7 6
62,605 276,721 1,484 0.024 2,776 4,767 327 0.118 22.5 24
295,965 1,329,113 { { 37,156 166,316 4,123 0.111 7.9 8
319,337 1,460,785 { { 54,019 245,139 2,523 0.047 5.9 6
* 456,174 2,148,585 { { 114,370 537,857 7,428 0.065 3.9 4
* 44,470 190,995 544 0.012 2,971 11,075 197 0.066 14.9 24
* 578,376 2,746,401 { { 49,848 234,431 15,214 0.305 11.6 12
* 209,629 1,044,361 { { 4,759 18,699 1,438 0.302 44.0 120
propositionsare invariant under the permutation symmetries. The absence of
attributecorruptioncanthereforebechecked fromthesymmetryreducedstate
spacebycheckingthepropertyforaCANAPP
(i;j)
forwhichpermutationisnot
allowed. CANAPPswhichcannotbepermutedarepresent incongurationsof
theowmetersystemcontaininga modulewithasingleCANAPP.An
alterna-tive approachto thisis tostrengthenthesymmetryspecicationsuchthatthe
CANAPP inquestioncannotbe permuted.
Table 7.3 gives some statistical informationon the generation of the
con-densedstatespaceforsomeselectedrepresentativecongurations. For
compar-ison italsogivesthesizeofthefullstate space. Thesizeof thefullstatespace
hasbeencalculatedfrom thecondensed state space inthecases wherethe full
state space could not be generated given the available computingpower. The
Time columngivesthetimeinsecondsittooktogenerate thestate space. T/N
gives the processing time (in seconds) per node in the state space. The Ratio
givesthereductionobtainedinthenumberofnodes. ThecolumnSymgivesthe
number of permutation symmetries for the congurations, which is an upper
limitonthereductionwhichcanbeobtained. Thecondensedstatespaceswere
generated on aSunWorkstation with 512MB of memory.
Ascanbeseenfrom Table7.3, theuseof symmetriesyieldedsignicant
re-ductionsinthesizeofthestatespacesandallowedustoconsidercongurations
oftheowmetersystemwhichcouldnotbehandledwithfullstatespaces. This
is what we wouldhave expected. It is,however, also worth observingthat the
generationof condensed state spaceswas fasterthanthe generationofthe full
state spaces. Eventhoughweonlyhavethree observations,they indicatewhat
seems to be a general fact: the time that is lost on a more expensive test on
equivalenceofmarkingsandbindingelements,isaccountedforbyhavingfewer
nodesandarcs togenerate; and alsoto comparewithbefore anewnodeorarc
can beinserted inthestate space.
Wewereableto verifytheabsenceofreachabledeadmarkingsinall
cong-urationsfor which a condensedstate space could be generated. Moreover, the
ulecontaining a singleCANAPP.In additionto these properties we wereable
to verify that theinitial markingwasa home marking. This meansthat from
any reachable marking it is always possible to return to the initial marking.
Thisisavery attractive propertysinceitmeansthattheowmetersystemcan
never be brought in a situation in which the system cannot be made to
reen-ter its initial state. Moreover, it could be veried that the binding elements
corresponding to the initiation of a request, receptionof a response, handling
of a request, and transmission of a response were live. This means that all
CANAPPs in the system always have the possibility of completing requests
andhandling incomingrequests.