Common modeling language for model checkers

Pathiah Abdul Samat, Abdullah Mohd. Zin

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

Problem statement: There are many different model checkers that have been developed. Each of the model checkers is based on different input languages and they are suitable for model checking different types of systems. Thus it is important for us to choose the right model checker or modeling and verifying a given system. However, moving from one model checker to another is not an easy task since we have to deal with different input languages. Approach: In order to solve the problem we propose a common modeling language that is based on UML state chart. Some translation rules for translating the model described in the common modeling language into the input languages of model checkers are also presented. Results: The result of the case study shows that our approach has been successfully applied in modeling the control system through the process of transformation and translation. Conclusion: Common modeling language can be used as a front end to help users to properly model a system before it is translated into input language of model checkers.

Original languageEnglish
Pages (from-to)99-106
Number of pages8
JournalJournal of Computer Science
Volume8
Issue number1
DOIs
Publication statusPublished - 2012

Fingerprint

Modeling languages
Model checking
Control systems

Keywords

  • Computational tree logic (CTL)
  • Linear Temporal Logic (LTL)
  • Model checking
  • Probabilistic computation tree logic (PCTL)
  • UML state chart

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications
  • Artificial Intelligence

Cite this

Common modeling language for model checkers. / Samat, Pathiah Abdul; Mohd. Zin, Abdullah.

In: Journal of Computer Science, Vol. 8, No. 1, 2012, p. 99-106.

Research output: Contribution to journalArticle

Samat, Pathiah Abdul ; Mohd. Zin, Abdullah. / Common modeling language for model checkers. In: Journal of Computer Science. 2012 ; Vol. 8, No. 1. pp. 99-106.
@article{7a10d002e4ec427fa13d453842b81be1,
title = "Common modeling language for model checkers",
abstract = "Problem statement: There are many different model checkers that have been developed. Each of the model checkers is based on different input languages and they are suitable for model checking different types of systems. Thus it is important for us to choose the right model checker or modeling and verifying a given system. However, moving from one model checker to another is not an easy task since we have to deal with different input languages. Approach: In order to solve the problem we propose a common modeling language that is based on UML state chart. Some translation rules for translating the model described in the common modeling language into the input languages of model checkers are also presented. Results: The result of the case study shows that our approach has been successfully applied in modeling the control system through the process of transformation and translation. Conclusion: Common modeling language can be used as a front end to help users to properly model a system before it is translated into input language of model checkers.",
keywords = "Computational tree logic (CTL), Linear Temporal Logic (LTL), Model checking, Probabilistic computation tree logic (PCTL), UML state chart",
author = "Samat, {Pathiah Abdul} and {Mohd. Zin}, Abdullah",
year = "2012",
doi = "10.3844/jcssp.2012.99.106",
language = "English",
volume = "8",
pages = "99--106",
journal = "Journal of Computer Science",
issn = "1549-3636",
publisher = "Science Publications",
number = "1",

}

TY - JOUR

T1 - Common modeling language for model checkers

AU - Samat, Pathiah Abdul

AU - Mohd. Zin, Abdullah

PY - 2012

Y1 - 2012

N2 - Problem statement: There are many different model checkers that have been developed. Each of the model checkers is based on different input languages and they are suitable for model checking different types of systems. Thus it is important for us to choose the right model checker or modeling and verifying a given system. However, moving from one model checker to another is not an easy task since we have to deal with different input languages. Approach: In order to solve the problem we propose a common modeling language that is based on UML state chart. Some translation rules for translating the model described in the common modeling language into the input languages of model checkers are also presented. Results: The result of the case study shows that our approach has been successfully applied in modeling the control system through the process of transformation and translation. Conclusion: Common modeling language can be used as a front end to help users to properly model a system before it is translated into input language of model checkers.

AB - Problem statement: There are many different model checkers that have been developed. Each of the model checkers is based on different input languages and they are suitable for model checking different types of systems. Thus it is important for us to choose the right model checker or modeling and verifying a given system. However, moving from one model checker to another is not an easy task since we have to deal with different input languages. Approach: In order to solve the problem we propose a common modeling language that is based on UML state chart. Some translation rules for translating the model described in the common modeling language into the input languages of model checkers are also presented. Results: The result of the case study shows that our approach has been successfully applied in modeling the control system through the process of transformation and translation. Conclusion: Common modeling language can be used as a front end to help users to properly model a system before it is translated into input language of model checkers.

KW - Computational tree logic (CTL)

KW - Linear Temporal Logic (LTL)

KW - Model checking

KW - Probabilistic computation tree logic (PCTL)

KW - UML state chart

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

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

U2 - 10.3844/jcssp.2012.99.106

DO - 10.3844/jcssp.2012.99.106

M3 - Article

VL - 8

SP - 99

EP - 106

JO - Journal of Computer Science

JF - Journal of Computer Science

SN - 1549-3636

IS - 1

ER -