Keyword Search:


Bookmark and Share

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

[img] PDF
Restricted to Repository staff only

253Kb

Official URL: http://www.thescipub.com/abstract/10.3844/jcssp.20...

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.

Item Type:Article
Keyword: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
Faculty or Institute:Faculty of Computer Science and Information Technology
Publisher:Science Publications
DOI Number:10.3844/jcssp.2011.225.233
Altmetrics:http://www.altmetric.com/details.php?domain=psasir.upm.edu.my&doi=10.3844/jcssp.2011.225.233
ID Code:22468
Deposited By: Nabilah Mustapa
Deposited On:08 Jun 2016 17:00
Last Modified:08 Jun 2016 17:00

Repository Staff Only: Edit item detail

Document Download Statistics

This item has been downloaded for since 08 Jun 2016 17:00.

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