doi: 10.3850/978-3-9815370-4-8_0583


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.

akumar.madhukar@tcs.com
br.mettag@tcs.com

2Chennai Mathematical Institute, Chennai, Tamil Nadu, India.

cmksrivas@hotmail.com

3Department of Computer Science, University of Oxford, United Kingdom.

dbjoern.wachter@cs.ox.ac.uk
ekroening@cs.ox.ac.uk

ABSTRACT

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)