TY  - JOUR
AU  - Samat, Pathiah Abdul 
AU  - Zin, Abdullah Mohd 
AU  - Shukur, Zarina 
PY  - 2011
TI  - Analysis of the Model Checkers' Input Languages for Modeling Traffic Light Systems
JF  - Journal of Computer Science
VL  - 7
IS  - 2
DO  - 10.3844/jcssp.2011.225.233
UR  - https://thescipub.com/abstract/jcssp.2011.225.233
AB  - 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.