MightyPPL improves timed system checks with exact event timing
MightyPPL : Towards model checking MTL
Logic in Computer Science
Summary
Checking whether events happen at specific exact times in computer systems is a challenging problem. The authors present an improved tool called MightyPPL that can now verify timing properties involving exact delays between events, as well as other temporal logic features. Their tool performs better than existing options on benchmarks. This means software that depends on precise timing could be tested more reliably and efficiently.
What this means in practice
- •For embedded software engineers: Verify that real-time software meets exact timing constraints between events to ensure system reliability.
- •For industrial automation teams: Check timed properties in control systems where precise event timing is critical for safety and efficiency.
Authors
Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh Pandya
Abstract
The theoretical foundation for model checking timed systems against Metric Interval Temporal Logic (MITL) was established in the early 1990s, yet the first practical tool supporting future MITL (MightyL) did not emerge until 2017. Recently, there has been growing interest in extending this toolchain to support more expressive logical operators, including past modalities, Pnueli modalities, and limited use of singular intervals. MightyPPL is one such toolchain. We introduce an upgraded version of MIghtyPPL that enables for the first time, the model checking of Metric Temporal Logic (MTL) properties of the form (whenever an event p occurs, it is eventually followed by some event q after exactly some k time units) in addition to Pnueli and Past modalities. We discuss the tool's underlying architecture and implementation, and present a performance evaluation against the Tempora tool across diverse satisfiability and model checking benchmarks, demonstrating that MightyPPL delivers significantly better performance.