An overview of the MOP runtime verification framework

被引:141
|
作者
Patrick O’Neil Meredith
Dongyun Jin
Dennis Griffith
Feng Chen
Grigore Roşu
机构
[1] University of Illinois at Urbana-Champaign,Department of Computer Science
关键词
Runtime verification; Monitoring; Testing; Real time systems;
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.
引用
收藏
页码:249 / 289
页数:40
相关论文
共 50 条
  • [1] MOP: An efficient and generic runtime verification framework
    Chen, Feng
    Rosu, Grigore
    [J]. ACM SIGPLAN NOTICES, 2007, 42 (10) : 569 - 588
  • [2] MOP: An Efficient and Generic Runtime Verification Framework
    Chen, Feng
    Rosu, Grigore
    [J]. OOPSLA: 22ND INTERNATIONAL CONFERENCE ON OBJECT-ORIENTED PROGRAMMING, SYSTEMS, LANGUAGES, AND APPLICATIONS, PROCEEDINGS, 2007, : 569 - 588
  • [3] An Algebraic Framework for Runtime Verification
    Jaksic, Stefan
    Bartocci, Ezio
    Grosu, Radu
    Nickovic, Dejan
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2018, 37 (11) : 2233 - 2243
  • [4] A Formal Verification Framework for Runtime Assurance
    Slagel, J. Tanner
    White, Lauren M.
    Dutle, Aaron
    Munoz, Cesar A.
    Crespo, Nicolas
    [J]. NASA FORMAL METHODS, NFM 2024, 2024, 14627 : 322 - 328
  • [5] An Overview of the Runtime Verification Tool Java PathExplorer
    Klaus Havelund
    Grigore Roşu
    [J]. Formal Methods in System Design, 2004, 24 : 189 - 215
  • [6] A Runtime Verification Framework for Control System Simulation
    Ciraci, Selim
    Fuller, Jason C.
    Daily, Jeff
    Malchmalbaf, Atefe
    Callahan, David
    [J]. 2014 IEEE 38TH ANNUAL INTERNATIONAL COMPUTERS, SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2014, : 75 - 84
  • [7] PCH Framework for IP Runtime Security Verification
    Guo, Xiaolong
    Dutta, Raj Gautam
    He, Jiaji
    Jin, Yier
    [J]. PROCEEDINGS OF THE 2017 ASIAN HARDWARE ORIENTED SECURITY AND TRUST SYMPOSIUM (ASIANHOST), 2017, : 79 - 84
  • [8] Model-based Runtime Verification Framework
    Zhao, Yuhong
    Rammig, Franz
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 253 (01) : 179 - 193
  • [9] An overview of the runtime verification tool Java']Java PathExplorer
    Havelund, K
    Rosu, G
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2004, 24 (02) : 189 - 215
  • [10] Towards a Runtime Verification Framework for the Ada Programming Language
    Pedro, Andre de Matos
    Pereira, David
    Pinho, Luis Miguel
    Pinto, Jorge Sousa
    [J]. RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE 2014, 2014, 8454 : 58 - 73