Enabling Practical Model Checking of Temporal Properties for Large-scale Systems from Design Time to Runtime

Model checking is the problem of checking that a system satisfies a formal specification and has successfully verified (or found bugs in) a wide range of real-world systems and algorithms. Temporal logics, such as Linear Temporal Logic (LTL) and Mission-time LTL (MLTL), are particularly powerful formal specification languages, demonstrating their usefulness in verifying models captured using languages such as SMV and System Verilog. A persistent challenge in applying model checking to large-scale, real-world systems is scalability; as systems grow larger and more complex, existing algorithms struggle to keep pace. We address model checking scalabiity at two stages of system development: design time and runtime. At design time, model checking verifies that every possible execution of the system satisfies a specification. At runtime, model checking verifies that the current execution of the system satisfies a specification. 

The model-checking-research ecosystem is currently disconnected and contains many proprietary, closed-source tools, making comparison between disparate tools and algorithms challenging. Current languages to unify this ecosystem (e.g., BTOR2) are insufficient for research beyond finite-state, hardware systems. We address these practical problems by presenting a novel research-enabling intermediate language, MoXI, for defining models and specifications for model checking. We also validate the language’s ability to sufficiently capture existing model checking problems by implementing a translation toolchain from a high-level modeling language (SMV) to a low-level, bit-precise language (BTOR2) via MoXI.  Experiments show that model checkers using the translated BTOR2 models perform competitively with the SMV-native tool nuXmv.

Beyond practical research challenges, algorithmic challenges persist in model checking as well, especially for LTL properties of infinite-state systems. Infinite-state systems are especially suitable for modeling hybrid or dynamic real-world systems, where sensor inputs are real- or integer-valued. Current algorithms are not sufficient for proving many LTL properties of such systems, since they often reduce to other undecidable problems (e.g., first-order satisfiability, ranking function synthesis). We improve the state-of-the-art in infinite-state LTL model checking by presenting rlive-inf, an infinite-state extension to the finite-state model checking algorithm rlive and demonstrate with experiments that the new algorithm complements existing approaches.

A technique more lightweight than full-scale model checking is verifying that a large set of simulated executions of a system satisfy a property. To this end, we develop a new algorithm for verifying that an execution of a system satisfies a MLTL specification based on an encoding into bit-vectors. We believe a reduction of System Verilog Assertions (SVA) to MLTL will enable the bit-vector-encoding-based algorithm implementation (SABRe) to efficiently verify a meaningful subset of SVA for System Verilog hardware designs during simulation.

Beyond checking hardware at design time, SABRe is well-suited for processing high-throughput streams of data more broadly, including at runtime. Existing approaches to checking executions of big data systems (e.g., large-scale servers) focus on first order temporal logic properties and struggle with high-speed streams of data. We therefore believe a reduction from a useful subset of Metric First Order Temporal Logic (MFOTL) to MLTL and will allow us to apply SABRe to the resulting specifications and achieve high-throughput verification. 

Runtime verification algorithms, especially for those targeting real-time systems such as R2U2, are only useful if they can fit on the target system. Furthermore, reducing the resource requirements for runtime monitors before deployment often lowers latency of the resulting monitors. We therefore present a technique for automatically optimizing the resource requirements of runtime monitors for MLTL via Equality Saturation, a time-tested approach for rewrite-based optimization. We also present a number of new MLTL rewrites as well as an SMT-based, push-button proof technique for proving that a rewrite is correct (i.e., maintains equivalence).

Committee: Kristin-Yvonne Rozier (major professor), Tichakorn Wongpiromsarn, Gianfranco Ciardo, Samik Basu and Konstantin Slutsky