Papers › Real-time System Modeling and Verification through Labeled Transition System Analyser (LTSA)
Real-time System Modeling and Verification through Labeled Transition System Analyser (LTSA)
Yilong Yang, Xiaoshan Li, Quan Zu
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
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.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections