一种软件模型检测方法及其原型系统  

A Software Model Checking Mothed and Its Prototype System

作　　者：顾滨兵[1] 

机构地区：[1]中国人民解放军91413部队

出　　处：《微计算机应用》2010年第11期39-46,共8页Microcomputer Applications

基　　金：国家自然科学基金(60473003)资助课题

摘　　要：模型检测是一种重要的自动化验证技术,使用该技术来保证软件安全性和可靠性已成为近年来的一个研究热点。提出的软件模型检测方法及实现的原型系统,在模型检测技术理论和方法的基础上,重点介绍该系统的基本思路和框架,并通过模型检测技术在软件质量保证领域方面的应用,结合中间代码转换、程序分析技术和基于SAT方法的模型检测技术,能够进行软件特别是并行程序的验证。Model checking is an important automated verification technology,and how to use the technology to ensure security and reliability of software has become a hot research topic in recent years.A software model checking mothed and its realized prototype sytem have been proposed on the base of the theory and motheds of model checking,and through applications of model checking technology in the field of software quality assurance,it can validate software,especially parallel program,by combining with intermediate code conversion,program analysis technology and model checking based on SAT solving implement.

关 键 词：模型检测 软件验证 程序分析技术 SAT方法 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]