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 [J].

Allan, C ;

Avgustinov, P ;

Christensen, AS ;

Hendren, L ;

Kuzins, S ;

Lhoták, O ;

de Moor, O ;

Sereni, D ;

Sittampalam, G ;

Tibble, 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 [J].

Chen, Feng ;

Meredith, Patrick O'Neil ;

Jin, Dongyun ;

Rosu, Grigore .

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 [J].

Chen, Zhe ;

Wei, Ou ;

Huang, Zhiqiu ;

Xi, Hongwei .

PROCEEDINGS 2015 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, 2015, :63-70

[7] Model checking aircraft controller software: a case study [J].

Chen, Zhe ;

Gu, Yi ;

Huang, Zhiqiu ;

Zheng, Jun ;

Liu, Chang ;

Liu, Ziyi .

SOFTWARE-PRACTICE & EXPERIENCE, 2015, 45 (07) :989-1017

[8] Control Systems on Automata and Grammars [J].

Chen, Zhe .

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 [J].

Coady, Y ;

Kiczales, G ;

Feeley, M ;

Hutchinson, N ;

Ong, JS .

COMMUNICATIONS OF THE ACM, 2001, 44 (10) :79-82

← 1 2 3 →