Model Checking Of LSC Specifications

Formal methods are gaining wide acceptance in every phase of the software life cycle with the development of Software Engineering technologies. Being an important technology to capture the software requirements, scenario-based approaches are widely used and many scenario description methods, such as Message Sequece Chart (MSC), are developed. While the Live Sequence Chart (LSC) is an expressive and rigorous language for the scenario description, the model checking of LSC specifications is possible which helps find some error earlier.In this thesis we present a method, which facilitates the model checking of the LSC specifications of the reactive systems, and we have also implemented a tool to automate the method. We first analyze the LSC language, which is an expressive visual behavioural specification language and has rigorous syntax and semantics. Model checking utilizes the state model of systems, thus, we present a method that generates the stale models from LSC models based on the LSC semantics. When the state models of the systems are generated, we can do model checking based on the state models. The property generation for LSC is also analyzed in the thesis. Having discussed the state model generation and the property generation, we studied the model checking methods of LSC specifications. At last, we design and implement a verification tool, which generates state transition models from the XML files of LSC specifications, accepts the input property, and then begins model checking. The model checking method and the supporting tool enable us to validate and verify the software requirements at an early stage.'...