References
[1] N.C. Narendra, “Adaptive Workflow Management – An Integrated Approach and System Architecture,” ACM Symposium on Applied Computing 2000, to appear
[2] N.C. Narendra, “Goal-based and Risk-based Creation of Adaptive Workflow Processes,” American Association for Artificial Intelligence (AAAI) Spring Symposium 2000, to appear
[3] Rajesh Bhave and N.C. Narendra “An Innovative Strategy for Organizational Learning,” World Congress on Total Quality (WCTQ) 2000
[4] W.M.P. van der Aalst, "Petri Net Based Scheduling," Computing Science
Reports 95/23, Eindhoven University of Technology, Eindhoven, 1995, also available
from http://wwwis.win.tue.nl/~wsinwa/orspec.ps
[6] W.M.P. van der Aalst, "Petri-net-based Workflow Management Software", In A. Sheth, editor, Proceedings of the NFS Workshop on Workflow and Process Automation in Information Systems, pages 114--118, Athens, Georgia, May 1996.
[7] Ellis, C., Keddara, K., and Wainer, J., "Modeling Workflow Dynamic Change Using Timed Hybrid Flow Nets", Proceedings of the Petri Net Workshop on Workflow Management: Net Based Concepts, Models, Techniques and Tools, June 1998.
[8] D.E. Kitchin and T.L. McCluskey, "Object-Centered Planning," 15th Workshop of the UK Planning and Scheduling Special Interest Group, Liverpool John Moores University, Liverpool 1996; available from ftp://helios.hud.ac.uk/pub/artform/sig_96.ps
[9] A. Cesta, A. Oddi and S.F. Smith, "Scheduling Multi-Capacitated Resources under Complex Temporal Constraints," Technical Report CMU-RI-TR-98-17, Robotics Institute, Carnegie-Mellon University, 1998; available from
http://www.cs.cmu.edu/afs/cs/project/ozone/www/PCP/publications/cl-pro-techrpt.html
[10] C. Cheng and S.F. Smith, "Generating Feasible Schedules under Complex Constraints," in Proceedings of 12 th National Conference on AI (AAAI-94), 1994.
[11] T. Bauer and P. Dadam, "Efficient Distributed Control of Enterprise-Wide and Enterprise Workflows," Proceedings Workshop Enterprise-wide and Cross-enterprise Workflow Management: Concepts, Systems, Applications, 29.
Jahrestagung der GI (Informatik '99), S. 25 - 32, 1999; available from http://www.informatik.uni-ulm.de/dbis/papers/1999/BaDa99a.pdf
[12] J. Kontio, D. Getto and D. Landes, "Experiences in improving risk management processes using the concepts of the Riskit method," available from http://mordor.cs.hut.fi/~jkontio/fse6-rm.pdf
[13] Q. Chen, P. Chundi, U. Dayal and M. Hsu, "Dynamic Agents", International Journal of Cooperative Information Systems, 1998
[14] M. Silva and J. Campos, "Structural Performance Analysis of Stochastic Petri Nets," In Procs. IEEE Intern. Computer Performance and Dependability Symp., pp.
61-70, Erlangen, Germany, April 1995; available from
http://www.cps.unizar.es/~jcampos/
Concurrent Ada Programs
Using Petri Nets
A.Burns
1
,A.J.Wellings 1
,F.Burns 2
,A.M.Koelmans
2
,M.Koutny
2
,A.Romanovsky
2
,andA. Yakovlev
2
1
Real-TimeSystemsResearchGroup
DepartmentofComputerScience
UniversityofYork,U.K.
2
AsynchronousSystemsLaboratory
DepartmentofComputingScience
UniversityofNewcastleuponTyne,U.K.
Abstract. Ada95 is anexpressive concurrent programminglanguage
with which it is possible to build complex multi-tasking applications.
Muchofthecomplexityoftheseapplicationsstemsfromtheinteractions
betweenthe tasks.Thispaperargues thatPetrinetsoerapromising,
tool-supported,techniqueforcheckingthelogicalcorrectnessofthe
task-ing algorithms.Thepaperillustratesthe eectivenessof thisapproach
byshowingthecorrectnessofanAdaimplementationoftheatomic
ac-tionprotocolusingavarietyofPetrinettools,includingPED,PEPand
INAforP/TnetsandDesign/CPNforColouredPetrinets.
1 Introduction
As high-integritysystemsbecome moresophisticated,the resultingcomplexity
is easier to manageif the applications arerepresented asconcurrentprocesses
rather thansequentialones.Inevitably,the introductionof concurrencybrings
problemsofprocessinteractionandcoordination.Intryingtosolvethese
prob-lems,languageandoperatingsystemresearchershaveintroducednewhigh-level
programmingconstructs.These design abstractions are oftencloselyrelated to
thespecicdomainbeingaddressed.Forexample,intheworldofsoftware
fault-tolerance, the notion of conversations [24] and atomic actions [11,19] are
in-troduced to facilitate the safeand reliablecommunicationbetweenagroup of
processesin thepresenceofhardwareandsoftwarefailures, in additionto
pro-viding a structuring technique for such systems. Research languages such as
ConcurrentPascalhavebeenusedasthebasisforexperimentation[18],oraset
of proceduralextensions or object extensions have been produced. For
exam-ple, Arjunauses thelatter approach to provide atransaction-basedtoolkitfor
C++ [29]. However,it is now acceptedthat the proceduraland object
exten-sionsareunable tocopewithallthesubtletiesinvolvedin synchronisation and
co-operationbetweenseveralcommunicatingconcurrentprocesses.
makethe transition into general-purpose programminglanguagesoroperating
systems. For example, no mainstreamlanguageor operatingsystems supports
thenotionofaconversation[9]. Theresultisthatall thehard-earnedresearch
experienceisnotpromulgatedintoindustrialuse.
If high-level support is not going to be found in mainstream languages,
therequiredfunctionalitymustbeprogrammedwithlower-levelprimitivesthat
are available. For some years nowwehavebeen exploring the use of the Ada
programming language as a vehicle for implementing reliable concurrent
sys-tems [32]. The Ada 95 programminglanguage denes anumber of expressive
concurrency features [1]. Used together they represent a powerful toolkit for
building higher-level protocols/designabstractions that havewide application.
Forexample,[32]recentlyshowedhowAda95canbeusedtoimplementAtomic
Actions.And,assuchanabstractionisnotdirectlyavailableinanycurrent
pro-gramming language,this representsa signicantstep in moving these notions
into generaluse. An examination of this, and other applications, showsthat a
numberoflanguagefeaturesareused intandem toachievetherequiredresult.
Featuresinclude:
{ Tasks-basicunitofconcurrency.
{ AsynchronousTransferofControl(ATC)-anasynchronousmeansof
aect-ingthebehaviourofothertasks.
{ Protected Types - abstract data types whose operations are executed in
mutualexclusion,andwhichsupportsconditionsynchronisation.
{ Requeue - a synchronisation primitive that allows a guardedcommand to
beprematurelyterminatedwiththecallingtaskplacedonanotherguarded
operation.
{ Exceptions- ameans ofabandoningtheexecutionof asequentialprogram
segment.
{ Controlledtypes-afeaturethatallowsmanipulationofobjectinitialisation,
nalisationandassignment.
Theexpressivepowerof theAda 95concurrencyfeaturesis thereforeclear.
What is not as straightforward is how to be condent that the higher-level
abstractionsproducedareindeedcorrect.Asanumberofinteractionsare
asyn-chronousthispresentsasignicantvericationproblem.Theideaofverication
usingModelCheckingwithanitestatemodel (FSM)ofanAdaprogramwas
rst presented in [10]. This method constructed a set of FSMs of individual
tasks interacting via channels, and applied analysis of the interleaving
seman-tics of the product of FSMsusing the softwaretoolUppaal. In this paper, we
investigatea complementaryapproach basedon Petri nets andtheir power to
model causalitybetweenelementaryeventsoractionsdirectly.This canbe
ad-vantageous for asynchronous nature of interactions between tasks. Petri nets,
bothordinary[26]and highlevel(e.g.coloured nets[17])oer awide rangeof
analysis toolsto model andverifythelogicalcorrectnessaccordingto two
cru-cial kindsof properties:(i) safety- anincorrectstate cannotbeentered (from
entered(fromalllegalinitialstatesofthesystem).
Petrinets havegenerallybeen applied tothe vericationofAda programs,
e.g. [28,23,8]. This work has mostly been focused on thesyntactic extraction
of Petrinets from Ada code in such away that the vericationof properties,
such as deadlock detection, could be done more eÆciently. To alleviate state
spaceexplosiontechniqueslikestructuralreduction[28]anddecomposition[23]
of`Adanets'havebeenproposed.
OurresearchisbasedonapplyingPetrinetstomodelconcurrentAdacode,
andusing Petri netstools,suchasPEPandDesign/CPN,toverifyits
correct-ness.However,weproposetodealwiththeunavoidablecomplexityofthe
result-ing programswithin acompositionalapproach employingaversatile libraryof
designabstractionswithwellunderstoodandformally veriedproperties.
Con-dence in the abstraction can be signicantly increased and the development
activityitself supported bymodelling, simulationand analysis of the dynamic
behaviourof thePetri net model; thebehaviourcanbeanalysed either by
ex-ploringtheset ofreachablestatesofthenetoritspartialordersemantics,such
as theunfoldingprex. Thislibrarycanthenbeusedto tackletheverication
of complexdesigns.Thus, while weare ultimatelyinterested in eÆcientmodel
checkingtoo,themainfocusofthispaperisonthesemanticmodellingofsalient
task interactionmechanismsfrom Ada95. Tothebestof ourknowledge, there
hasbeennoattemptofusingPetrinetstoanalyseAda95modelsofAtomic
Ac-tions,particularlywithATCandexceptions.However,someworkonanalysing
Ada 95 programs (with ATC,protected objects,and requeue statement) with
Petrinetshasbeenrecentlyreportedin[15].
Thispaperisorganisedasfollows.Anintroductiontomodelcheckingbased
onPetrinetsisgiven inthe nextsection. Weuseourexisting studyof Atomic
Actions to illustrate the adopted procedure. A simple model is introduced in
Section3anditsrenementinSection4.ConclusionsarepresentedinSection5.
2 Model Checking using Petri Nets
Modelcheckingisatechniqueinwhichthevericationofasystemiscarriedout
usinganiterepresentationofitsstatespace.Basicproperties,suchasabsence
of deadlock or satisfactionof a stateinvariant(e.g. mutual exclusion), can be
veriedbycheckingindividualstates.Moresubtleproperties,suchasguarantee
ofprogress,requirecheckingforspeciccyclesinagraphrepresentingthestates
and possible transitions betweenthem. Properties to bechecked are typically
describedbyformulaein abranchingtimeorlineartimetemporallogic[13].
Themain drawbackof modelchecking isthat it suers from the
combina-torial explosion problem. That is, even a relatively small system specication
may,andoftendoes,yieldaverylargestatespacewhichdespitebeingnite
re-quirescomputationalpowerforitsmanagementbeyondtheeectivecapability
of available computers.Tohelp cope withthe stateexplosion problem a
num-beroftechniqueshavebeenproposed whichcanroughlybeclassiedasaiming
rentsystem, or at an explicit representation of areduced, yet suÆcient, state
space of the system. Examples of the former are algorithms based on the
bi-narydecisiondiagrams(BDDs)[7].Techniquesaimedatreducedrepresentation
of statespacesaretypicallybasedontheindependence of someactions,which
is a characteristicfeature of reactive concurrent systems,often relying on the
partial order view of concurrent computation. Briey, in a sequential system,
it is theactual order ofthe executionof individual actions which is usually of
importance,whereasin aconcurrentsystemtheactualorderinwhich,say,two
messagesweresentandthenreceivedmaybeirrelevanttothecorrectnessofthe
whole system.Examplesinclude partial orderverication[16,21]andstubborn
set method [31].The partial order view of concurrentcomputation is also the
basisof the algorithmsemployingMcMillan's unfoldings [14],where theentire
statespaceisrepresentedimplicitlyusinganacyclicdirectedgraphrepresenting
system'sactionsandlocalstates.
Model checking is a technique that requires tool support. For Petri nets,
therearemanytoolsofdierentmaturityavailable.Thesetoolsarecategorised
accordingto many parameters[33].Inour study, weused three relatively
ma-turetools.One isPEP [2,3],which usesordinaryPlace/Transitionnets anda
number of model checking methods, such asreachability analysis and
unfold-ing prex.The secondoneis INA(Integrated NetAnalyzer) [27].Thethird is
Design/CPN[34],which isbasedontheColoured Petri netsand hasextensive
facilitiesforsimulationandoccurrence(reachbility)graphanalysis.
2.1 The PEP Tool
ThePEPtool[2,3,22]providesamodellingandvericationenvironmentbased
onPetrinets,however,itsprincipalmethodofinputtinglargedesignsistousea
simpleconcurrentprogramminglanguage.Thetoolcompilesaprogramintoan
internalrepresentationin termsofa1-safePetrinetwhich canthenbeveried
forcorrectnessusingavarietyoftechniques,includingones supportedbyother
modelcheckingtools,suchasSPINorSMV.Therelevantcorrectnessproperties,
canbespeciedin ageneral-purposelogic notation, such asCTL*orS4. The
PEPsystemincorporatesmodelcheckersbasedonunfoldingandstructuralnet
theory.
ThePEPtool's additionaladvantageis thatit isbased onacompositional
Petrinetmodel,bothP/T-netbasedandhigh-levelnetbased[4{6].Ittherefore
providesa sound ground to develop acompositional model supporting design
abstractions.
2.2 The INA Tool
TheINAtoolisaninteractiveanalysistoolwhich incorporatesalargenumber
ofpowerfulmethodsforanalysisofP/Tnets.Thesemethodsincludeanalysisof:
(i) structuralproperties, such asstate-machine decomposability, deadlock-trap
analysis,T-and P-invariantanalysis,structuralboundedness; (ii)behavioural
conict-freenes; (iii) specic user-dened properties, such as those dened by
predicates and CTL formulas and tracesto pre-dened states. These analyses
employ various techniques, such as linear-algebraic methods (for invariants),
reachabilityandcoverabilitygraphtraversals,reducedreachabilitygraphbased
onstubbornsetsandsymmetries.
TheINAtoolusesacombinationofinteractivetechniques,wheretheuseris
prompted forvarious specicationsandqueries,and le-processing techniques.
ThebasicPetrinetleformatiscompatiblewithothertools,suchasPEDand
PEP,using Petrinetgraphicaleditors.
2.3 The Design/CPN Tool
ColouredPetriNets(CP-nets)areanextensionofthebasicPetriNetmodel[17].
ACP-netmodelconsistsofacollectionofplaces,transitions,andarcsbetween
these places and transitions. The model contains tokens that ow around the
model and are stored in the places. The essential feature of CP-nets is that
theyallowcomplexdatatypes,i.e.objects,tobeattachedtothetokens.These
objects contain attributes reecting the system being modelled. The ow of
thetokensisdetermined bysocalled guards,whichareconditions,attached to
the arcs of the model, that determine whether a transition is allowed to re.
These guards therefore determine the dynamic behaviour of the model; they
allowsophisticatedbehaviouralpropertiestobemodelled.Theonlysoftwaretool
currentlycapableofsimulatingandanalysingCP-Netmodelsandgeneratingan
executablecode(intheMLprogramminglanguage)isDesign/CPN[34].Inthe
Design/CPNsystem,guardsarespeciedinML.Crucially,Design/CPNallows
entryofhierarchicalmodels,whichgreatlyaidsintheunderstandingofcomplex
models.
3 Model of Simple Atomic Actions
3.1 Atomic Actions
An atomicactionisadynamicmechanismforcontrollingthejointexecutionof
a groupof tasks such that their combined operation appears asan indivisible
actions [19,25]. Essentially, an action is atomic if the tasks performing it can
detectnostatechangeexceptthoseperformedbythemselves,andiftheydonot
reveal their statechanges until the action is complete. Atomic actions can be
extendedtoincludeforwardorbackwarderrorrecovery.Inthispaperwewill
fo-cusonlyonforwarderrorrecoveryusingexceptionhandling[11].Ifanexception
occursinoneofthetasksactiveinanatomicactionthenthatexceptionisraised
in all processesactivein theaction.Theexception issaidto beasynchronous
as itoriginatesfromanotherprocess.
ToshowhowatomicactionscanbeprogrammedinAda[32],considerasimple
non-nested action between, say, three tasks. The action is encapsulated in a
packagewiththreevisibleprocedures,eachofwhichiscalledbytheappropriate
task. It is assumed that no tasks are aborted and that there are no deserter
tasks[18].
package simple_action is
procedure T1(params : param); -- from Task 1
procedure T2(params : param); -- from Task 2
procedure T3(params : param); -- from Task 3
end simple_action;
The body of the package automatically provides a well-dened boundary,
soallthat isrequiredis to provide theindivisibility. A protectedobject,
Con-troller, can beused for this purpose. Thepackage'svisible procedures callthe
appropriateentries andproceduresintheprotectedobject.
Thebodyofthepackageisgivenbelow.
with Ada.Exceptions; use Ada.Exceptions;
package body action is
type Vote_T is (Commit, Aborted);
protected controller is
entry Wait_Abort(E: out Exception_Id);
entry Done;
entry Cleanup (Vote : Vote_t; Result : out Vote_t);
procedure Signal_Abort(E: Exception_Id);
private
entry Wait_Cleanup(Vote : Vote_t; Result : out Vote_t);
Killed : boolean := False;
Releasing_cleanup : Boolean := False;
Releasing_Done : Boolean := False;
Reason : Exception_Id;
Final_Result : Vote_t := Commit;
informed : integer := 0;
end controller;
-- any local protected objects for communication between actions
protected body controller is
entry Wait_Abort(E: out Exception_id) when killed is
begin
E := Reason;
informed := informed + 1;
if informed = 3 then
Killed := False;
end if;
end Wait_Abort;
entry Done when Done'Count = 3 or Releasing_Done is
begin
if Done'Count > 0 then
Releasing_Done := True;
else
Releasing_Done := False;
end if;
end done;
entry Cleanup (Vote: Vote_t;
Result: out Vote_t) when True is
begin
if Vote = Aborted then
Final_result := Aborted;
end if;
requeue Wait_Cleanup with abort;
end Cleanup;
procedure Signal_Abort(E: Exception_id) is
begin
killed := True;
reason := E;
end Signal_Abort;
entry Wait_Cleanup (Vote : Vote_t; Result: out Vote_t)
when Wait_Cleanup'Count = 3 or Releasing_Cleanup is
begin
Result := Final_Result;
if Wait_Cleanup'Count > 0 then
Releasing_Cleanup := True;
else
Releasing_Cleanup := False;
Final_Result := Commit;
end if;
end Wait_Cleanup;
end controller;
procedure T1(params: param) is
X : Exception_ID;
Decision : Vote_t;
begin
select
Controller.Wait_Abort(X);
raise_exception(X);
then abort
begin
Controller.Done; --signal completion
exception
when E: others =>
Controller.Signal_Abort (Exception_Identity(E));
end;
end select;
exception
-- if any exception is raised during
-- the action all tasks must participate in the recovery
when E: others =>
-- Exception_Identity(E) has been raised in all tasks
-- handle exception
if handled_ok then
Controller.Cleanup(Commit, Decision);
else
Controller.Cleanup(Aborted, Decision);
end if;
if Decision = Aborted then
raise atomic_action_failure;
end if;
end T1;
procedure T2(params : param) is ...;
procedure T3(params : param) is ...;
end action;
Eachcomponentoftheaction(T1,T2,andT3)hasidenticalstructure.The
componentexecutes aselectstatement withan abortable part.The triggering
eventissignalledbythecontroller protectedobjectifanycomponentindicates
that anexception has beenraised and not handled locally in one of the
com-ponents.Theabortablepartcontainstheactualcodeof thecomponent.If this
codeexecuteswithoutincident, thecontrolleris informedthat thiscomponent
isreadyto committheaction.
Ifanyexceptions are raisedduring the abortable part,the controller is
in-formedand theidentityoftheexceptionpassed.
If thecontroller has receivednotication of an unhandled exception, it
re-leasesalltaskswaitingontheWaitAborttriggeringevent(anytasklatein
arriv-ingwillreceivetheeventimmediatelyittriestoenterintoitsselectstatement).
Thetasks havetheirabortableparts aborted (if started),and theexception is
raisedin eachtaskbythestatementaftertheentrycalltothecontroller.Ifthe
exceptionissuccessfullyhandledbythecomponent,thetaskindicatesthatitis
preparedtocommittheaction.Ifnot,thenitindicatesthat theactionmustbe
aborted.Ifanytaskindicatesthattheactionistobeaborted,thenalltaskswill
simplystatetransitiondiagram.