框架时序逻辑语言MSVL中面向对象机制的实现

doi:10.3969/j.issn.1001-2400.2010.03.031

J4 ›› 2010, Vol. 37 ›› Issue (3): 559-564+575.doi: 10.3969/j.issn.1001-2400.2010.03.031

• Original Articles • Previous Articles Next Articles

Implementation of objected-oriented mechanism in framed temporal logic language MSVL

WANG Xiao-bing^1,2,3;DUAN Zhen-hua¹

(1. Research Inst. of Computing Theory, Xidian Univ., Xi'an 710071， China;
2. Technology and State Key Lab. of Integrated Service Networks, Xidian Univ., Xi'an 710071， China;
3. State Key Lab. of Software Eng., Wuhan Univ., Wuhan 430072， China)

Received:2009-11-10 Online:2010-06-20 Published:2010-07-23
Contact: WANG Xiao-bing E-mail:xbwang@foxmail.com

Abstract

Abstract:

In order to overcome the shortages which the available temporal logic programming languages have such as existence of the frame problem, lack of object-oriented mechanisms and high formalization, the framed temporal logic language MSVL is defined, which includes some techniques such as new frame operator, await statement, nondeterministic choice statement,and object-oriented programming. The implementation plan for the interpreter for MSVL is proposed based on the normal form and normal form graph. An example for concurrent access to shared resources shows that MSVL is much more similar to high-level programming languages than other temporal logic languages, and that the implementation plan for the interpreter is workable.

Key words: framing, temporal logic, temporal logic language, object oriented programming, interpreter

WANG Xiao-bing;DUAN Zhen-hua. Implementation of objected-oriented mechanism in framed temporal logic language MSVL[J].J4, 2010, 37(3): 559-564+575.

References

[1]Miao Huaikou, Zeng Hongwei. Model Checking-based Verification of Web Application[C]//The Proceeding of ICECCS 2007. Auckland: IEEE Computer Society Press, 2007: 47-55.
[2]Moszkowski B C. Executing Temporal Logic Programs[M]. Cambridge: Cambridge University Press, 1986.
[3]Lamport L. The Temporal Logic of Actions[J]. ACM Trans on Programming Languages and Systems, 1994, 16(3): 872-923.
[4]Duan Z, Koutny M. A Framed Temporal Logic Programming Language[J]. Journal of Computer Science and Technology, 2004, 19(3): 341-351.
[5]唐稚松. 时序逻辑程序设计与软件工程[M]. 北京: 科学出版社, 1999.
[6]Duan Z, Yang X, Koutny M. Framed Temporal Logic Programming[J]. Science of Computer Programming, 2008, 70(1): 31-61.
[7]王小兵, 段振华. 框架投影时序逻辑程序设计语言中的指针[J]. 西安电子科技大学学报, 2008, 35(6): 1069-1074.
Wang Xiaobing, Duan Zhenhua. Pointers in Framing Projection Temporal Logic Programming Languages[J]. Journal of Xidian University, 2008, 35(6): 1069-1074.
[8]Mccarthy J, Hayes P J. Some Philosophical Problems from the Standpoint of Artificial Intelligence[M]. Edinburgh: Machine Intelligence 4, Edinburgh University Press, 1969.
[9]Ma Y, Duan Z, Wang X, et al. An Interpreter for Framed Tempura and Its Application[C]//The Proceeding of TASE 2007. Shanghai: IEEE Press, 2007: 251-260.
[10]王小兵, 段振华. 面向对象的时序逻辑语言[J]. 电子科技大学学报, 2009, 38(1): 97-101.
Wang Xiaobing, Duan Zhenhua. Object-Oriented Temporal Logic Language[J]. Journal of University of Electronic Science and Technology of China, 2009, 38(1): 97-101.
[11]Duan Z. Temporal Logic and Temporal Logic Programming[M]. Beijing: Science Press, 2006.
[12]王小兵. 面向对象MSVL语言及其在组合Web服务验证中的应用[D]. 西安: 西安电子科技大学, 2009.
[13]Duan Z, Tian C. A Unified Model Checking Approach with Projection Temporal Logic[C]//The Proceeding of ICFEM 2008. Berlin: Springer-Verlag, 2008: 167-186.
[14]Levine J. Flex & Bison: Text Processing Tools[M]. 1st ed. Sebastopol: O'Reilly Media, 2009.

Implementation of objected-oriented mechanism in framed temporal logic language MSVL

PDF (PC)

Like

Knowledge

Cited

Abstract

Cite this article

share this article

References

Related Articles 13

Metrics

Comments

Recommended 0

[1]	SHU Xinfeng,WANG Changtai,WANG Yan,ZHANG Lili. Propositional projection temporal logic based distributed model checking method [J]. Journal of Xidian University, 2020, 47(4): 39-47.
[2]	MAO Liqiang;HUANG Ying. Automated security analysis techniques in MANET routing protocols [J]. Journal of Xidian University, 2016, 43(6): 56-61.
[3]	MA Qian;DUAN Zhenhua. Automatic theorem proving technique for MSVL [J]. J4, 2016, 43(1): 75-81.
[4]	PANG Tao;DUAN Zhenhua;LIU Xiaofang. Symbolic model checking of Verilog programs with the propositional projection temporal logic [J]. J4, 2014, 41(2): 79-84.
[5]	ZHANG Nan;DUAN Zhenhua. Compositional verification of a carry-save adder with the propositional projection temporal logic [J]. J4, 2012, 39(5): 192-196.
[6]	YANG Chen;DUAN Zhenhua. Stutter-invariant propositional interval temporal logic [J]. J4, 2011, 38(2): 151-156.
[7]	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.
[8]	SHU Xin-feng;DUAN Zhen-hua. Axiomatization for the first-order projection temporal logic and formal verifications [J]. J4, 2009, 36(4): 680-729.
[9]	ZHANG Hai-bin;DUAN Zhen-hua. Model checking interval temporal logic [J]. J4, 2009, 36(2): 338-342.
[10]	WANG Xiao-bing;DUAN Zhen-hua. Pointers in framing projection temporal logic programming languages [J]. J4, 2008, 35(6): 1069-1074.
[11]	ZHANG Hai-bin;DUANG Zhen-hua. Model checking multirate hybrid systems [J]. J4, 2008, 35(1): 60-648.
[12]	LEI Li-hui;DUAN Zhen-hua. Modelling concurrent workflow with the extended interval temporal logic [J]. J4, 2007, 34(4): 673-680.
[13]	ZHANG Hai-bin;DUAN Zhen-hua. Decidability of the dense timed interval temporal logic [J]. J4, 2007, 34(3): 463-467.