【摘 要】
：
并发模型分析主要用于业务流程逻辑验证,并不能很好支持多线程程序建模。目前大部分研究主要针对Java程序的死锁检测,对于使用POSIX线程库开发的C语言程序研究并不多。为了检
【基金项目】
：
全国工程专业学位研究生教育指导委员会立项项目(2016-ZX-095),山西省应用基础研究项目(201801D121141).
论文部分内容阅读
并发模型分析主要用于业务流程逻辑验证,并不能很好支持多线程程序建模。目前大部分研究主要针对Java程序的死锁检测,对于使用POSIX线程库开发的C语言程序研究并不多。为了检测POSIX线程库开发的C语言程序是否存在死锁问题,提出一种对多线程程序进行自动建模与死锁检测的形式化验证方法。首先,根据C++CSP框架和源程序之间的联系,实现源程序到C++CSP框架的语义转换;然后,对C++CSP框架建立通信顺序进程(CSP)模型,并通过过程分析工具(PAT)对建立的模型进行死锁检测;最后,通过实例验证了本文中自动
其他文献
灯光效果控制是舞台演出表达艺术情感、营造匹配气氛的主要手段之一,特别是舞蹈人员的追光灯控制需要准确的人体目标检测与跟踪。因此,提出一种基于轮廓模型和AdaBoost算法的舞蹈人员跟踪算法。首先在YCbCr颜色空间采用Canny算子实现人体轮廓模型的检测,有效提高了跟踪的鲁棒性;然后采用基于级联结构的AdaBoost算法实现人体目标跟踪,并对弱分类器的构建与更新进行分析。实验结果显示相比其他算法,提
CORBA,JNI技术下传统演示的Matlab图形窗体存在诸多弊端,COM对象下Com Builder的虚拟演示能够使Matlab图形窗体独立直观显示,保留了原有的窗体属性,诸如获取某点的横纵坐标、