|
|
|
|
Experiments
Our ExampleThe example we will be working with, to demonstrate our design and implementation as well as to perform analysis on, is shown below:State Chart To Petri Net
Reachability Analysis for state chart
Case With Consistent Behavior
Sequence Diagram To Petri Nets
Final Merged Petri Net
Reachability AnalysisReachability Analysis for sequence diagramReachability Analysis for final modelNotice how the tail of this final model corresponds to what the sequence diagram imposed on the model with respect to the sequence of events to occur and be sent to the state chart
Case With Inconsistent Behavior
Sequence Diagram To Petri Nets
Final Merged Petri Net
Reachability AnalysisReachability Analysis for Sequence DiagramReachability Analysis for Final ModelNotice how the tail of this final model differs from what the sequence diagram imposed on the model with respect to the sequence of events to occur and be sent to the state chart. In this case we where expecting the transition withdraw1 to fire but instead withdraw1Dual2 fired indicating that something when wrong since the sequence diagram specified that withdraw is sent and received and then deposit was sent and received. | ||||||||||||||||||||||
|
|