Real-Time System Modeling and Verification Through Labeled Transition System Analyzer

Yilong Yang, Quan Zu, Wei Ke, Miaomiao Zhang, Xiaoshan Li

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)

Abstract

Model checking as a computer-assisted verification method is widely used in many fields to verify whether a design model satisfies the requirements specifications of the target system. In practice, it is difficult to design a system without the sophisticated requirements analysis. Unlike other model checking tools, the labeled transition system analyzer (LTSA) not only can specify the property specifications of the target system but also provides a structure diagram to specify the system architecture of the requirements model, which can be further used to design the target system. In this paper, we demonstrate the abilities of LTSA shipped with the classic case study of the steam boiler system. In the requirements analysis, the LTSA can specify the cyber and physical components of the target system and interactions between the components and the safety properties of the target system. In system design, the LTSA can automatically generate a start-up design model as the finite state process from the requirements model, and then a design model can be further accomplished by system architects and developers. Finally, the LTSA can automatically verify whether the design model meets the requirements specifications. Our work demonstrates the potential power of model checking tools can be applied and useful in software engineering for requirements analysis, system design, and verification.

Original languageEnglish
Article number8642885
Pages (from-to)26314-26323
Number of pages10
JournalIEEE Access
Volume7
DOIs
Publication statusPublished - 2019

Keywords

  • LTSA
  • UML
  • model checking
  • steam boiler

Fingerprint

Dive into the research topics of 'Real-Time System Modeling and Verification Through Labeled Transition System Analyzer'. Together they form a unique fingerprint.

Cite this