Please wait a minute...

Frontiers of Computer Science

Front. Comput. Sci.    2017, Vol. 11 Issue (5) : 762-785     DOI: 10.1007/s11704-016-6059-4
RESEARCH ARTICLE |
MSVL: a typed language for temporal logic programming
Xiaobing WANG, Cong TIAN(), Zhenhua DUAN, Liang ZHAO
ICTT and ISN Lab, Xidian University, Xi’an 710071, China
Download: PDF(1013 KB)  
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
Abstract

The development of types is an important but challenging issue in temporal logic programming. In this paper, we investigate how to formalize and implement types in the temporal logic programming language MSVL, which is an executable subset of projection temporal logic (PTL). Specifically, we extendMSVL with a few groups of types including basic data types, pointer types and struct types. On each type, we specify the domain of values and define some standard operations in terms of logic functions and predicates. Then, it is feasible to formalize statements of type declaration of program variables and statements of struct definitions as logic formulas. As the implementation of the theory, we extend the MSV toolkit with the support of modeling, simulation and verification of typedMSVL programs. Applications to the construction of AVL tree and ordered list show the practicality of the language.

Keywords type      temporal logic programming      MSVL      type declaration      struct definition     
Corresponding Authors: Cong TIAN   
Just Accepted Date: 16 November 2016   Online First Date: 07 June 2017    Issue Date: 26 September 2017
 Cite this article:   
Xiaobing WANG,Cong TIAN,Zhenhua DUAN, et al. MSVL: a typed language for temporal logic programming[J]. Front. Comput. Sci., 2017, 11(5): 762-785.
 URL:  
