Today s Lecture Lecture 9 Petri Nets Continued Kenneth M Anderson Foundations of Software Engineering CSCI 5828 Spring Semester 2000 Finish the Filling Station Example Look at analysis techniques using Petri Nets Look at extensions to the basic Petri Net formalism add data to tokens add conditionals to transitions February 15 2000 Filling Station Example 2 Concurrency Problems Starvation Lets model the following situation Fuel Pumps Spaces next to Pumps A cashier that takes payment Enabled transition never fired Deadlock Unintended lack of enabled transitions Questions V V Tries to Detect These Problems What is the concurrency that we want modeled How do we handle the parameterization of the Petri net e g lets say I want to add a pump February 15 2000 Kenneth M Anderson 2000 Kenneth M Anderson 2000 3 Static and dynamic analysis techniques February 15 2000 Kenneth M Anderson 2000 4 Approaches to Analysis Analysis of Specifications Dynamic Analysis Design is a Human Activity Executes specification text to reveal properties Requires executable specifications Example testing Can be wrong can change Verification and Validation V V are W R T Activities A Confidence Game Static Analysis Examines specification text to reveal properties Useful in the absence of execution semantics but also where execution would be impractical Example proof of correctness V V can only be used to raise confidence in the quality of a specification February 15 2000 Kenneth M Anderson 2000 5 Dynamic Analysis Kenneth M Anderson 2000 Kenneth M Anderson 2000 6 Petri Net Dynamic 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 of Error February 15 2000 February 15 2000 7 Reachability Graph The reachability graph of a Petri net is a graph representation of its possible firing sequences Analysis Cast as Search for Node in Reachability Graph Found means behavior possible not found means behavior impossible February 15 2000 Kenneth M Anderson 2000 8 Two process Semaphore In1 Petri Net Dynamic Analysis Example Two process Semaphore In2 Is it possible for both processes to be in their critical regions at the same time in the same marking That is is the following a valid marking Sem Out1 February 15 2000 CR1 CR2 M In1 CR1 Out1 Sem In2 CR2 Out2 Out2 0 1 0 0 0 1 0 Kenneth M Anderson 2000 9 February 15 2000 Kenneth M Anderson 2000 10 Reachability Graph Reachability Graph Each node in the graph is a marking In1 CR1 Out1 Sem In2 CR2 Out2 Each node in the graph is a marking In1 CR1 Out1 Sem In2 CR2 Out2 0 0 1 1 1 0 0 0 1 0 0 1 0 0 0 0 1 0 0 1 0 M0 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0 1 0 0 1 0 0 0 0 1 1 0 0 1 0 0 1 February 15 2000 Kenneth M Anderson 2000 11 February 15 2000 Kenneth M Anderson 2000 12 Static Analysis Petri Net Dynamic Analysis Example Two process Semaphore Is it possible for both processes to be in their critical regions at the same time in the same marking That is is the following a valid marking 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 Error M In1 CR1 Out1 Sem In2 CR2 Out2 0 1 0 0 0 1 0 February 15 2000 Kenneth M Anderson 2000 13 Petri Net Static Analysis February 15 2000 Kenneth M Anderson 2000 14 Petri Net Static Analysis The Method of Invariants Example Two process Semaphore Invariants are properties of a Petri net that hold in all markings Analysis Cast as Proof of Invariance Is the sum of the tokens in CR1 CR2 and Sem equal to 1 in all reachable markings That is forAll m all possible markings does CR1 CR2 Sem 1 February 15 2000 Kenneth M Anderson 2000 15 February 15 2000 Kenneth M Anderson 2000 16 Shortcoming of Basic Petri Nets Some Enhancements to Basic Petri Nets Simplicity of building blocks leads to complexity in nets Typed places and information bearing tokens Predicate transitions Hierarchical decomposition of places and transitions Example Semaphore for n processes requires 2n transitions and 3n 1 places Would Like Requirement for analysis of higher level nets reducible to basic nets for analysis Enable and fire as computations Tokens as data not just control February 15 2000 Higher Level Petri Nets Kenneth M Anderson 2000 17 February 15 2000 Higher Level Net 19 71 p p s 1 s true 19 71 s Kenneth M Anderson 2000 p p 3 p s 0 s 1 s true s 1 p February 15 2000 18 Higher Level Net p s 0 Kenneth M Anderson 2000 s token value 3 s 1 p 19 February 15 2000 Kenneth M Anderson 2000 20 Higher Level Net 19 71 Higher Level Net p transition predicate p p s 0 s 1 s true s 19 71 token value transition predicate 3 21 February 15 2000 p s 0 s 1 s true p Kenneth M Anderson 2000 s token value 3 s 1 arc expression Kenneth M Anderson 2000 22 Execution Model p p February 15 2000 s 1 s p Higher Level Net transition predicate s 0 true s 1 Kenneth M Anderson 2000 19 71 p p p February 15 2000 p s Enable is a Predicate on Input Tokens token value Transition with k input places is enabled if there exists a k tuple of tokens one at each input place that satisfy the predicate called a ready tuple Enabled transition and ready tuple are nondeterministically selected Tokens of selected ready tuple removed at firing 3 s 1 arc expression 23 February 15 2000 Kenneth M Anderson 2000 24 Execution Model Higher Level Net Semaphore 19 71 Function Computes Output Token Values Transition with h output places uses the function to compute h values one for each output token p p p s 0 s 1 s true s 3 s 1 p February 15 2000 Kenneth M Anderson 2000 25 February 15 2000 Kenneth M Anderson 2000 Enabled Transition 19 71 After Firing p 19 p p s 0 s 1 s true Kenneth M Anderson 2000 p s p 3 71 p s 0 s 1 s true s 1 p February 15 2000 26 s 2 s 1 p 27 February 15 2000 Kenneth M Anderson 2000 28 Enabled Transitions 19 After Firing p p p 71 p s 0 s 1 s true s p 2 71 s 1 s true s 1 s 1 p Kenneth M Anderson 2000 29 February 15 2000 Kenneth M Anderson 2000 Enabled Transition 30 After Firing p p p 19 71 p s 1 p February 15 2000 19 s 0 p s 0 s 1 s true s p 1 71 p s 0 s 1 s true s 1 s 2 s 1 …
View Full Document
Unlocking...