用于C语言程序验证的性质描述语言C-PDL  

C-PDL:a property description language of C based on specification patterns system

作　　者：左春华[1] 张广泉[1] 郭亮[2] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006 [2]中国科学院软件研究所,北京100080

出　　处：《苏州大学学报（自然科学版）》2007年第3期31-36,共6页Journal of Soochow University(Natural Science Edition)

基　　金：江苏省高校自然科学基金资助项目(05KJB520119);重庆市自然科学基金资助项目(CSTC;2006BB2259);中国科学院计算机科学国家重点实验室开放课题(SYSKF0303)

摘　　要：为了保证程序的正确性,可以先将程序抽象成模型,再采用模型检测技术对模型进行验证.模型检测工具只接受形式化的性质描述语言,而一般程序员很难正确地使用,因此,文章提出了半形式化的描述语言C-PDL,并介绍了采用C-PDL描述性质的验证系统.C-PDL采用时序逻辑语言XYZ/AE的语法结构,结合了C语言程序性质的特点,引入规范模式系统,其语法简单且描述能力强.另外,C-PDL表达式可以方便地转换成模型检测工具识别的各种时序逻辑公式.In order to assure the program correct,we can abstract the program to a model by program properties and then verify the model by Model Checkers.Model Checkers just accept formal description languages for properties.Programmers are hard to use.So the article brings forward the language C-PDL and explains the structure of the verifying system in C-PDL.C-PDL is the integration of XYZ/AE and the Specification Patterns System.And the C program＇s characters are taken into account.It＇s easy and powerful.The formulas in C-PDL can easily be translated into all kinds of temporal logic formulas that Model Checkers accept.

关 键 词：C-PDL 规范模式系统 程序性质 模型检测 XYZ/AE 

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