Real-time System Modeling and Verification through Labeled Transition System Analyser (LTSA)
This work addresses the problem of requirement verification in software engineering for developers, but it is incremental as it applies an existing tool to a specific domain.
The paper tackled the difficulty of applying model checking to verify system requirements by using the Labeled Transition System Analyser (LTSA) to bridge the gap between requirements and design, demonstrating its abilities through a steam boiler case study and verifying the derived model against required properties.
With the advancement of software engineering in recent years, the model checking techniques are widely applied in various areas to do the verification for the system model. However, it is difficult to apply the model checking to verify requirements due to lacking the details of the design. Unlike other model checking tools, LTSA provides the structure diagram, which can bridge the gap between the requirements and the design. In this paper, we demonstrate the abilities of LTSA shipped with the classic case study of the steam boiler system. The structure diagram of LTSA can specify the interactions between the controller and the steam boiler, which can be derived from UML requirements model such as system sequence diagram of the steam boiler system. The start-up design model of LTSA can be generated from the structure diagram. Furthermore, we provide a variation law of the steam rate to avoid the issue of state space explosion and show how explicitly and implicitly model the time that reflects the difference between system modeling and the physical world. Finally, the derived model is verified against the required properties. Our work demonstrates the potential power of integrating UML with model checking tools in requirement elicitation, system design, and verification.