Parametric Runtime Verification of C Programs

被引：13
作者：
Chen, Zhe [1 ,2 ]
Wang, Zhemin [1 ]
Zhu, Yunlong [1 ]
Xi, Hongwei [3 ]
Yang, Zhibin [1 ]
机构：
[1] Nanjing Univ Aeronaut & Astronaut, Coll Comp Sci & Technol, 29 Jiangjun Ave, Nanjing 211106, Jiangsu, Peoples R China
[2] Collaborat Innovat Ctr Novel Software Technol & I, Nanjing, Jiangsu, Peoples R China
[3] Boston Univ, Dept Comp Sci, 111 Cummington St, Boston, MA 02215 USA
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016) | 2016年 / 9636卷
基金：
中国国家自然科学基金;
关键词：
D O I：
10.1007/978-3-662-49674-9_17
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Many runtime verification tools are built based on Aspect-Oriented Programming (AOP) tools, most often AspectJ, a mature implementation of AOP for Java. Although already popular in the Java domain, there is few work on runtime verification of C programs via AOP, due to the lack of a solid language and tool support. In this paper, we propose a new general purpose and expressive language for defining monitors as an extension to the C language, and present our tool implementation of the weaver, the Movec compiler, which brings fully-fledged parametric runtime verification support into the C domain.
引用
收藏
页码：299 / 315
页数：17
相关论文
共 22 条
  • [1] Adding trace matching with free variables to AspectJ
    Allan, C
    Avgustinov, P
    Christensen, AS
    Hendren, L
    Kuzins, S
    Lhoták, O
    de Moor, O
    Sereni, D
    Sittampalam, G
    Tibble, J
    [J]. ACM SIGPLAN NOTICES, 2005, 40 (10) : 345 - 364
  • [2] Avgustinov P, 2007, OOPSLA: 22ND INTERNATIONAL CONFERENCE ON OBJECT-ORIENTED PROGRAMMING, SYSTEMS, LANGUAGES, AND APPLICATIONS, PROCEEDINGS, P589
  • [3] Efficient Formalism-Independent Monitoring of Parametric Properties
    Chen, Feng
    Meredith, Patrick O'Neil
    Jin, Dongyun
    Rosu, Grigore
    [J]. 2009 IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 383 - 394
  • [4] Chen F, 2009, LECT NOTES COMPUT SC, V5505, P246, DOI 10.1007/978-3-642-00768-2_23
  • [5] Chen F, 2007, OOPSLA: 22ND INTERNATIONAL CONFERENCE ON OBJECT-ORIENTED PROGRAMMING, SYSTEMS, LANGUAGES, AND APPLICATIONS, PROCEEDINGS, P569
  • [6] Formal Semantics of Runtime Monitoring, Verification, Enforcement and Control
    Chen, Zhe
    Wei, Ou
    Huang, Zhiqiu
    Xi, Hongwei
    [J]. PROCEEDINGS 2015 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, 2015, : 63 - 70
  • [7] Model checking aircraft controller software: a case study
    Chen, Zhe
    Gu, Yi
    Huang, Zhiqiu
    Zheng, Jun
    Liu, Chang
    Liu, Ziyi
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 2015, 45 (07) : 989 - 1017
  • [8] Control Systems on Automata and Grammars
    Chen, Zhe
    [J]. COMPUTER JOURNAL, 2015, 58 (01) : 75 - 94
  • [9] Coady Y., 2001, Software Engineering Notes, V26, P88, DOI 10.1145/503271.503223
  • [10] Structuring operating system aspects
    Coady, Y
    Kiczales, G
    Feeley, M
    Hutchinson, N
    Ong, JS
    [J]. COMMUNICATIONS OF THE ACM, 2001, 44 (10) : 79 - 82
123