Journal of Computer Science

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

Pathiah Abdul Samat, Abdullah Mohd Zin and Zarina Shukur

DOI : 10.3844/jcssp.2011.225.233

Journal of Computer Science

Volume 7, Issue 2

Pages 225-233


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.


© 2011 Pathiah Abdul Samat, Abdullah Mohd Zin and Zarina Shukur. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.