Modeling Distributed Real-time Elevator System by Three Model Checkers

Authors

  • Qian Zhongsheng Jiangxi University of Finance and Economics, China
  • Li Xin Jiangxi University of Finance and Economics, China
  • Wang Xiaojin Jiangxi University of Finance and Economics, China

DOI:

https://doi.org/10.3991/ijoe.v14i04.8383

Keywords:

Distributed Elevator System, SPIN, UPPAAL, NuSMV, Linear Temporal Logic, Model Checking

Abstract


The characteristics of three popular model checking tools called SPIN, UPPAAL and NuSMV respectively, are compared and analyzed to determine which type of systems is propitious to be described. And a distributed elevator system model is built, whose related properties are verified and compared by these three model checking tools. To begin with, SPIN, UPPAAL and NuSMV, whose modeling language features are compared, are employed to construct an elevator system model respectively. Then, the three validation tools are used to verify several important properties of the elevator model, and the result is analyzed and their own characteristics are summarized. Finally, the experimental results show that SPIN and NuSMV are more suitable for verifying distributed systems while UPPAAL is better for verifying real-time systems.

Downloads

Published

2018-04-26

How to Cite

Zhongsheng, Q., Xin, L., & Xiaojin, W. (2018). Modeling Distributed Real-time Elevator System by Three Model Checkers. International Journal of Online and Biomedical Engineering (iJOE), 14(04), pp. 94–110. https://doi.org/10.3991/ijoe.v14i04.8383

Issue

Section

Papers