投影时序逻辑的公理系统与形式验证     投影时序逻辑  公理系统  形式化方法       font style='font-size:12px;'> 2009/12/9

为了采用定理证明的方法对并发及交互式系统进行验证，提出了一阶投影时序逻辑的公理系统．利用投影时序逻辑既可描述待验证系统性质和规范，又可描述其实现模型的特点，在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述，并使用公理系统完成系统性质的证明．最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用．

存档文本 存档附件 原文地址 文献传递