UPM Institutional Repository

Analysis of the model checkers' input languages for modeling traffic light systems


Abdul Samad, Pathiah and Mohd Zin, Abdullah and Shukur, Zarina (2011) Analysis of the model checkers' input languages for modeling traffic light systems. Journal of Computer Science, 7 (2). pp. 225-233. ISSN 1549-3636; ESSN: 1552-6607


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.

Download File

[img] PDF
Restricted to Repository staff only

Download (259kB)

Additional Metadata

Item Type: Article
Divisions: Faculty of Computer Science and Information Technology
DOI Number: https://doi.org/10.3844/jcssp.2011.225.233
Publisher: Science Publications
Keywords: Computational Tree Logic (CTL); Distributed control system; Distributed Control System (DCS); Linear Temporal Logic (LTL); Model checking; Probabilistic Computation Tree Logic (PCTL); State Transition Diagram (STD); User interface
Depositing User: Nabilah Mustapa
Date Deposited: 08 Jun 2016 09:00
Last Modified: 08 Jun 2016 09:00
Altmetrics: http://www.altmetric.com/details.php?domain=psasir.upm.edu.my&doi=10.3844/jcssp.2011.225.233
URI: http://psasir.upm.edu.my/id/eprint/22468
Statistic Details: View Download Statistic

Actions (login required)

View Item View Item