Incorporating Object-Orientedness in Transformations from Live Sequence Charts to Colored Petri Nets

摘要

This paper presents an approach of automatic model checking in the requirement model of a software system known as Live Sequence Charts by transforming the behavior into Colored Petri Nets. The technique of combining Objects and Colored Petri Nets is used to provide a robust mechanism for the model checking which serves towards research in code generation from the software requirement model. Two major concepts: Objects inside Petri Nets and Petri Nets inside Objects are used in the composed Colored Petri Nets model to monitor the object's state during system run and to check individual object's behavior when interacting with other objects respectively.