A compiler for MSVL and its applications

被引：19
|
作者：
Yang, Kai
Duan, Zhenhua [1 ]
Tian, Cong [1 ]
Zhang, Nan
机构：
[1] Xidian Univ, ICTT, Xian 710071, Shaanxi, Peoples R China
来源：
THEORETICAL COMPUTER SCIENCE | 2018年 / 749卷
基金：
中国国家自然科学基金;
关键词：
MSVL; Model checking; Compiler; Verification; Al planning; DYNAMIC THERMAL MANAGEMENT; TEMPORAL LOGIC; VERIFICATION;
D O I：
10.1016/j.tcs.2017.07.032
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper, we present a method for implementing a compiler called MC for Modeling, Simulation and Verification Language (MSVL) based on LLVM. MC accepts a well formed MSVL program as input and generates an executable binary code. Different from other compilers, MC can be used not only to compile programs but also to model and verify programs. The details of implementation including the architecture design, lexical, syntactic and semantic analysis, as well as preprocessing and scheduling algorithms. Besides, we show MC can be utilized as an infrastructure for Artificial Intelligence (Al) planning. Several examples are given to show applications of MC in modeling and verifying programs, as well as Al planning. (C) 2017 Elsevier B.V. All rights reserved.
引用
收藏
页码：2 / 16
页数：15
相关论文
共 50 条
  • [1] DAG-Based Formal Modeling of Spark Applications with MSVL
    Fan, Kaixuan
    Wang, Meng
    INFORMATION, 2023, 14 (12)
  • [2] Translating Xd-C programs to MSVL programs
    Wang, Meng
    Tian, Cong
    Zhang, Nan
    Duan, Zhenhua
    Yao, Chenguang
    THEORETICAL COMPUTER SCIENCE, 2020, 809 : 430 - 465
  • [3] A Framework Based on MSVL for Verifying Probabilistic Properties in Social Networks
    Wang, Xiaobing
    Ren, Liyuan
    Zhao, Liang
    Shu, Xinfeng
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2017, 2018, 10795 : 133 - 147
  • [4] Model Checking MSVL Programs Based on Dynamic Symbolic Execution
    Duan, Zhenhua
    Bu, Kangkang
    Tian, Cong
    Zhang, Nan
    COMPUTING AND COMBINATORICS, 2015, 9198 : 521 - 533
  • [5] A structural transformation from p-π to MSVL
    Luo, Ling
    Duan, Zhenhua
    Tian, Cong
    Wang, Xiaobing
    JOURNAL OF COMBINATORIAL OPTIMIZATION, 2015, 29 (01) : 308 - 329
  • [6] Model Checking Python']Python Programs with MSVL
    Shu, Xinfeng
    Gao, Fengyun
    Gao, Weiran
    Zhang, Lili
    Wang, Xiaobing
    Zhao, Liang
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD (SOFL+MSVL 2019), 2020, 12028 : 205 - 224
  • [7] Translation from Workflow Nets to MSVL
    Shi, Ya
    Duan, Zhenhua
    Tian, Cong
    FORMAL METHODS AND SOFTWARE ENGINEERING, 2013, 8144 : 281 - 296
  • [8] MSVL: a typed language for temporal logic programming
    Wang, Xiaobing
    Tian, Cong
    Duan, Zhenhua
    Zhao, Liang
    FRONTIERS OF COMPUTER SCIENCE, 2017, 11 (05) : 762 - 785
  • [9] Extending MSVL with Semaphore
    Shu, Xinfeng
    Duan, Zhenhua
    COMPUTING AND COMBINATORICS, COCOON 2016, 2016, 9797 : 599 - 610
  • [10] Object-Oriented MSVL and Its Application
    Wang, Xiaobing
    Duan, Zhenhua
    Tian, Cong
    Zhang, Haibin
    FOURTH INTERNATIONAL CONFERENCE ON MACHINE VISION (ICMV 2011): MACHINE VISION, IMAGE PROCESSING, AND PATTERN ANALYSIS, 2012, 8349
12345