Analysis of the Model Checkers' Input Languages for Modeling Traffic Light Systems | Science Publications

Journal of Computer Science

Pathiah A. Samat¹  Abdullah M. Zin¹  Zarina Shukur¹ 

关键词: Model checking;    distributed control system;    user interface;    Linear Temporal Logic (LTL);    Computational Tree Logic (CTL);    Distributed Control System (DCS);    Probabilistic Computation Tree Logic (PCTL);    State Transition Diagram (STD);   

DOI  :  10.3844/jcssp.2011.225.233

学科分类：计算机科学（综合）

来源: Science Publications

【 摘 要 】

Problem statement: Model checking is an automated verification technique that can beused for verifying properties of a system. A number of model checking systems have been developedover the last few years. However, there is no guideline that is available for selecting the most suitablemodel checker to be used to model a particular system. Approach: In this study, we compare the useof 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 formodeling this type of system. Limitations and differences of their input language are compared andanalyses by using a set of questions. Results: The result of the study shows that although the inputlanguages of these model checkers have a lot of similarities, they also have a significant number ofdifferences. The result of the study also shows that one model checker may be more suitable thanothers for verifying this type of systems Conclusion: User need to choose the right model checker forthe problem to be verified.

【 授权许可】

Unknown