Paper Info
Title
Verifying synchronous reactive systems using lazy abstraction
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.
Year
Venue
Keywords
2015
DATE
model checking,schedules,concurrent computing,multi threading,algorithm design and analysis,software verification,data structures
Field
DocType
ISSN
Transition system,Asynchronous communication,Model checking,Concurrency,Computer science,Parallel computing,Real-time computing,Reactive system,State space,Software verification,Distributed computing,Formal verification
Conference
1530-1591
Citations 
PageRank 
References 
1
0.36
7
Authors
5
Name
Order
Citations
PageRank
Kumar Madhukar110.70
Mandayam Srivas221.86
Björn Wachter332620.09
Daniel Kroening43084187.60
Ravindra Metta5265.93