Lecture 9: Petri-Nets (Continued)Kenneth M. AndersonFoundations of Software EngineeringCSCI 5828 - Spring Semester, 2000February 15, 2000 © Kenneth M. Anderson, 2000 2Today’s Lecture• Finish the Filling Station Example• Look at analysis techniques using Petri Nets• Look at extensions to the basic Petri Netformalism– add “data” to tokens– add “conditionals” to transitionsFebruary 15, 2000 © Kenneth M. Anderson, 2000 3Filling Station Example• Lets model the following situation– Fuel Pumps– Spaces next to Pumps– A cashier that takes payment• Questions– What is the concurrency that we want modeled?– How do we handle the parameterization of thePetri net? (e.g. lets say I want to add a pump)February 15, 2000 © Kenneth M. Anderson, 2000 4Concurrency Problems• Starvation Enabled transition never fired• Deadlock Unintended lack of enabled transitions• V&V Tries to Detect These Problems Static and dynamic analysis techniquesFebruary 15, 2000 © Kenneth M. Anderson, 2000 5Analysis of Specifications• Design is a Human Activity Can be wrong; can change• Verification and Validation• V&V are “W.R.T.” Activities• A Confidence Game V&V can only be used to raise confidence inthe quality of a specificationFebruary 15, 2000 © Kenneth M. Anderson, 2000 6Approaches to Analysis• Dynamic Analysis– Executes specification text to reveal properties– Requires executable specifications– Example: testing• Static Analysis– Examines specification text to reveal properties– Useful in the absence of execution semantics, but alsowhere execution would be impractical– Example: proof of correctnessFebruary 15, 2000 © Kenneth M. Anderson, 2000 7Dynamic Analysis• An Experimentation Activity• Goal: Demonstrate (In)correct Behavior• An Experiment Characterizes a Single Behavior• Applied to the Artifact Itself• Can Miss Critical Behaviors• In General, Impossible to Demonstrate Absence ofErrorFebruary 15, 2000 © Kenneth M. Anderson, 2000 8Petri Net Dynamic Analysis• Reachability Graph–The reachability graph of a Petri net is a graphrepresentation of its possible firing sequences• Analysis Cast as Search for Node inReachability Graph– Found, means behavior possible, not foundmeans behavior impossibleFebruary 15, 2000 © Kenneth M. Anderson, 2000 9Two-process SemaphoreIn1In2Out1Out2CR1CR2SemFebruary 15, 2000 © Kenneth M. Anderson, 2000 10Petri Net Dynamic Analysis• Example: Two-process Semaphore Is it possible for both processes to be in theircritical regions at the same time in the samemarking? That is, is the following a validmarking? M = ( In1 , CR1 , Out1 , Sem , In2 , CR2 , Out2 ) = (0,1,0,0,0,1,0)February 15, 2000 © Kenneth M. Anderson, 2000 11Reachability GraphEach node in the graph is a marking( In1 , CR1 , Out1 , Sem , In2 , CR2 , Out2 )February 15, 2000 © Kenneth M. Anderson, 2000 12Reachability GraphEach node in the graph is a marking( In1 , CR1 , Out1 , Sem , In2 , CR2 , Out2 )(0,1,0,0,1,0,0)(1,0,0,0,0,1,0)(0,0,1,1,1,0,0)(1,0,0,1,0,0,1)(0,1,0,0,0,0,1)(1,0,0,1,1,0,0)M0(0,0,1,0,0,1,0)(0,0,1,1,0,0,1)February 15, 2000 © Kenneth M. Anderson, 2000 13Petri Net Dynamic Analysis• Example: Two-process Semaphore Is it possible for both processes to be in theircritical regions at the same time in the samemarking? That is, is the following a validmarking? M = ( In1 , CR1 , Out1 , Sem , In2 , CR2 , Out2 ) = (0,1,0,0,0,1,0)February 15, 2000 © Kenneth M. Anderson, 2000 14Static Analysis• Goal: Prove Theorems About Properties• An Analysis Characterizes a Class of Behaviors• Applied to a (Static) Model• Can Abstract Away Critical Apsects• In General, Impossible to Prove Absence of ErrorFebruary 15, 2000 © Kenneth M. Anderson, 2000 15Petri Net Static Analysis• The Method of Invariants Invariants are properties of a Petri net that holdin all markings• Analysis Cast as Proof of InvarianceFebruary 15, 2000 © Kenneth M. Anderson, 2000 16• Example: Two-process Semaphore Is the sum of the tokens in CR1, CR2, and Semequal to 1 in all reachable markings? That is,forAll(m ε [all possible markings]) does: CR1 + CR2 + Sem = 1Petri Net Static AnalysisFebruary 15, 2000 © Kenneth M. Anderson, 2000 17Shortcoming of Basic Petri NetsWould Like…– Enable and fire as computations– Tokens as data, not just controlSimplicity of building blocks leads tocomplexity in netsExample: Semaphore for n processes requires 2n transitions and 3n+1 placesFebruary 15, 2000 © Kenneth M. Anderson, 2000 18Higher-Level Petri Nets• Some Enhancements to Basic Petri Nets– Typed places and information-bearing tokens– Predicate transitions– Hierarchical decomposition of places andtransitionsRequirement for analysis of higher-level nets:reducible to basic nets for analysisFebruary 15, 2000 © Kenneth M. Anderson, 2000 19Higher-Level Netppppsss + 1true19713s > 0s - 1February 15, 2000 © Kenneth M. Anderson, 2000 20Higher-Level Netppppsss + 1true19713tokenvalues > 0s - 1February 15, 2000 © Kenneth M. Anderson, 2000 21Higher-Level Netppppsss + 1true19713transitionpredicatetokenvalues > 0s - 1February 15, 2000 © Kenneth M. Anderson, 2000 22Higher-Level Netppppsss + 1true19713transitionpredicatetokenvaluearcexpressions > 0s - 1February 15, 2000 © Kenneth M. Anderson, 2000 23Higher-Level Netppppsss + 1true19713transitionpredicatetokenvaluearcexpressions > 0s - 1February 15, 2000 © Kenneth M. Anderson, 2000 24Execution Model• “Enable” is a Predicate on Input Tokens– Transition with k input places is enabled if thereexists a k-tuple of tokens, one at each inputplace, that satisfy the predicate; called a readytuple– Enabled transition and ready tuple arenondeterministically selected– Tokens of selected ready tuple removed atfiringFebruary 15, 2000 © Kenneth M. Anderson, 2000 25Execution Model• Function Computes Output Token Values– Transition with h output places uses thefunction to compute h values, one for eachoutput tokenFebruary 15, 2000 © Kenneth M. Anderson, 2000 26Higher-Level Net Semaphoreppppsss + 1true19713s > 0s - 1February 15, 2000 © Kenneth M. Anderson, 2000 27Enabled Transitionppppsss + 1s > 0true19713s - 1February 15, 2000 © Kenneth M. Anderson, 2000 28After Firingppppsss + 1true19271s >
View Full Document
Unlocking...