基于CSP的多线程自动建模及死锁检测研究

• 作者: 武淑红 王耀力 高飞
• 来源期刊: 现代电子技术
• 关键词: 多线程建模 死锁检测 语义转换 形式化验证 通信顺序进程 过程分析
• 年，卷（期）: 2019,（12）
• 所属期刊栏目: 计算机科学与应用
• 页码范围: 57-61
• 页数: 5页
• 分类号: TN911.23-34|TP311.5
• 语种: 中文
• DOI: 10.16652/j.issn.1004-373x.2019.12.014

摘要

并发模型分析主要用于业务流程逻辑验证,并不能很好支持多线程程序建模.目前大部分研究主要针对Java程序的死锁检测,对于使用POSIX线程库开发的C语言程序研究并不多.为了检测POSIX线程库开发的C语言程序是否存在死锁问题,提出一种对多线程程序进行自动建模与死锁检测的形式化验证方法.首先,根据C++CSP框架和源程序之间的联系,实现源程序到C++CSP框架的语义转换;然后,对C++CSP框架建立通信顺序进程(CSP)模型,并通过过程分析工具(PAT)对建立的模型进行死锁检测;最后,通过实例验证了本文中自动建模与死锁检测方法的可行性与有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王耀力	太原理工大学信息与计算机学院	35	182	6.0	12.0
2	武淑红	太原理工大学信息与计算机学院	18	42	4.0	5.0
3	高飞	太原理工大学信息与计算机学院	9	2	1.0	1.0