An overview of the MOP runtime verification framework

被引：143

作者：

Meredith, Patrick O'Neil ^{[1
]}

Jin, Dongyun ^{[1
]}

Griffith, Dennis ^{[1
]}

Chen, Feng ^{[1
]}

Roşu, Grigore ^{[1
]}

机构：

[1] Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL 61801

来源：

International Journal on Software Tools for Technology Transfer | 2012年 / 14卷 / 03期

基金：

美国国家科学基金会; 美国国家航空航天局;

关键词：

Monitoring; Real time systems; Runtime verification; Testing;

D O I：

10.1007/s10009-011-0198-6

中图分类号：

学科分类号：

摘要：

This article gives an overview of the, monitoring oriented programming framework (MOP). In MOP, runtime monitoring is supported and encouraged as a fundamental principle for building reliable systems. Monitors are automatically synthesized from specified properties and are used in conjunction with the original system to check its dynamic behaviors. When a specification is violated or validated at runtime, user-defined actions will be triggered, which can be any code, such as information logging or runtime recovery. Two instances of MOP are presented: JavaMOP (for Java programs) and BusMOP (for monitoring PCI bus traffic). The architecture of MOP is discussed, and an explanation of parametric trace monitoring and its implementation is given. A comprehensive evaluation of JavaMOP attests to its efficiency, especially in comparison with similar systems. The implementation of BusMOP is discussed in detail. In general, BusMOP imposes no runtime overhead on the system it is monitoring. © 2011 Springer-Verlag.

引用

页码：249 / 289

页数：40

共 54 条

[1]

Abercrombie P., Karaorman M., jContractor: Bytecode instrumentation techniques for implementing DBC in Java, Runtime Verification (RV'02), ENTCS, 70, (2002)

[2]

Aho A.V., Sethi R., Ullman J.D., Compilers, Principles, Techniques, and Tools, pp. 215-246, (1986)

[3]

Allan C., Avgustinov P., Christensen A.S., Hendren L.J., Kuzins S., Lhotak O., de Moor O., Sereni D., Sittampalam G., Tibble J., Adding trace matching with free variables to AspectJ, Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'05), pp. 345-364, (2005)

[4]

Alur R., Etessami K., Madhusudan P., A temporal logic of nested calls and returns, Tools and Algorithms For the Construction and Analysis of Systems (TACAS'04), 2988, pp. 467-481, (2004)

[5]

Avgustinov P., Tibble J., de Moor O., Making trace monitors feasible, Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'07), pp. 589-608, (2007)

[6]

Barnett M., Leino K.R.M., Schulte W., The Spec# programming system: An overview, Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS'04), 3362, pp. 49-69, (2004)

[7]

Runtime Verification (RV'05), ENTCS, 144, (2005)

[8]

Barringer H., Goldberg A., Havelund K., Sen K., Rule-Based Runtime Verification, Verification, Model Checking, and Abstract Interpretation (VMCAI'04), LNCS, 2937, pp. 44-57, (2004)

[9]

Barringer H., Rydeheard D., Havelund K., Rule systems for run-time monitoring: From EAGLE to RULER, J. Logic Comput, (2008)

[10]

Bartetzko D., Fischer C., Moller M., Wehrheim H., Jass-Java with Assertions, Runtime Verification (RV'01), 55, pp. 103-117, (2001)

← 1 2 3 4 5 6 →