CSCI 599 - Formal Methods Concurrency ExamplesAgendaConcurrency IssuesTutorial of Petri NetsTutorial of Petri Nets (2)Tutorial of Petri Nets (3)Tutorial of Petri Nets (4)Tutorial of Petri Nets (5)Tutorial of Petri Nets (6)Tutorial of Petri Nets (7)Tutorial of Petri Nets (8)Tutorial of Petri Nets (9)Tutorial of Petri Nets (10)Tutorial of Petri Nets (11) Producer-ConsumerTutorial of Petri Nets (12) Producer-ConsumerAssumptions Gas Station ExampleAssumptions Gas Station Example (2)Gas Station Example Tank ComponentGas Station Example Operator ComponentGas Station Example Pump ComponentGas Station Example Customer ComponentGas Station Example Example Linking ComponentsAssumptions Cruise Control ExampleAssumptions Cruise Control Example (2)Cruise Control Example Engine ComponentCruise Control Example Gas/Break Pedal ComponentsSlide 27Concluding Remarks1Gas Station and Cruise Control Gas Station and Cruise Control SpecificationsSpecificationsRonnie ApcarRonnie ApcarEdwin ChiuEdwin ChiuHasmik JerejianHasmik JerejianNovember 2, 2000November 2, 2000CSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianCSCI 599 - Formal Methods CSCI 599 - Formal Methods Concurrency Examples Concurrency Examples2Concurrency IssuesConcurrency IssuesBrief Tutorial of Petri NetsBrief Tutorial of Petri NetsThe Gas Station SpecificationThe Gas Station SpecificationThe Cruise Control SpecificationThe Cruise Control SpecificationConcluding RemarksConcluding RemarksQ&AQ&ACSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianAgenda Agenda3Synchronization and CommunicationSynchronization and CommunicationResource sharingResource sharingDeadlockDeadlockStarvationStarvationNon-determinismNon-determinismCSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianConcurrency Issues Concurrency Issues4What are Petri Nets?What are Petri Nets?–Petri Nets are a graphical formalism for Petri Nets are a graphical formalism for systems specificationsystems specificationPetri Nets are formed from Petri Nets are formed from finitefinite sets of sets of–PlacesPlaces–TransitionsTransitions–ArrowsArrows connecting either places to connecting either places to transitions or transitions to placestransitions or transitions to placesCSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianTutorial of Petri Nets Tutorial of Petri Nets5A Petri Net (PN) is given a A Petri Net (PN) is given a statestate by by markingmarking its places. its places. MarkingMarking of a PN consists of assigning a of a PN consists of assigning a nonnegative integer to each nonnegative integer to each placeplace. . –Graphically, Graphically, tokenstokens are inserted in places of a PN are inserted in places of a PNInput placeInput place - arrow goes from the place to - arrow goes from the place to the transtionthe transtionOutput placeOutput place - arrow goes from the - arrow goes from the transition to the placetransition to the placeCSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianTutorial of Petri Nets (2) Tutorial of Petri Nets (2)6CSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianTutorial of Petri Nets (3) Tutorial of Petri Nets (3)7CSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianTutorial of Petri Nets (4) Tutorial of Petri Nets (4)8A A transitiontransition may have one or more may have one or more InputInput and and Output placesOutput placesA A transitiontransition is is enabledenabled if there is at least if there is at least one one tokentoken in in eacheach of its of its input placesinput places..An An EnabledEnabled transition may transition may firefire::– one one tokentoken is removed from each is removed from each input input placeplace and one and one tokentoken is inserted in each is inserted in each ouput placeouput place of the transition of the transitionCSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianTutorial of Petri Nets (5) Tutorial of Petri Nets (5)9A Petri Net as A Petri Net as a four-tuple (P,T,I,O)a four-tuple (P,T,I,O), , wherewhere–P is a set of P is a set of placesplaces–T is a set of T is a set of transitionstransitions–I is an input function:I is an input function:for places leading for places leading intointo a transition a transition–O is an output functionO is an output functionfor places leading for places leading outout of a transition of a transitionCSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianTutorial of Petri Nets (6) Tutorial of Petri Nets (6)10Describing Concurrent Systems with PNDescribing Concurrent Systems with PN–TransitionsTransitions - model events or actions - model events or actions–Transition FiringsTransition Firings - model occurrence of - model occurrence of events or execution of actionsevents or execution of actions–Presence of Presence of tokenstokens - denote existence of - denote existence of some condition, that allow an event or some condition, that allow an event or actionaction–TransitionsTransitions are concurrent - if enabled, firing are concurrent - if enabled, firing of one does not prevent others from firingof one does not prevent others from firingCSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianTutorial of Petri Nets (7) Tutorial of Petri Nets (7)11StarvationStarvation–a process never receives access to a a process never receives access to a needed resourceneeded resourceDeadlockDeadlock–iff no transition iff no transition is enabled in that markingis enabled in that markingLiveLive–no deadlock can ever occurno deadlock can ever occurCSCI 599 Formal MethodsNovember 2, 2000Concurrency Examples R. Apcar, E. Chiu, H. JerejianTutorial of Petri Nets (8) Tutorial of Petri Nets (8)12Limitations and extensions of Petri NetsLimitations and extensions of Petri Nets–similar to FSMs (Finite State Machines), similar to FSMs (Finite State Machines), control-oriented modelcontrol-oriented model–tokenstokens are anonymous are anonymoussolution: assigning values to tokenssolution: assigning values to tokens–not possible to specify selection policynot possible to specify
View Full Document
Unlocking...