欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
位置：立项数据库 > 立项详情页
中文摘要：
当前软件错误定位主要依赖于人工分析和调试，存在时间开销大、分析效率和精度低等问题。本项目研究基于模型检查的软件错误定位技术，即从程序中提取有限状态模型，采用模型检查和特征匹配等算法搜索和发现错误路径，从而提高软件错误定位的效率和精度，减少人工分析与调试的工作开销。本项目研究程序软件模型检查算法，解决基于事件驱动的软件系统的模型检查问题；提出过程间并发程序分析不可判定的必要条件解决该类程序的分析问题；本项目开发了Java源程序分析与模型检查系统(JAMCT)以及C模型提取工具C2Spin，自动化提取程序模型，并对程序进行模型检查，从而实现错误定位分析；对实际软件系统和网络协议开展实验分析，发现或重现了一些重要漏洞和缺陷。安全漏洞是一种特殊性质的错误，采用错误路径匹配，识别出可疑的潜在安全漏洞；本项目研究高性能错误路径匹配技术，提出了高效错误特征匹配算法，提高错误匹配的吞吐量和存储空间开销；提出了加速错误匹配的新型布鲁姆过滤器，通过减少错误路径匹配操作次数来提高其性能；提出了Linux下基于多路径的恶意行为规范自动挖掘算法。
结论摘要：
英文主题词Model Checking; Program Analysis; Software Model Extracting; Property Verification; Signature Matching
成果综合统计
期刊论文
会议论文
专利
获奖
著作
期刊论文
会议论文
相关项目
张大方的项目
