【摘 要】
：
为了保证程序的正确性,可以先将程序抽象成模型,再采用模型检测技术对模型进行验证.模型检测工具只接受形式化的性质描述语言,而一般程序员很难正确地使用,因此,文章提出了半
【机 构】
：
苏州大学计算机科学与技术学院,中国科学院软件研究所
【基金项目】
：
江苏省高校自然科学基金资助项目（05KJB520119）,重庆市自然科学基金资助项目（CSTC,2006BB2259）,中国科学院计算机科学国家重点实验室开放课题（SYSKF0303）.
论文部分内容阅读
为了保证程序的正确性,可以先将程序抽象成模型,再采用模型检测技术对模型进行验证.模型检测工具只接受形式化的性质描述语言,而一般程序员很难正确地使用,因此,文章提出了半形式化的描述语言C-PDL,并介绍了采用C-PDL描述性质的验证系统.C-PDL采用时序逻辑语言XYZ/AE的语法结构,结合了C语言程序性质的特点,引入规范模式系统,其语法简单且描述能力强.另外,C-PDL表达式可以方便地转换成模型检测工具识别的各种时序逻辑公式.
其他文献
采用循环伏安法和交流阻抗法对由十八烷基硫醇和半胱胺在金电极上形成的混合自组装膜进行表征.结果表明,致密单层膜的形成有效阻碍了Fe（CN）63-探针分子的通过;参考点腐蚀模型,
粗糙集的概念被推广到模糊近似空间上,给出了上近似、下近似的新定义,并获得上近似和下近似的计算解析式.
介绍了时间自动机形式模型，在此基础上给出了时间自动机网络的形式语法和语义，然后给出一种基于时间自动机网络的实时系统形式化验证方法，并采用基于时间自动机网络的模型检测工
先证明高度是h的准红黑树至少有2┌h/2┐＋2└h/2┘-2个结点，再证明有n个结点的准红黑树的高度至多是2└log2（n＋2）┘＋└log2（n＋2）-└log2（n＋2）┘/log2 3-1┘-2，最后证明有n个结点的红黑树的
测定了Fe73Cu1Nb1.5V2Si13.5B9纳米微晶带纵向驱动磁阻抗的相频曲线和不同频率的相位随外磁场变化的曲线.从相频曲线的峰位可确定出样品趋肤效应的临界频率.从临界频率随外磁