Analysis of the model checkers' input languages for modeling traffic light systems
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 check...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Science Publications
2011
|
| Online Access: | http://psasir.upm.edu.my/id/eprint/22468/ http://psasir.upm.edu.my/id/eprint/22468/1/jcssp.2011.225.233.pdf |
| _version_ | 1848844492889653248 |
|---|---|
| author | Abdul Samad, Pathiah Mohd Zin, Abdullah Shukur, Zarina |
| author_facet | Abdul Samad, Pathiah Mohd Zin, Abdullah Shukur, Zarina |
| author_sort | Abdul Samad, Pathiah |
| building | UPM Institutional Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-15T08:31:47Z |
| format | Article |
| id | upm-22468 |
| institution | Universiti Putra Malaysia |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-15T08:31:47Z |
| publishDate | 2011 |
| publisher | Science Publications |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | upm-224682016-06-08T09:00:07Z http://psasir.upm.edu.my/id/eprint/22468/ Analysis of the model checkers' input languages for modeling traffic light systems Abdul Samad, Pathiah Mohd Zin, Abdullah Shukur, Zarina 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. Science Publications 2011 Article PeerReviewed application/pdf en http://psasir.upm.edu.my/id/eprint/22468/1/jcssp.2011.225.233.pdf 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 http://www.thescipub.com/abstract/10.3844/jcssp.2011.225.233 10.3844/jcssp.2011.225.233 |
| spellingShingle | Abdul Samad, Pathiah Mohd Zin, Abdullah Shukur, Zarina Analysis of the model checkers' input languages for modeling traffic light systems |
| title | Analysis of the model checkers' input languages for modeling traffic light systems |
| title_full | Analysis of the model checkers' input languages for modeling traffic light systems |
| title_fullStr | Analysis of the model checkers' input languages for modeling traffic light systems |
| title_full_unstemmed | Analysis of the model checkers' input languages for modeling traffic light systems |
| title_short | Analysis of the model checkers' input languages for modeling traffic light systems |
| title_sort | analysis of the model checkers' input languages for modeling traffic light systems |
| url | http://psasir.upm.edu.my/id/eprint/22468/ http://psasir.upm.edu.my/id/eprint/22468/ http://psasir.upm.edu.my/id/eprint/22468/ http://psasir.upm.edu.my/id/eprint/22468/1/jcssp.2011.225.233.pdf |