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

Pathiah Abdul Samat, Abdullah Mohd. Zin, Zarina Shukur

Research output: Contribution to journalArticle

3 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)225-233
Number of pages9
JournalJournal of Computer Science
Volume7
Issue number2
DOIs
Publication statusPublished - 2011

Fingerprint

Telecommunication traffic
Model checking
Distributed parameter control systems

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

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications
  • Artificial Intelligence

Cite this

Analysis of the model checkers' input languages for modeling traffic light systems. / Samat, Pathiah Abdul; Mohd. Zin, Abdullah; Shukur, Zarina.

In: Journal of Computer Science, Vol. 7, No. 2, 2011, p. 225-233.

Research output: Contribution to journalArticle

@article{31db50fa59284b5e843ddd10dff0821f,
title = "Analysis of the model checkers' input languages for modeling traffic light systems",
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.",
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",
author = "Samat, {Pathiah Abdul} and {Mohd. Zin}, Abdullah and Zarina Shukur",
year = "2011",
doi = "10.3844/jcssp.2011.225.233",
language = "English",
volume = "7",
pages = "225--233",
journal = "Journal of Computer Science",
issn = "1549-3636",
publisher = "Science Publications",
number = "2",

}

TY - JOUR

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

AU - Samat, Pathiah Abdul

AU - Mohd. Zin, Abdullah

AU - Shukur, Zarina

PY - 2011

Y1 - 2011

N2 - 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.

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.

KW - Computational Tree Logic (CTL)

KW - Distributed control system

KW - Distributed Control System (DCS)

KW - Linear Temporal Logic (LTL)

KW - Model checking

KW - Probabilistic Computation Tree Logic (PCTL)

KW - State Transition Diagram (STD)

KW - User interface

UR - http://www.scopus.com/inward/record.url?scp=80052845200&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80052845200&partnerID=8YFLogxK

U2 - 10.3844/jcssp.2011.225.233

DO - 10.3844/jcssp.2011.225.233

M3 - Article

AN - SCOPUS:80052845200

VL - 7

SP - 225

EP - 233

JO - Journal of Computer Science

JF - Journal of Computer Science

SN - 1549-3636

IS - 2

ER -