科研之友
微信
新浪微博
Facebook
分享链接
摘要
时序逻辑程序设计语言能被用于验证C、Verilog/VHDL程序的正确性.但目前时序逻辑程序设计语言程序只能纯手工进行定理证明.针对该问题提出了一种基于定理证明器原型验证系统的时序逻辑程序设计语言程序的自动定理证明方法.该方法首先使用原型验证系统规范语言描述时序逻辑程序设计语言的语法和语义,使得原型验证系统能够正确识别时序逻辑程序设计语言程序;然后使用原型验证系统规范语言描述时序逻辑程序设计语言的公理系统和待证定理;最后输入原型验证系统命令调用原型验证系统证明器来进行时序逻辑程序设计语言程序的推演证明.在证明过程中,细节被原型验证系统自动地证明,使得人工仅在复杂的步骤上指导控制,从而实现半自动地验证时序逻辑程序设计语言程序,简化了该定理的证明过程.
- 出版日期2016
- 单位西安电子科技大学
