Capturing a requirement is a great challenge in the initial stages of the software development, be it a system requirement or a customer requirement to the software engineers. Understanding the requirement and predicting or differentiating what may happen and what must happen is difficult especially in the complex real time systems. Live sequence charts are extensions of the message sequence charts which can specify the live ness of the requirements. And the play engine tool is used to specify, validate, and analyze the scenarios of the requirements. This thesis is to evaluate live sequence charts using the play engine tool and to see if the built-in model checkers can detect inconsistencies in the LSC’s.

The requirements capturing and analysis has always been the initial criteria and main problem during the software design and development for the software engineers. It’s been very common to use natural language for capturing the requirements in the industries because of its ease of use. The graphical languages were used to represent the requirements, its behavior and the scenarios graphically or visually, for example UML. UML Sequence diagrams are used in the real time software development to capture the requirements which specifies the scenarios of the system behavior and also the interactions between the objects graphically. Message sequence charts are also a graphical language for representing the scenarios and also the behavior of the system especially in the telecommunication domain. But these two are only useful in specifying the one aspect of the behavior and not much helpful in specifying the liveness of the requirement. Liveness can be defined as something good will happen [34] or something must happen. For this reason live sequence charts were developed which can specify the liveness of the requirement. Live sequence charts are capable of specifying the scenarios what may happen and what must happen. This thesis is to evaluate the live sequence charts using the play engine tool running on the windows machine and also to study the built in model checkers for formal verification. The thesis starts with the various types of graphical representation of requirements in Software Engineering, followed by the Research Methodology, next a bit more explanation of Live Sequence Charts, Evaluation, Result, Conclusions and Lessons Learned from the thesis.