SigAbort Start
Wait s
Restart_ns Restart_nf
Fail_n Test
Success_n Test
AbortAll [#flg va=false orelse #flg vc=false]
DoneAll
CommitAll
[#flg va=true andalso #flg vc=true]
Synced Sync
Sync
VoteA Vote P In SigAbort_
n Wait P In
VoteNA Vote P I/O NotKilled
Wait s
P Ou Wait Abort Wait P In
Killed Wait P In
LocDone_
n Done P In Start_n Task
1‘{tsk=task(1),flg=true}++
1‘{tsk=task(2),flg=true}
P Ou
Voted_n Voted P In NoIntTasks
Wait P In
n‘sy
sy
1‘va++1‘vc
te
te te
te te
1‘da++1‘dc sy
n‘dw
sy
1‘va++1‘vc aa
aa ab
vt ab
vt
vt ca
ca
init_task init_task
Fig.5.CPNmodelofController
TheHomeProperties showthatitispossibletoreachanymarkingfromany
othermarkingintheO-graph.TheLivenessProperties showtherearenoDead
Markings. Some of the Fairness Properties of the O-graph are shown below.
Only Arrnis Impartialwhich impliesthat repeatedcycles ofthe wholegraph
requireoccurenceofofringofthisnode.
Liveness Properties Fairness Properties
--- --
---Dead Markings: None Control'AbortAll 1 Fair
Live Transitions Instances: Control'CommitAll 1 Fair
Control'AbortAll 1 Control'Restart_nf 1 Fair
Control'CommitAll 1 Control'Restart_ns 1 Fair
Control'Restart_nf 1 Control'SigAbort 1 Fair
Control'Restart_ns 1 Control'Sync 1 Fair
Control'SigAbort 1 Tasks'Arr_n 1 Impartial
Control'Sync 1 Tasks'Done_n 1 Just
...
Thefollowingareexamplesofthetestingof morespecicproperties
formu-latedasQueries toO-graphanditsnodes.Thesequeriesarebasedonfunctions
that aredenedinML.
FunctionSuccess testsallmarkingsinwhichtheSuccess nnodeisactive.
Afunction Fail canbedenedin asimilarmanner.
Function
-fun Success_ (s: Test) : Node list
= PredAllNodes (fn n =>
cf(s, Mark.Control'Success_n 1 n) > 0);
-- - --
---Thefollowingtestscanberun usingthesefunctions:
Test Result
--- ---- --- --
---Success_(s); val it = [29] : Node list
Fail_(s); val it = [63] : Node list
Success_(s) <> Fail_(s); val it = true : bool
length(Success_(s))+length(Fa il_( s))=2 ; val it = true : bool
--- ---- --- ---
---This means that Success and Fail do occur, that they cannot occur
si-multaneously, and that there can be onlyone of each. All these results are as
expected.
Wecantest forspecic occurrencesof theSuccess nnode(node 29)to be
activated. It shows that there are only twopossibleoccurrences that canlead
tothishappening,i.e.onefromVotedcausingCommitall(node60)orDoneall
(node20).
Functions and Tests Result
--- ---- --- ---
---Success_(s); val it = [29] : Node list
InNodes(29); val it = [60,20] : Node list
OutNodes(60);OutNodes(20); val it = [29] : Node list
val it = [29] : Node list
--- ---- --- ---
---Stateoroccurrence60representstransitionCommitAllbeingactivatedwhich
leadstoSuccessn.Stateoroccurrence20representstransition DoneAllbeing
activatedwhichalsoleadstoSuccess n.There arenoothersuchoccurrences.
numberofTasksisincreased.
---Size of Occurence Graph with number of Tasks
---|Tasks| Nodes Arcs |Tasks| Nodes Arcs
---2 63 114 5 7568 25883
3 298 689 6 39331 158444
4 1481 4220 7 207667 969677
---5 Conclusion
We have shown that a relatively complicated Ada program using tasking can
be modelled and veried using Petri nets (ordinary P/T nets and Coloured)
and Model Checking.This signicantlyimprovescondence in thecorrectness
ofhigher-levelabstractionsuchasatomicactions.
Thispaperis apreliminaryattempt in pursuingourchosendirection of
re-search, in which we would like to develop amorecomprehensivemethodology
forverifyinghigh-integritysystemsbuiltofAtomicActionsandimplementedin
Ada95.
The majornew aspects of this work, which also reveal the potentially
ex-ploitableadvantagesofthePetrinetapproachovertheStateMachineone[10],
are:
{ Renementofbothstatesandtransitions;
{ Analysisof behaviouratthetrueconcurrencyandcausalitylevel;
{ High-levelaspectsofmodelling,suchasparametrisation,arepossibleusing
high-levelPetrinets.
Forexample,ifrenementwith threads(e.g., task spawning),recursiveatomic
actions,etc.werepossibleinthemodelledsystems,thenPetrinetswouldprovide
amuch moreeÆcientwayofmodellingthanstatemachines.
Wehaveonlyshownwaysofmodellinginteractionmechanismsatthe
seman-tical level.Part of theintendedfuture workwouldbeto developnew methods
ofextractingPetrinetsfromtheAda95syntax.
Althoughthis paperhas notintroduced real-time issues, thechoice of tool
andmodellingtechniqueimpliesthat theapproachcanbeextended toatimed
Petrinetapproach.
References
1. Ada 95: Information technology - Programming languages -Ada. Language and
StandardLibraries.ISO/IEC8652:1995(E), Intermetrics,Inc.,1995.
Methods inVerication. G.Holzmann,D. Peled,V. Pratt (eds),Am.Math. Soc.
(1997)305-328.
3. E.BestandB.Grahlmann:PEP-morethanaPetriNetTool.Proc.ofToolsand
Al-gorithmsfortheConstructionandAnalysisofSystems,2ndInternationalWorkshop,
TACAS'96,Passau,March1996,T.Margaria,B.Steen(eds).Springer-Verlag,
Lec-tureNotesinComputerScience1055,Springer-Verlag(1996)397-401.
4. E.Best, R.Devillers, J.Hall: The Petri Box Calculus: a New Causal Algebra with
Multilabel Communication.Advances inPetri Nets 1992, Lecture Notes in
Com-puterScience609,Springer-Verlag(1992)21-69.
5. E.Best, R.Devillers,and M.Koutny:Petri Nets,Process Algebrasand Concurrent
ProgrammingLanguages.LecturesonPetriNetsII:Applications,AdvancesinPetri
Nets.LectureNotesinComputerScience1492,Springer-Verlag(1998)1-84.
6. E.Best,H.Fleischhack,W.Fraczak,R.P.Hopkins,H.KlaudelandE.Pelz:M-nets:An
AlgebraofHigh-levelPetriNets,withanApplicationtotheSemanticsofConcurrent
ProgrammingLanguages.ActaInformatica35(1998)813-857.
7. R.E.Bryant: Symbolic Boolean Manipulation with Ordered Binary-decision
Dia-grams.ACMComputingSurveys24(1992)293-318.
8. D.Buchs,C.BuardandP.Racloz:ModellingandValidationofTaskswithAlgebraic
Structured Nets. Proc. of Adain Europe'95, LectureNotes in ComputerScience
1031, Springer-Verlag(1995)284-297.
9. A.BurnsandA.J.Wellings:Real-TimeSystemsandProgrammingLanguages
(Sec-ondedition)AddisonWesley(1996).
10. A.BurnsandA.J.Wellings:HowtoVerifyConcurrentAdaPrograms-The
Appli-cationofModelChecking.AdaLetters,VolumeXIX,Number2(1999)78-83.
11. R.H.Campbell and B.Randell: Error Recovery in Asynchronous Systems. IEEE
Transactions onSoftwareEngineering SE-12(1986)811-826.
12. E.M.ClarkeandE.A.Emerson:Synthesisofsynchronizationskeletonsfor
branch-ing time temporal logic. In Dexter Kozen, editor, Logic of Programs: Workshop,
LNCS, vol.131,Springer-Verlag,1981.
13. E.M.ClarkeandJ.Wing:FormalMethods:StateoftheArtandFutureDirections.
Report,CarnegieMellonUniversity(June1996).
14. J.Esparza:ModelCheckingBasedonBranchingProcesses.ScienceofComp.Prog.
23, 151-195(1994).
15. R.K. Gedela and S.M. Shatz. Modeling of advancedtasking in Ada-95: a Petri
netperspective.Proc.2-ndInt.WorkshoponSoftwareEngineeringforParalleland
DistributedSystems(PDSE'97),Boston,MA,pp.4-14(May1997).
16. P.Godefroid and P.Wolper:A Partial Approachto ModelChecking.Information
andComputation,110(2),305-326(1994).
17. K.Jensen:ColouredPetriNets.BasicConcepts.EATCSMonographsonTheoretical
ComputerScience(1992).
18. K.H.Kim: Approaches to Mechanization of the Conversation Scheme Based on
Monitors.IEEETransactionsonSoftwareEngineeringSE-8(1982)189-197.
19. D.B.Lomet:ProcessStructuring,SynchronisationandRecoveryusingAtomic
Ac-tions.Proc.ofACMConferenceLanguageDesignforReliableSoftware.SIGPLAN
(1977)128-137.
20. PED.http://www-dssz.Informatik.TU -Cott bus. DE/~w wwds sz/{thehomepage
ofPED(aHierachicalPetriNetEditor).
21. D. Peled:Combining Partial Order Reductions with On-the-y Model-checking.
FormalMethodsinSystemsdesign8(1),39-64(1996).
homepageofPEP(aProgrammingEnvironmentBasedofPetriNets).
23. M. Pezze,R.N.TaylorandM.Young:GraphModelsforReachabilityAnalysisof
ConcurrentPrograms.ACMTransactionsonSoftwareEngineering and
Methodol-ogy4/2(April1995)171-213.
24. B. Randell:SystemStructureforSoftware FaultTolerance.IEEETrans.on
Soft-wareEngineering1(2) 220-232(1975).
25. B.Randell,P.LeeandP.Treleaven:Reliabilityissuesincomputingsystemsdesign.
ACM ComputingSurveys10(2):123-165(1978).
26. W.Reisig: PetriNets. An Introduction. Springer-Verlag, EATCS Monographson
TheoreticalComputerScienceVol.3,(1985).
27. S. Roch and P.H. Starke: INA: Integrated Net Analyzer, Version 2.2, Manual
Humboldt-UniveritatzuBerlin,InstututfurInformatik,April1999.
28. S.M. Shatz,S.Tu,T. Murataand S.Duri: An Application of PetriNet
Reduc-tionfor AdaTasking DeadlockAnalysis.IEEETrans.onParallelandDistributed
Systems7(12),1309-1324 (December1996).
29. S.K.Shrivastava,G.N.DixonandG.D.Parrington:AnOverviewoftheArjuna
Dis-tributedProgrammingSystem.IEEESoftware8(1991)66-73.
30. S.Tu,S.M.ShatzandT.Murata:TheoryandApplicationofPetriNetReductionfor
Ada-TaskingFeadlock Analysis.TR91-15,EECS Dept.,Univ.ofIllinois,Chicago
(1991).
31. A.Valmari:TheStateExplosionProblem.LecturesonPetriNetsII:Applications,
AdvancesinPetriNets.LectureNotes inComputerScience1492,Springer-Verlag
(1998)429-528.
32. A.J.WellingsandA.Burns:ImplementingAtomicActionsinAda95,IEEE
Trans-actionsonSoftwareEngineering23(1996)107-123.
33. The Home page of Petri net Tools on the Web:
http://www.daimi.aau.dk/~pet rine t/too ls/
34. TheHomepageoftheDesign/CPNtool:http://www.daimi.au.dk/design CPN/