http://journal.hep.com.cn/fcs/EN/10.1007/s11704-016-6059-4
http://journal.hep.com.cn/fcs/EN/Y2017/V11/I5/762
Service
E-mail this article
E-mail Alert
RSS
Articles by authors
Xiaobing WANG
Cong TIAN
Zhenhua DUAN
Liang ZHAO
1 LiuS Y, ChenY T, NagoyaF, McDermid J A. Formal specificationbased inspection for verification of programs. IEEE Transactions on Software Engineering, 2012, 38(5): 1100–1122
doi: 10.1109/TSE.2011.102
2 LeeS U J, DobbieG, SunJ, Groves L. Theorem prover approach to semistructured data design. Formal Methods in System Design, 2010, 37(1): 1–60
doi: 10.1007/s10703-010-0099-4
3 LiuZ Y, PangJ, ZhangC Y. Design and formal verification of a CEM protocol with transparent TTP. Frontiers of Computer Science, 2013, 7(2): 279–297
doi: 10.1007/s11704-013-1268-6
4 DingZ J, JiangC J, ZhouM C. Design, analysis and verification of real-time systems based on time petri net refinement. ACM Transactions on Embedded Computing Systems, 2013, 12(1): 4
doi: 10.1145/2406336.2406340
5 FisherM. An Introduction to Practical Formal Methods Using Temporal Logic. Chichester: John Wiley & Sons, 2011
doi: 10.1002/9781119991472
6 GherghinaC, DavidC, QinS, Chin W N. Expressive program verification via structured specifications. International Journal on Software Tools for Technology Transfer, 2014, 16(4): 363–380
doi: 10.1007/s10009-014-0306-5
7 HoareC A R. Communicating sequential processes. Communications of the ACM, 1983, 26(1): 100–106
doi: 10.1145/357980.358021
8 MilnerR. A Calculus of Communicating Systems. Secaucus, NJ: Springer-Verlag New York, Inc., 1982
9 MilnerR, ParrowJ, WalkerD. A calculus of mobile processes, i. Information and Computation, 1992, 100(1): 1–40
doi: 10.1016/0890-5401(92)90008-4
10 PerrinD, PinJ É. Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics Series. London, San Diego (Calif.): Academic, 2004
11 DongJ S, LiuY, SunJ, Zhang X. Towards verification of computation orchestration. Formal Aspects of Computing, 2014, 26(4): 729–759
doi: 10.1007/s00165-013-0280-9
12 DuanZ H, YangX X, KoutnyM. Framed temporal logic programming. Science of Computer Programming, 2008, 70(1): 31–61
doi: 10.1016/j.scico.2007.09.001
13 DuanZ H, TianC.A unified model checking approach with projection temporal logic. In: Proceedings of the 10th International Conference on Formal Methods and Software Engineering. 2008, 167–186
doi: 10.1007/978-3-540-88194-0_12
14 YangX X, DuanZ H. Operational semantics of framed tempura. The Journal of Logic and Algebraic Programming, 2008, 78(1): 22–51
doi: 10.1016/j.jlap.2008.08.001
15 YangX X, DuanZ H, MaQ. Axiomatic semantics of projection temporal logic programs. Mathematical Structures in Computer Science, 2010, 20(5): 865–914
doi: 10.1017/S0960129510000241
16 ZhangN, DuanZ H, TianC, Du D Z. A formal proof of the deadline driven scheduler in PPTL axiomatic system. Theoretical Computer Science, 2014, 554: 229–253
doi: 10.1016/j.tcs.2013.12.014
17 ZhangP, DuanZ H, TianC. Simulation of CTCS-3 protocol with temporal logic programming. In: Proceedings of the 17th IEEE International Conference on Computer Supported Cooperative Work in Design. 2013, 72–77
doi: 10.1109/cscwd.2013.6580942
18 WangX B, SunT. A method based on MSVL for verification of the social network privacy policy. In: Proceedings of the International Workshop on Structured Object-Oriented Formal Language and Method. 2015, 118–131
19 ShiY, TianC, DuanZ H, Zhou M C. Model checking petri nets with MSVL. Information Sciences, 2016, 363: 274–291
doi: 10.1016/j.ins.2016.01.036
20 TianC, DuanZ H. Expressiveness of propositional projection temporal logic with star. Theoretical Computer Science, 2011, 412(18): 1729–1744
doi: 10.1016/j.tcs.2010.12.047
21 MannaZ, PnueliA. The Temporal Logic of Reactive and Concurrent Systems. New York, NY: Springer-Verlag New York, Inc., 1992
doi: 10.1007/978-1-4612-0931-7
22 LefticaruR, TudoseC, IpateF. Towards automated verification of P systems using Spin. In: de Castro L N, ed. Natural Computing for Simulation and Knowledge Discovery. IGI Global, 2014, 159–170
doi: 10.4018/978-1-4666-4253-9.ch010
23 WrightA. Type theory comes of age. Communications of the ACM, 2010, 53(2): 16–17
doi: 10.1145/1646353.1646361
24 WangS L, LongQ, QiuZ Y. Type Safety for FJ and FGJ. In: Proceedings of the International Colloquium on Theoretical Aspects of Computing. 2006, 257–271
doi: 10.1007/11921240_18
25 KeW, LiuZ M, WangS L, Zhao L. A graph-based generic type system for object-oriented programs. Frontiers of Computer Science, 2013, 7(1): 109–134
doi: 10.1007/s11704-012-1307-8
26 CousineauD, Doligez D, LamportL , MerzS, Ricketts D, VanzettoH . Tla+ proofs. In: Proceedings of the International Symposium on Formal Methods. 2012, 147–154
doi: 10.1007/978-3-642-32759-9_14
27 FisherM, HeppleA. Executing logical agent specifications. In: El Fallah Seghrouchni A, Dix J, Dastani M, et al., eds. Multi-Agent Programming: Languages, Tools and Applications. Boston, MA: Springer US, 2009, 1–27
doi: 10.1007/978-0-387-89299-3_1
28 LamportL. The PlusCal algorithm language. In: Proceedings of the International Colloquium on Theoretical Aspects of Computing. 2009, 36–60
doi: 10.1007/978-3-642-03466-4_2
29 FisherM, DennisL, WebsterM. Verifying autonomous systems. Communications of the ACM, 2013, 56(9): 84–93
doi: 10.1145/2500468.2494558
30 WangX B, DuanZ H, ZhaoL. Formalizing and implementing types in MSVL. In: Proceedings of the 3rd International Workshop on Structured Object-Oriented Formal Language and Method. 2014, 62–75
doi: 10.1007/978-3-319-04915-1_5
31 DuanZ H. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2006
32 GansnerE R, NorthS C. An open graph visualization system and its applications to software engineering. Software Practice and Experience, 2000, 30(11): 1203–1233
doi: 10.1002/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N
33 TianC, DuanZ H. Complexity of propositional projection temporal logic with star. Mathematical Structures in Computer Science, 2009, 19(1): 73–100
doi: 10.1017/S096012950800738X
34 KnuthD E. The Art of Computer Programming, Vol 3: Sorting and Searching. 2nd ed. Redwood City, CA: AddisonWesley Longman Publishing Co., Inc., 1998
[1] FCS-0762-16059-CT_suppl_1 Download
Related articles from Frontiers Journals
[1] Yuan LI, Yuhai ZHAO, Guoren WANG, Xiaofeng ZHU, Xiang ZHANG, Zhanghui WANG, Jun PANG. Finding susceptible and protective interaction patterns in large-scale genetic association study[J]. Front. Comput. Sci., 2017, 11(3): 541-554.
[2] Samir ZEGHLACHE,Djamel SAIGAA,Kamel KARA. Fault tolerant control based on neural network interval type-2 fuzzy sliding mode controller for octorotor UAV[J]. Front. Comput. Sci., 2016, 10(4): 657-672.
[3] Xiaoxiao YANG,Yu ZHANG,Ming FU,Xinyu FENG. A temporal programming model with atomic blocks based on projection temporal logic[J]. Front. Comput. Sci., 2014, 8(6): 958-976.
[4] Pushpinder SINGH. Some new distance measures for type-2 fuzzy sets and distance measure based ranking for group decision making problems[J]. Front. Comput. Sci., 2014, 8(5): 741-752.
[5] Le DONG,Wenling WU,Shuang WU,Jian ZOU. Known-key distinguishers on type-1 Feistel scheme and near-collision attacks on its hashing modes[J]. Front. Comput. Sci., 2014, 8(3): 513-525.
[6] Changpeng ZHU, Yinliang ZHAO, Bo HAN, Qinghua ZENG, Ying MA. Runtime support for type-safe and context-based behavior adaptation[J]. Front. Comput. Sci., 2014, 8(1): 17-32.
[7] Qin SHU, Zongyan QIU, Shuling WANG. Confinement framework for encapsulating objects[J]. Front Comput Sci, 2013, 7(2): 236-256.
[8] Wei KE, Zhiming LIU, Shuling WANG, Liang ZHAO. A graph-based generic type system for object-oriented programs[J]. Front Comput Sci, 2013, 7(1): 109-134.
[9] Baojian HUA. Static typing for a substructural lambda calculus[J]. Front Comput Sci Chin, 2011, 5(3): 369-380.
[10] Ruixuan LI, Kunmei WEN, Xiwu GU, Yuhua LI, Xiaolin SUN, Bing LI. Type-2 fuzzy description logic[J]. Front Comput Sci Chin, 2011, 5(2): 205-215.
[11] Shuling WANG, Qin SHU, Yijing LIU, Zongyan QIU, . A semantic model of confinement and Locality Theorem[J]. Front. Comput. Sci., 2010, 4(1): 28-46.
[12] ZHAO Yuzhong, XU Yun, ZHANG Qiangfeng, CHEN Guoliang. An overview of the haplotype problems and algorithms[J]. Front. Comput. Sci., 2007, 1(3): 272-282.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed