Verifying Synchronous Reactive Systems using Lazy Abstraction
Kumar Madhukar1,2,a, Mandayam Srivas2,c, Björn Wachter3,d, Daniel Kroening3,e and Ravindra Metta1,b
1Tata Research Development and Design Center, Pune, Maharashtra, India.
2Chennai Mathematical Institute, Chennai, Tamil Nadu, India.
3Department of Computer Science, University of Oxford, United Kingdom.
Embedded software systems are frequently modeled as a set of synchronous reactive processes. The transitions performed by the processes are given as sequential, atomic code blocks. Most existing verifiers flatten such programs into a global transition system, to be able to apply off-the-shelf verification methods. However, this monolithic approach fails to exploit the lock-step execution of the processes, severely limiting scalability.
We present a novel formal verification technique that analyses synchronous concurrency explicitly rather than encoding it. We present a variant of Lazy Abstraction with Interpolants (LAWI), a technique successfully used in software verification, and tailor it to synchronous reactive concurrency. We exploit the synchronous communication structure by fixing an execution schedule, circumventing the exponential blow-up of state space caused by simulating synchronous behaviour by means of interleavings. The technique is implemented in SYMPARA, a verification tool for synchronous reactive systems. To evaluate the effectiveness of our technique, we compare SYMPARA with Bounded Model Checking and k-induction, and a LAWI-based verifier for multi-threaded (asynchronous) software. On several realistic examples SYMPARA outperforms the other tools by an order of magnitude.
Full Text (PDF)