Model Check What You Can, Runtime Verify the Rest

Citations Over Time

Abstract

Model checking and runtime verification are pillars of formal verification but for the most part are used independently. In this position paper we argue that the formal verification community would be well-served by developing theory, algorithms, implementations, and applications that combine model checking and runtime verification into a single, seamless technology. This technology would allow system developers to carefully choose the appropriate balance between offline verification of expressive properties (model checking) and online verification of important parts of the system's state space (runtime verification). We present several realistic examples where such technology appears necessary and a preliminary formalization of the idea.

Related Papers

• → Generic System Verilog Universal Verification Methodology Based Reusable Verification Environment for Efficient Verification of Image Signal Processing IPS/SOCS(2012)2 cited
• → Verification Runtime Analysis: Get the Most Out of Partial Verification(2020)2 cited
• A Study on the Verification of System-On-a-Chip(2003)
• Function Verification Platform Design for Switch Controller(2006)
• → Generic System Verilog Universal Verification Methodology based Reusable\n Verification Environment for Efficient Verification of Image Signal\n Processing IPs/SoCs(2013)