School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

doi:10.3969/j.issn.1006-2475.2012.09.055

Computer and Modernization ›› 2012, Vol. 1 ›› Issue (9): 209-214.doi: 10.3969/j.issn.1006-2475.2012.09.055

• 应用与开发 • Previous Articles Next Articles

School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

XU Xiao-li

School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

Received:2012-05-21 Revised:1900-01-01 Online:2012-09-21 Published:2012-09-21

Abstract

Abstract: Because of the high degree of automation, model checking technology has become one of the most popular way to ensure correctness in the formal verification field. To use the model checker, the user should model the verification-needed system. This paper summarizes the basic principles of model checking technology and explores the Promela modeling with model checker SPIN. Finally, a simple bus operation prototype model is given, and the experimental results are analyzed.


Key words: model checking, modeling, SPIN, Promela

XU Xiao-li. School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China[J]. Computer and Modernization, 2012, 1(9): 209-214.

[1]	LIU Ruoying1, ZOU Weiyu1, HU Shaoqian2, JI Shunhui3. Survey of Digital Twin Modeling and Applications in Power System [J]. Computer and Modernization, 2024, 0(09): 61-68.
[2]	CHEN Rongxin1, WEI Tonghao2, LIU Jie2, HU Zhenzhen2. Design and Verification of UAV-based Cluster Communication Architecture Based on Central Node [J]. Computer and Modernization, 2024, 0(06): 121-126.
[3]	GUAN Jin-ping, YANG Jin-ji, YANG Cheng-long. Formal Verification of Raft Protocol Based on Probabilistic Model [J]. Computer and Modernization, 2023, 0(09): 77-81.
[4]	LYU Zhi-xing, YU Hui, KANG Kai, LI Teng-chang, DU Guo-li. A Feature Modeling Based Bidding Trading Mechanism in Power Blockchain [J]. Computer and Modernization, 2023, 0(08): 112-118.
[5]	SHI Qing-lin, LIU Li-zhe, LI Xing-jian. Troposcatter Channel Estimation Based on Massive MIMO [J]. Computer and Modernization, 2022, 0(12): 18-25.
[6]	DING Xu-dong, YANG Dong-run, LIU Hui, ZHAO Xing-kai, ZHANG Ying, SUN Mei, . A Data-driven Online Modeling Method for Evaporators [J]. Computer and Modernization, 2022, 0(11): 22-31.
[7]	LIU Hui, DING Xu-dong, YANG Dong-run, ZHANG Ying, LIU Zhong-chen, SUN Mei. A Hybrid Modeling Method for Real-time Prediction of Heat Collection in Solar Heat Collection Systems [J]. Computer and Modernization, 2022, 0(10): 55-61.
[8]	WANG Ke-yang, ZHANG Yao, LI Ke-wen, ZHANG Bao-qian, LI Jiang, REN Jie-wen. On-line Detection System of CNC Tool Breakage Based on Attention-LSTM [J]. Computer and Modernization, 2022, 0(05): 68-74.
[9]	ZENG Xu-yang, SUN Ka. Campus Fire Training Simulation Based on DI-Guy [J]. Computer and Modernization, 2021, 0(08): 35-39.
[10]	JIANG Chao-qun, TONG Jing, GUO Ming-deng, LU Rong-jie, CHEN Zheng-ming. Modeling Method of 3D Printing Full Contact Insole Based on Triply Periodic Minimal Surface [J]. Computer and Modernization, 2021, 0(05): 13-19.
[11]	SONG Xin , FAN Zhi-qiang , . Information Service Performance Modeling Based on Laguerre FNN [J]. Computer and Modernization, 2021, 0(03): 1-6.
[12]	LIU Hong-fei, YANG Yao-quan, YANG Yu-hang. Moving Target Tracking Based on Improved Optical Flow Characteristics [J]. Computer and Modernization, 2021, 0(03): 115-121.
[13]	LIU Meng-chao, WANG Yu-mei, WU Ya-fei, ZANG Yi-hua, LIANG Jia. Ontology Based Knowledge Modeling and Analysis of Military Equipment [J]. Computer and Modernization, 2021, 0(01): 76-80.
[14]	LIU Jian-gao, BIN Min. Reconstruction of 3D Cartoon Character Modeling Based on Topology Analysis [J]. Computer and Modernization, 2020, 0(10): 76-83.
[15]	WEN Jing， ZHENG Yang-fei. Generation of Community Correctional Personnel Label Based on Stacking [J]. Computer and Modernization, 2020, 0(03): 60-.

School of Computer Science, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments