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.