techniques for tackling the problem of fragmentation experienced during model checking of real-time systems with
hughly varying time-scales, e.g. in verification of the run-time behaviour of LEGO Mindstorms programs.
for Coloured Petri Nets
?
GuyEdwardGallasch 1
,Lars MichaelKristensen 1
,and Thomas Mailund 2
1
ComputerSystemsEngineeringCentre
UniversityofSouthAustralia
MawsonLakesCampus,SA5095,AUSTRALIA
Email:guy.gallasch@postgrads.unisa. edu.a u,lars.kristensen@unisa.edu.au
2
DepartmentofComputerScience,UniversityofAarhus
IT-parken,Aabogade34, DK-8200AarhusN,DENMARK
Email:mailund@daimi.au.dk
Abstract. Thebasicideaofthesweep-linestatespacemethodistoexploita
formal notion of progress foundin manyconcurrent and distributed systems.
Exploiting progress makes it possible to sweep through the state space of a
CP-net while storing only a small fragment of the states in memory at any
time.Propertiesofthesystemcanthenbeveriedon-the-yduringthesweep
of thestate space.This canlead to signicant savings inpeakmemory usage
andcomputation time.Examples ofsystemspossessingprogress aretransport
protocols,transactionsprotocols,workowmodels,andsystemsmodelledwith
TimedCP-nets.WepresentSweep/CPN,alibraryextensiontoDesign/CPN
supportingthesweep-linemethod,anddemonstrateitsuse.
Keywords:Statespace methods,Stateexplosionproblem,extensions to
De-sign/CPN,Vericationandvalidation.
1 Introduction
State space explorationand analysis is a powerful way to investigate the
cor-rectnessof distributedand concurrent systems,andis oneof themainanalysis
methods for Coloured Petri Nets (CP-nets or CPNs) [11,12]. The basic idea
behindstatespaceexplorationistoconstruct adirected graph(calledthestate
space,orthereachability/occurrencegraph)representingallreachablestatesof
the system and the transitions between these states. From this graph a large
number of dynamic properties of the system can be analysed algorithmically.
Themaindrawbackofusingstatespacesforanalysisofsystemsisthestate
ex-plosionproblem: even forsystemsofmoderatecomplexitythenumberof
reach-able states can be astronomical, and storing the state space in the available
computermemory mightnotbe feasible.
In an attempt to alleviate the state explosion problem a number of state
spacereductionmethodsandtechniqueshavebeendeveloped.Thesetechniques
canbesplitintothree mainclasses. Therst arethosemethodsthatrepresent
thestate space in acompact orcondensed form.Symmetry reduction[4,5,13]
isan exampleof this,wherea representative state is usedto represent a setof
symmetricstates.Thesecondclassofmethodsrepresentonlyasubsetofthefull
state space. Such methods include partialorder reduction methods [17,20,21]
?
SupportedbyanAustralianResearchCouncil(ARC)DiscoveryGrant(DP0210524).
stored. The reduction is done in such a way that the answers to verication
questions can stillbe determinedfrom thereducedstate space.
Thethirdclassofreductiontechniquesinvolvedeletingstatesorstate
infor-mationduringstate spaceexploration. Suchmethodsincludehash-compaction
[18,22] andbit-state hashing[8,9]inwhicha hash-valueis calculatedfromthe
state andonlythehash-value{nottheentirestate{ isstored.Thestatespace
cachingmethod[6,10], isanothermethodbasedondeletinginformationduring
exploration. State space caching exploits thefactthat duringa depth-rst
ex-plorationof thestatespace, onlythestates onthedepth-rststackneedto be
storedtoensuretermination.Statesnotonthestackcanbedeletedonce
mem-ory becomes scarce without compromising the termination of the state space
exploration.
The sweep-line method [3,15] is a state space method belonging to the
third category. It is aimed at systems for whichthe notion of progresscan be
formalised as a progress measure mapping from markings to a set of ordered
progress values. The sweep-line method uses the progress values on markings
to determine which states can safely be deleted. Progress measures provide a
conservative estimate of reachability: For a marking to be reachable from the
set of unprocessed markings, it would have to have a progress value larger
than at least one of the unprocessed markings. Markings with progress value
smallerthanallunprocessedmarkingscanthereforesafelybedeletedwhilestill
guaranteeingterminationofthestatespaceexploration.Progressmeasureswill
often bespecic to thesystemunder consideration, such assequence numbers
and retransmission counters in communicationprotocols, and the controlow
of the system. However in some instances a progress measure can be dened
based onthemodellinglanguageitself,and suchprogress measuresthenapply
to all modelsof systemsconstructedusingthismodellinglanguage. Theglobal
clockrepresentingtimeinTimedColouredPetriNets[12]isanexampleofone
such progressmeasure. The sweep-line method was used in [7] for verication
oftransactionsintheWirelessApplicationProtocol(WAP)withareductionin
peak memoryusage to 20%. The use of the sweep-linemethod on Timed
CP-nets wasstudied in[2].The sweep-linemethodis nottied to CP-nets,butcan
beappliedtoallmodellinglanguageswherestatespacemethodsareapplicable.
The contribution of this paper is to study the sweep-line method in the
contextofCP-nets,andtopresentSweep/CPN[16],alibraryextensiontothe
Design/CPN state space tool [1] implementing the basic sweep-line method
from [3] for CP-nets. Consequently there is a shift in the focus of the paper,
fromatheoreticalintroductiontothesweep-linemethodtoadescriptionofthe
Sweep/CPN implementation,whichcouldberegarded asa highlevelmanual
forpractitioners.
Therestofthispaperisorganisedasfollows.Section2introducesthe
stop-and-wait protocol which we will use as a running example throughout this
paper. Section 3 gives the necessary background information on state spaces
for CP-nets,whileSect. 4 and 5 present thesweep-line methodand the
appli-cation of Sweep/CPN to the stop-and-wait protocol. Section 6 presents the
set of generic state space exploration functions availablefor verication using
tionscan be specialised for the verication of standard dynamicproperties of
CP-nets. Finally, in Sect. 8 we sum up with a conclusion and discuss future
work.
2 The Stop-and-wait Communication Protocol
Tointroducethesweep-linemethodanddemonstrate theuseof Sweep/CPN,
we will use a simplecommunication protocol as a running example. The
pro-tocolunder considerationis a stop-and-wait communicationprotocol from the
datalinkcontrollayerof theOSI (Open SystemsInterconnection)network
ar-chitecture.TheCPNmodelofthestop-and-waitprotocolistakenfrom[14].The
stop-and-wait protocol is not a sophisticated protocol, however it is
interest-ingenoughtodeservecloserinvestigation,andcomplexenoughtodemonstrate
the use of Sweep/CPN. In this paper we only explain the part of the CPN
model necessary to understand the application of Sweep/CPN. A complete
descriptionof theCPN model canbe foundin[14].
Figure 1 shows the prime page of the CPN model. The system consists
of a Sender (left) transmitting data packets to a Receiver (right) across a
bi-directionalCommunicationChannel(bottom).Thepacketstobetransmittedare
storedin a Send buerat thesender side, and the packets received by the
re-ceiverarestoredinaReceivedbuer.TheCommunicationChannelisunreliable,
which means that loss and overtaking is possible, however for simplicity only
lossisconsideredinthis example.The datapackets intheSend buerhave to
be delivered over the communicationchannel exactly once, and in the correct
order,to the Received buer. A stop-and-wait strategy is employed to achieve
this, whereby the sender will send a data packet and continue to retransmit
thesame datapacket untila matching acknowledgement is received, at which
pointthenext datapacketcan betransmitted.The numberof retransmissions
of a datapacket allowed by thisstop-and-waitprotocol is unbounded for
sim-plicity.Inorder to make theCPN modeltractableforstate spaceanalysis, the
buersbetweenthesender,receiver,andcommunicationchannel(TransmitData,
ReceiveAck, TransmitAck, ReceiveData) have been modelled with a maximum
capacity of one packet each. This still allows for unbounded retransmissions,
whilstensuring thestate space willbe nite.
3 State Spaces of CP-nets
Inthissectionwebrieyrecallthebasicideasoffullstatespaceexplorationfor
CP-nets [12]. The state space of a CP-net can be characterised as a directed
graphG=(V;E),whereV =[M
0
i(thesetofnodesormarkingsreachablefrom
theinitialmarkingM
0
),andE =f(M;(t;b);M 0
)2VBEV jM[(t;b)iM 0
g,
i.e.,thereisanarc(M;(t;b);M 0
)inthestate spaceifthebindingelement(t;b)
(belongingto thesetof allbindingelementsBE)is enabledinthemarking M
andits occurrence leadsto themarkingM 0
.