This section describes how the two design proposals based on the PWP and
the IWP approaches have been analysed by means of state spaces and the
Design/CPNOccurrenceGraphTool(OGTool)[26]. Thissectionalsopresents
the modicationsmade to the CPN modelin order to make itsuited forstate
space analysis, it states thegoals of theanalysis, and it presentsthe obtained
results.
To make the CPN modelsuited for state space analysis some adjustments
were needed. Essentially two modications of the CPN model were made.
The modellingofthe attributesinthe CANAPPswassimpliedsuch thatthe
concretevaluesoftheattributeswerenolongermodelled. Thissimplicationis
justiedsince nopartsof theCPN model make choicesdependingon concrete
values of the attributes. When the concrete values of the attributes are not
modelled, then the read and write messages become similarsince their eect
is no longermodelled. The Broadcast and Event messages were not considered.
Handling these messages in the context of state space analysis would require
moreextensivemodicationstotheCPNmodelinordertoobtainaCPNmodel
with a nitestate space. It was therefore decidedto leave these two kinds of
messagesout.
7.5.1 Analysis Goals
Theprimarygoalofthestatespaceanalysiswastoinvestigatewhetherthetwo
designproposalsfullledthethree requirements statedintheend ofSect. 7.3.
The rst step in order to investigate thiswas to translate them into dynamic
propertiesof theCPN model. Thismakes itpossibleto formulate the
require-ments as queries in the OG Tool. The answers to the queries can then be
automatically determinedbythe OGToolwhen a state space hasbeen
gener-ated. Belowwe showhowto translateeach ofthe threepropertiesinto queries
Absence of Deadlocks.
Thispropertycan beformulatedastheabsence ofreachabledead markings in
the CPN model. A dead marking is a marking without enabled transitions,
and it is an example of a standard dynamic property of a CPN model. The
OGToolhasabuilt-instandardqueryfunctionListDeadMarkings,whichliststhe
reachable deadmarkings (ifsuch markingsexist).
Absence of Attribute Corruption.
WhenaCANAPPhasinitiatedarequest itisnotallowedto starthandlingan
incoming request before the request has been completed, i.e., a response has
beenreceived. Thispropertycannoteasilybeformulatedasastandarddynamic
propertyof theCPN model. However, itcan beconvenientlyformulatedusing
temporallogic [22]. The OGToollibrary ASK-CTL [26] makesit possibleto
makequeriesformulatedinastateandactionorientedvariantofCTL[13]. That
theattributes cannot be corrupted for a given CANAPP
(i;j)
can be expressed
asthefollowingaction-based CTLformula. An explanation isgiven below.
AG((Request;hcanapp=CANAPP
(i;j) i))
A((:(Indication;hcanapp=CANAPP
(i;j)
i))U(Conrm;hcanapp=CANAPP
(i;j) i))
Theformulastatesthatwhenever(denotedAG)thetransitionRequestoccursina
bindingcorrespondingtoCANAPP
(i;j)
,theninallfutures(denotedA)the
tran-sitionIndication cannot occurin abinding corresponding to CANAPP
(i;j) until
(denotedU) the transition Conrm hasoccurred ina binding corresponding to
CANAPP
(i;j)
. Anoccurrence ofthetransitionRequestinabinding
correspond-ing to CANAPP
(i;j)
has been written as (Request;hcanapp =CANAPP
(i;j) i).
Thebindingof IndicationandConrmiswrittenina similarway. Anoccurrence
of thetransition Request(see Fig. 7.6)modelsthestart ofa request, an
occur-renceof transition Indication modelsthe startof handlingan incomingrequest,
andan occurrence oftransition Conrm(seeFig. 7.6)modelsthereceptionofa
response.
Topology Independence.
Thetwo propertiesabove shouldbevalidforthesystemindependentlyof how
the CANAPPs are placed in the modules in the system. This property can
thereforebeinvestigatedbyanalysingdierent congurationsof theowmeter
system. Investigating dierent congurations can be donebysimply changing
the initial marking of the CPN model. Hence, topology independence can be
investigatedbyconstructing state spacesfordierent initialmarkings.
7.5.2 Analysis Results
Statespaceshavebeenconstructedforanumberofcongurationsofthe
owme-tersystem. Table7.2 givessome statisticalinformationon thestate spacesfor
Table 7.2: Generation statisticsforfullstate spaces.
Conguration WP Nodes Arcs Time
PWP 37 73 1
IWP 6 5 1
PWP 1,299 4,189 7
IWP 14 13 1
PWP 19,770 74,941 223
IWP 11,451 37,513 109
PWP 37,825 146,721 1,499
* IWP 2,266 4,841 15
PWP 133 281 1
IWP 80 133 1
PWP 5,581 18,707 44
IWP 446 869 1
PWP 62,605 276,721 1,484
IWP 26 25 1
PWP 44,470 190,945 544
* IWP 3,866 8,473 33
question. We have useda graphicalnotationto indicatetheconguration
con-sidered. For instance, the second row in the right-most part of Table 2 gives
statistics for a conguration with two modules with one and two CANAPPs,
respectively. TheWPcolumnshows whichwaitpointapproachwasconsidered.
The Nodes and Arcs columns give the number of nodes and arcs in the state
space,respectively. TheTimecolumngivesthetimeinsecondsittookto
gener-atethestate space. AllstatespacesweregeneratedonaSunWorkstationwith
512 MBofmemory. It isworthobservingthattheIWPapproachgivessmaller
state spaces thanthe PWP approach. The reasonfor this is that inthe IWP
approachtheCANAPPsblockaftertransmissionofamessage,andhencethere
is less concurrency between the CANAPPs compared to the PWP approach.
With the available computing power and due to the state explosion problem,
it was not possible to construct the full state space for large congurations
in the PWP approach. Therefore, in some of the congurations only external
communication (communication between CANAPPs located in dierent
mod-ules) is analysed. An asterisk () indicatesthat onlyexternal communication
is analysed in the given conguration. However, even the analysis of small
congurations of the owmeter system showed that neither of the two design
alternatives satisestherequiredproperties.
In all the congurations considered, the analysis revealed that the design
based on theIWP approach had several deadlocks. Below we will concentrate
on a specic deadlock situation found in the analysis of the IWP approach.
Figure7.7: Visualisationof apathleading to adeadlock.
two moduleseach withtwo CANAPPs. Figure 7.7visualisesapath/execution
leading to a dead marking of the CPN model. This marking was identied
usingthequery functionListDeadMarkings followed bytheuse of anotherquery
functionwhich isable to ndone oftheshortestpaths (occurrence sequences)
inthestatespaceleadingfromtheinitialmarkingtoaspeciedmarking. Once
such an occurrence sequence has been found, it is straightforward to visualise
itusingMSCs. The MSCinFig.7.7 shows thefollowingsequence ofevents.
1. CANAPP
(1;2)
sendsaWriteRequesttoCANAPP
(2;2)
. Asthemodelisbased
on theIWPapproach bothCANAPP
(1;1)
and CANAPP
(1;2)
are blocked
untila WriteResponseis received.
2. CANAPP
(2;1)
sendsa WriteRequest to CANAPP
(1;1)
. Both CANAPP
(2;1)
and CANAPP
(2;2)
are blocked untilaWriteResponseisreceived.
3-10. ThemessagesaresentovertheCAN.AlloftheCANAPPsinthe
owme-tersystemareblocked. Thus,neitherCANAPP
(1;1)
norCANAPP
(2;2) can
receive theWriteRequests,and adeadlockhasoccurred.
Alldeadlocks are of course unwanted, but especially the kind of deadlock
vi-sualised inFig. 7.7 is problematicin a owmeter system. The reason is that
itshould be possible to distributethe CANAPPs freely in themodulesin the
system and the concrete location of the CANAPPs should not aect the
cor-rectnessof thesystem. IfCANAPP
(2;2)
intheexampleaboveinstead isplaced
in a separate module (if the owmeter system consisted of three modules
in-stead of two) no deadlock would occur for the above communication pattern.
The above also illustratestopology independence as a non-trivial property of
theowmetersystem. Analysis ofthePWPapproach showed thatnoneof the
congurations analysedhad anynodes corresponding to deadmarkings of the
CPN model. Therefore, all the congurations analysed inthe PWP approach
Figure7.8: Visualisationof apathleading to corruptionofan attribute.
Theanalysisoftheowmetersystemregardingtheabsenceofattribute
cor-ruptionshowedthatallcongurationsanalysedfortheIWPapproachfullthis
property. However, theanalysisinthecase ofthe PWPapproachshowed that
thisapproachdoesnotfulltheproperty. Figure7.8visualisesapath/execution
to a node inthe state space representing a marking inwhichan attributehas
beencorrupted. Thecongurationoftheowmetersystemconsideredconsists
oftwomoduleseachwithoneCANAPP.TheMSCshowsthefollowingsequence
of events.
1. CANAPP
(1;1)
sendsaWriteRequestto writean attributeof CANAPP
(2;1) .
CANAPP
(1;1)
nowwaitsforaresponse butisnotblocked.
2. CANAPP
(2;1)
sendsaWriteRequestto writean attributeof CANAPP
(1;1) .
3-10. The messages and corresponding acknowledgements are sent over the
CAN.
11. CANAPP
(1;1)
receives theWriteRequest message from CANAPP
(2;1) .
12. CANAPP
(1;1)
changesitsattributesaccordingtothevalueintheWriteRequest
from CANAPP
(2;1)
. A corruptionhasoccurred.
To summarise the results of the analysis: the design based on the IWP
approachviolatestherstproperty(absenceofdeadlocks)butfullsthesecond
(absence of attributecorruption). The designbased on thePWP approach on
theotherhandfullstherstpropertybutviolatesthesecond. Thus,neitherof
thetwodesignproposalsaresuitableforanalimplementationoftheowmeter
system. In the next section we will consider a variant of the PWP approach