MSVL语言的公理系统的程序验证

doi:10.3969/j.issn.1001-2400.2010.01.017

J4 ›› 2010, Vol. 37 ›› Issue (1): 96-101.doi: 10.3969/j.issn.1001-2400.2010.01.017

MSVL语言的公理系统的程序验证

杨潇潇;段振华

(西安电子科技大学计算理论与技术研究所，陕西西安 710071)

收稿日期:2008-12-10 出版日期:2010-02-20 发布日期:2010-03-29
通讯作者: 杨潇潇
作者简介:杨潇潇(1981-)，女，西安电子科技大学博士研究生，E-mail: yang_xiao@126.com．
基金资助:
国家自然科学基金资助项目(60873018);国家自然科学基金重点资助项目(60433010)

Verification of programs based on an axiom system for the MSVL language

YANG Xiao-xiao;DUAN Zhen-hua

(Research Inst. of Computing Theory & Technology, Xidian Univ., Xi'an 710071， China)

Received:2008-12-10 Online:2010-02-20 Published:2010-03-29
Contact: YANG Xiao-xiao

摘要/Abstract

摘要：

MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言．为了证明区间时序逻辑程序的正确性，提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则，以及将程序从一个状态转换到另一个状态的区间公理和区间推演规则．最后给出验证实例说明基于该公理系统的程序验证方法．

关键词: 形式验证, 时序逻辑, 正则形, 安全性, 公理系统

Abstract:

The language MSVL is an interval temporal logic programming language. It can be used for the purpose of modeling, simulation and verification of programs. To prove the correctness of interval temporal logic programs, we present a proof system for MSVL. To do so, a set of state axioms and state inference rules is given to deduce a program into its normal form. In addition, a set of axioms and inference rules over intervals is formalized to transform a program from one state to another. Finally, an example is given to illustrate how the axiom system works.

Key words: verification, temporal logic, normal form, safety, axiom system

杨潇潇;段振华. MSVL语言的公理系统的程序验证[J]. J4, 2010, 37(1): 96-101.

YANG Xiao-xiao;DUAN Zhen-hua. Verification of programs based on an axiom system for the MSVL language[J]. J4, 2010, 37(1): 96-101.

参考文献

［1］Manna Z, Pnueli A. Temporal Logic of Reactive and Concurrent Systems［M］. Berlin/Heidelberg: Springer-Verlag, 1992.
［2］Barringer H, Fisher M, Gabbay D, et al. METATEM: a Framework for Programming in Temporal Logic［C］//Proceeding REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formulisms, Correctness, Mook, LNCS 430. Netherlands: Springer, 1989: 94-129.
［3］Fujita M, Kono S, Tanaka H, et al. Tokio: Logic Programming Language Based on Temporal Logic and Its Compilation to PROLOG［C］//Third International Conference on Logic Programming, LNCS 225. London: Springer, 1986: 695-709.
［4］Lamport L. The Temporal Logic of Actions［J］. ACM Transactions on Programming Languages and Systems, 1994(16): 872-923.
［5］Moszkowski B. Executing Temporal Logic Programs［D］. Cambridge: Cambridge University Press, 1986.
［6］Tang C S. A Temporal Logic Language Oriented Toward Software Engineering—Introduction to XYZ System (I) ［J］. Chinese Journal of Advanced Software Research, 1994, 1(1): 1-27.
［7］Duan Z, Yang X, Koutny M. Framed Temporal Logic Programming ［J］. Science of Computer Programming, 2008, 70(1): 31-61.
［8］雷丽晖, 段振华. 使用扩展区间时序逻辑为并发工作流建模［J］. 西安电子科技大学学报, 2007, 34(4): 673-680.
Lei Lihui, Duan Zhenhua. Modelling Concurrent Workflow with the Extended Interval Temporal Logic［J］. Journal of Xidian University, 2007, 34(4): 673-680.
［9］Yang Xiaoxiao, Duan Zhenhua. Operational Semantics of Framed Temporal Logic Programming Languages［J］. Journal of Logic and Algebraic Programming, 2008, 78(1): 22-51.
［10］Duan Z. An Extended Interval Temporal Logic and A Framing Technique for Temporal Logic Programming ［D］. Glasgow: University of Newcastle Upon Tyne, 1996.
［11］Duan Z. Temporal Logic and Temporal Logic Programming ［M］. Beijing: Science Press, 2006.
［12］Hoare C A R. An Axiomatic Basis for Computer Programming［J］. Communications of ACM, 1969, 12(10): 576-583.

[1]	舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.
[2]	丁明,张书玲,张琛,张军. 一种航空电子系统安全性需求验证方法[J]. 西安电子科技大学学报, 2019, 46(3): 66-73.
[3]	马倩;段振华. MSVL程序的自动定理证明方法[J]. J4, 2016, 43(1): 75-81.
[4]	李昊星;李凤华;宋承根;苏铓;刘歆. 支持多关键字的可搜索公钥加密方案[J]. J4, 2015, 42(5): 20-25.
[5]	逄涛;段振华;刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. J4, 2014, 41(2): 79-84.
[6]	张南;段振华. 进位保留加法器的命题投影时序逻辑组合验证[J]. J4, 2012, 39(5): 192-196.
[7]	李慧贤. 轻量级RFID双向认证协议设计与分析[J]. J4, 2012, 39(1): 172-178.
[8]	杨琛;段振华. 支持Stutter-不变性的命题区间时序逻辑[J]. J4, 2011, 38(2): 151-156.
[9]	王小兵;段振华. 框架时序逻辑语言MSVL中面向对象机制的实现[J]. J4, 2010, 37(3): 559-564+575.
[10]	金军;舒红平. 一种基于元胞自动机的安全多重图像水印算法[J]. J4, 2010, 37(1): 174-180.
[11]	邱钢;王宏;肖鸿;肖国镇. 两个前向安全盲签名体制的安全性分析[J]. J4, 2010, 37(1): 107-112+147.
[12]	舒新峰;段振华. 投影时序逻辑的公理系统与形式验证[J]. J4, 2009, 36(4): 680-729.
[13]	张海宾;段振华. 区间时序逻辑的模型检查 [J]. J4, 2009, 36(2): 338-342.
[14]	王小兵;段振华. 框架投影时序逻辑程序设计语言中的指针 [J]. J4, 2008, 35(6): 1069-1074.
[15]	张海宾;段振华. 多速率混合系统的模型检查 [J]. J4, 2008, 35(1): 60-648.

MSVL语言的公理系统的程序验证

Verification of programs based on an axiom system for the MSVL language

PDF (PC)

赞

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 10