计算机科学 ›› 2008, Vol. 35 ›› Issue (10): 295-299.
• • 上一篇 下一篇
出版日期:
发布日期:
基金资助:
Online:
Published:
摘要： 模型检测是一种强大的自动分析验证技术。分析了LINUX进程间通信的部分源代码并进行手工形式化建模,使用有限状态自动机描述模型,继而转换成SPIN的输入语言PROMELA,对其进行模型检测,验证了系统的有界性和可终止性,并就进程间通信中容易发生的问题提出了改进方案。
关键词: 模型检测 LINUX 进程间通信 SPIN 系统验证
Abstract: Model checking is a powerful technique to analyse and verify system automatically. Part of the source code of Linux interprocess communication was chosen to be analysed and formalized modeled, then these models were translated into PROMELA, the input lang
Key words: Model checking, Linux, Interprocess communication, Spin, System verification
. LINUX进程间通信的模型检测[J]. 计算机科学, 2008, 35(10): 295-299. https://doi.org/
0 / / 推荐
导出引用管理器 EndNote|Reference Manager|ProCite|BibTeX|RefWorks
链接本文: https://www.jsjkx.com/CN/
https://www.jsjkx.com/CN/Y2008/V35/I10/295
Cited
首页