Real-time System Modeling and Verification through Labeled Transition System Analyser (LTSA)

TL;DR

This paper demonstrates how LTSA, a system modeling and verification tool, can effectively bridge the gap between requirements and design using UML-based structure diagrams, verified through a steam boiler case study.

Contribution

It introduces a method to generate start-up models from UML structure diagrams and integrates explicit and implicit time modeling to enhance verification accuracy.

Findings

LTSA effectively models interactions in the steam boiler system.

The approach reduces state space explosion issues.

Verification confirms system properties align with requirements.

Abstract

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.