摘要
针对现今软件使用逻辑错误的问题越来越多的出现,提出了对最流行最普遍的编程语言——C语言子集的模型检测方法的研究.采用基于Verds工具的模型,运用C语言子集转化成Verds模型的算法,结合Verds工具和MAGIC工具实现模型检测.引入反例引导的抽象精化方法使模型检测解决状态爆炸的问题.
In problem of software logic errors, nowadays it emerges more and more. The paper presents the research for model checking methods of C language, that it is the most popular and general programming languages. The model checking based on Verds tools, using C language subset into Verds model algorithm, combined with the Verds tools and MAGIC tools. Introducing the counterexample guided abstraction refinement （CEGAR） method to solve the problem of state explosion.
出处
《计算机系统应用》
2013年第11期19-25,18,共8页
Computer Systems & Applications
基金
国家科技重大专项(2012ZX01039-004)
