|
|
Motivation
In RAM we model behavior of our aspects using UML sequence and state diagrams. Both these formalisms, while different, will
essentially allow us to model the same behavior but depict it from two different perspectives. The challenge is to ensure that
both these views do indeed correspond to the same behavior.
When models get very large and complex it becomes very hard to verify consistency dynamically.
It is imperative to have an algorithmic way of solving this issue.
Thus, we wish to exploit the analysis power of petri-nets in order to verify the consistency of RAM.
We hope to do this by performing state space analysis and reachability analysis using widely available tools(such as pipe2).
|
