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

作者：高飞; 武淑红; 王耀力

来源：现代电子技术, 2019, 42(12): 57-61.

DOI：10.16652/j.issn.1004-373x.2019.12.014

• 多线程建模
• 死锁检测
• 语义转换
• 形式化验证
• 通信顺序进程
• 过程分析

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

• 单位
  太原理工大学