Research Article Open Access

Analysis of the Model Checkers' Input Languages for Modeling Traffic Light Systems

Pathiah Abdul Samat, Abdullah Mohd Zin and Zarina Shukur

Abstract

Problem statement: Model checking is an automated verification technique that can be used for verifying properties of a system. A number of model checking systems have been developed over the last few years. However, there is no guideline that is available for selecting the most suitable model checker to be used to model a particular system. Approach: In this study, we compare the use of four model checkers: SMV, SPIN, UPPAAL and PRISM for modeling a distributed control system. In particular, we are looking at the capabilities of the input languages of these model checkers for modeling this type of system. Limitations and differences of their input language are compared and analyses by using a set of questions. Results: The result of the study shows that although the input languages of these model checkers have a lot of similarities, they also have a significant number of differences. The result of the study also shows that one model checker may be more suitable than others for verifying this type of systems Conclusion: User need to choose the right model checker for the problem to be verified.

Journal of Computer Science
Volume 7 No. 2, 2011, 225-233

DOI: https://doi.org/10.3844/jcssp.2011.225.233

Submitted On: 29 October 2010 Published On: 25 February 2011

How to Cite: Samat, P. A., Zin, A. M. & Shukur, Z. (2011). Analysis of the Model Checkers' Input Languages for Modeling Traffic Light Systems. Journal of Computer Science, 7(2), 225-233. https://doi.org/10.3844/jcssp.2011.225.233

  • 3,480 Views
  • 4,840 Downloads
  • 1 Citations

Download

Keywords

  • Model checking
  • distributed control system
  • user interface
  • Linear Temporal Logic (LTL)
  • Computational Tree Logic (CTL)
  • Distributed Control System (DCS)
  • Probabilistic Computation Tree Logic (PCTL)
  • State Transition Diagram (STD)