基于扩展CSP多线程形式化建模与死锁检测研究

发布时间：2021-11-13 19:43

　　随着POSIX多线程（POSIX Threads,Pthreads）广泛应用于各类复杂并发系统,由线程竞争资源或推进顺序不合适所引发的死锁问题变得越来越常见。死锁会造成多线程程序崩溃或非正常终止,对于安全性要求较高的行业会带来灾难性的后果,因此如何有效检测出POSIX多线程程序中潜在的死锁至关重要。近年来,主流的死锁检测方法主要有形式化模型静态死锁检测分析和动态死锁检测两种。相比动态死锁检测方法而言,基于形式化模型分析的静态死锁检测方法由于具备完善的数学理论并且可以在软件系统编译之前检测到程序中潜在的死锁,因此备受广大学者推崇。但是该方法仍存在以下几方面问题需要研究:（1）形式化语言和多线程程序语义描述存在很大偏差,不能直接实现多线程程序语义到形式化模型的映射;（2）使用形式化语言对多线程程序建模时,很容易造成模型过于庞大,以至于在模型检测阶段会产生状态空间爆炸;（3）难以对多线程程序指针建立等价语义的形式化模型。针对以上问题,本文基于扩展CSP（extended CSP,CSP#）提出了一种对POSIX多线程程序自动建模与死锁检测的新方法,主要从以下几方面开展研究:一、提出一种POS... 

【文章来源】：太原理工大学山西省 211工程院校

【文章页数】：76 页

【学位级别】：硕士

【部分图文】：

模型检测基本流程

POSIX多线程程序转换为CSP#模型流程

图 3-3 共享内存数据读写方式 mode of shared memory data readiP 中声明如式(3-1)所示：sp::Chanouttypename_osp::Chanintypename_in

【参考文献】：
期刊论文
[1]面向资源的物联网系统形式化建模与验证[J]. 马莉,李维康,梁晨,李爱萍.  小型微型计算机系统. 2018(01)
[2]使用锁分配图动态检测混合死锁[J]. 禹振,苏小红,邱景.  计算机研究与发展. 2017(07)
[3]由MDA/PIM到Java代码的转换及验证[J]. 李凯宁,武淑红,王耀力.  计算机工程与设计. 2017(06)
[4]模型检测在完整性形式化验证中的应用研究[J]. 严亚伟,周雁舟,惠文涛.  计算机工程与应用. 2017(04)
[5]多核多线程技术综述[J]. 眭俊华,刘慧娜,王建鑫,秦庆旺.  计算机应用. 2013(S1)
[6]基于Elastos线程同步机制的死锁检测技术研究[J]. 张捷,陈榕.  计算机科学. 2008(12)
[7]通信系统演算CCS与自动验证工具MWB[J]. 李元,李祥.  通信技术. 2005(S1)
[8]基于Petri网的模型检测研究[J]. 蒋屹新,林闯,曲扬,尹浩.  软件学报. 2004(09)
[9]形式化方法B及其程序规约机理[J]. 肖美华,薛锦云.  计算机工程. 2004(16)
[10]B语言和方法与Z、VDM的比较[J]. 邹盛荣,郑国梁.  计算机科学. 2002(10)

硕士论文
[1]基于Petri网的多线程死锁检测研究[D]. 黄理.中国科学技术大学 2015



本文编号：3493603