投影时序逻辑的公理系统与形式验证
Axiomatization for the first-order projection temporal logic and formal verifications作者机构：西安电子科技大学计算理论与技术研究所陕西西安710071 西安邮电学院计算机系陕西西安710121
出 版 物：《西安电子科技大学学报》 (Journal of Xidian University)
年 卷 期：2009年第36卷第4期
页 面：680-685,729页
核心收录：
学科分类：0808[工学-电气工程] 0809[工学-电子科学与技术（可授工学、理学学位）] 08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论]
基 金：国家自然科学基金资助(60873018) 国家自然科学基金重点项目资助(60433010)
摘 要：为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统.利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,并使用公理系统完成系统性质的证明.最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用.
维普期刊数据库
同方期刊数据库