Transformation from Live Sequence Charts to Colored Petri Nets

摘要

A tool called LSC2CPN has been developed to reduce the gap between informal and formal methods of loosely coupled distributed software specification, verification, and validation. This tool reads the Live Sequence Chart (LSC) model as an input and transforms the system into an equivalent Colored Petri Nets model. LSC is a richer construct than UML Sequence Diagram. The resulting Colored Petri net can be analyzed using CPNTools to check whether the model satisfies desired behavioral properties. The paper presents atomic transformation steps required to map Live Sequence Charts into behaviorally equivalent Colored Petri nets. The proposed transformation method is scalable with respect to Colored Petri net modeling efforts as a function of the number of messages in LSC. It may not be scalable from CPNTools simulation time perspective due to potential state explosion problem.