An overview of the MOP runtime verification framework

被引:141
|
作者
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, 201 N Goodwin Ave., Urbana, IL 61801, United States
关键词
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
    ACM SIGPLAN NOTICES, 2007, 42 (10) : 569 - 588
  • [2] MOP: An Efficient and Generic Runtime Verification Framework
    Chen, Feng
    Rosu, Grigore
    OOPSLA: 22ND INTERNATIONAL CONFERENCE ON OBJECT-ORIENTED PROGRAMMING, SYSTEMS, LANGUAGES, AND APPLICATIONS, PROCEEDINGS, 2007, : 569 - 588
  • [3] MOP: An efficient and generic runtime verification framework
    University of Illinois, Urbana-Champaign, United States
    Proc Conf Object Orient Program Syst Lang Appl OOPSLA, (569-588):
  • [4] An Algebraic Framework for Runtime Verification
    Jaksic, Stefan
    Bartocci, Ezio
    Grosu, Radu
    Nickovic, Dejan
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2018, 37 (11) : 2233 - 2243
  • [5] A Formal Verification Framework for Runtime Assurance
    Slagel, J. Tanner
    White, Lauren M.
    Dutle, Aaron
    Munoz, Cesar A.
    Crespo, Nicolas
    NASA FORMAL METHODS, NFM 2024, 2024, 14627 : 322 - 328
  • [6] An Overview of the Runtime Verification Tool Java PathExplorer
    Klaus Havelund
    Grigore Roşu
    Formal Methods in System Design, 2004, 24 : 189 - 215
  • [7] A Runtime Verification Framework for Control System Simulation
    Ciraci, Selim
    Fuller, Jason C.
    Daily, Jeff
    Malchmalbaf, Atefe
    Callahan, David
    2014 IEEE 38TH ANNUAL INTERNATIONAL COMPUTERS, SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2014, : 75 - 84
  • [8] PCH Framework for IP Runtime Security Verification
    Guo, Xiaolong
    Dutta, Raj Gautam
    He, Jiaji
    Jin, Yier
    PROCEEDINGS OF THE 2017 ASIAN HARDWARE ORIENTED SECURITY AND TRUST SYMPOSIUM (ASIANHOST), 2017, : 79 - 84
  • [9] Model-based Runtime Verification Framework
    Zhao, Yuhong
    Rammig, Franz
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 253 (01) : 179 - 193
  • [10] An overview of the runtime verification tool Java']Java PathExplorer
    Havelund, K
    Rosu, G
    FORMAL METHODS IN SYSTEM DESIGN, 2004, 24 (02) : 189 - 215