Proceedings of the 2016 5th International Conference on Advanced Materials and Computer Science

CTL Model Checking based on Giraph

Authors
Tingyin Duan, Qinglei Zhou, Shan Pan, Weijun Zhu
Corresponding Author
Tingyin Duan
Available Online June 2016.
DOI
10.2991/icamcs-16.2016.133How to use a DOI?
Keywords
CTL, Kripke, Model checking, Giraph, Hadoop
Abstract

Model checking is a popular model based formal automated verification technology. Computation tree logic is a prominent branching temporal logic for specifying system properties. In order to dispose of the state space explosion problem, we proposed a novel method based on BSP model employing Giraph which is an iterative graph processing system with high scalability. The result of the experiments shows that our method is much more efficient than current methods based on Map-Reduce model.

Copyright
© 2016, the Authors. Published by Atlantis Press.
Open Access
This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

Volume Title
Proceedings of the 2016 5th International Conference on Advanced Materials and Computer Science
Series
Advances in Engineering Research
Publication Date
June 2016
ISBN
978-94-6252-189-6
ISSN
2352-5401
DOI
10.2991/icamcs-16.2016.133How to use a DOI?
Copyright
© 2016, the Authors. Published by Atlantis Press.
Open Access
This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Cite this article

TY  - CONF
AU  - Tingyin Duan
AU  - Qinglei Zhou
AU  - Shan Pan
AU  - Weijun Zhu
PY  - 2016/06
DA  - 2016/06
TI  - CTL Model Checking based on Giraph
BT  - Proceedings of the 2016 5th International Conference on Advanced Materials and Computer Science
PB  - Atlantis Press
SP  - 652
EP  - 657
SN  - 2352-5401
UR  - https://doi.org/10.2991/icamcs-16.2016.133
DO  - 10.2991/icamcs-16.2016.133
ID  - Duan2016/06
ER  -