pthread库多线程C程序到MSVL程序的转换方法、计算机程序

摘要

本发明属于计算机软件技术领域，公开了一种pthread库多线程C程序到MSVL程序的转换方法、计算机程序；所述pthread库多线程C程序到MSVL程序的转换方法包括：对pthread库多线程C程序进行静态分析，得到程序的层次语法图；将pthread库多线程C程序通过给出的规则转换为语义等价的MSVL程序。本发明适用于模型检测中pthread库多线程C程序的转换，相较于传统的模型检测方式，MSVL语言的优势在于集系统建模、仿真和验证于一体，可用于描述系统的顺序、选择、循环、并发、同步和信号量等特征，同时可以满足并发及分布式系统的建模需求。本发明提升了工作效率，促进了模型检测技术在学术界和工业界的推广。