Systematic Testing of Asynchronous Reactive Systems
Ankush Desai, Shaz Qadeer, Sanjit Seshia

Citation
Ankush Desai, Shaz Qadeer, Sanjit Seshia. "Systematic Testing of Asynchronous Reactive Systems". ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2015, August, 2015.

Abstract
We introduce the concept of a delaying explorer with the goal of performing prioritized exploration of the behaviors of an asynchronous reactive program. A delaying explorer stratifies the search space using a custom strategy, and a delay operation that allows deviation from that strategy. We show that prioritized search with a delaying explorer performs significantly better than existing prioritization techniques. We also demonstrate empirically the need for writing different delaying explorers for scalable systematic testing and hence, present a flexible delaying explorer interface. We introduce two new techniques to improve the scalability of search based on delaying explorers. First, we present an algorithm for stratified exhaustive search and use efficient state caching to avoid redundant exploration of schedules. We provide soundness and termination guarantees for our algorithm. Second, for the cases where the state of the system cannot be captured or there are resource constraints, we present an algorithm to randomly sample any execution from the stratified search space. This algorithm guarantees that any such execution that requires $d$ delay operations is sampled with probability at least $1/L^d$, where $L$ is the maximum number of program steps. We have implemented our algorithms and evaluated them on a collection of real-world fault-tolerant distributed protocols.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Ankush Desai, Shaz Qadeer, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/572.html"
  >Systematic Testing of Asynchronous Reactive
  Systems</a>, ACM SIGSOFT Symposium on the Foundations
  of Software Engineering, 2015, August, 2015.

• Plain text

  Ankush Desai, Shaz Qadeer, Sanjit Seshia. "Systematic
  Testing of Asynchronous Reactive Systems". ACM SIGSOFT
  Symposium on the Foundations of Software Engineering, 2015,
  August, 2015.

• BibTeX

  @inproceedings{DesaiQadeerSeshia15_SystematicTestingOfAsynchronousReactiveSystems,
      author = {Ankush Desai and Shaz Qadeer and Sanjit Seshia},
      title = {Systematic Testing of Asynchronous Reactive Systems},
      booktitle = {ACM SIGSOFT Symposium on the Foundations of
                Software Engineering, 2015},
      month = {August},
      year = {2015},
      abstract = {We introduce the concept of a delaying explorer
                with the goal of performing prioritized
                exploration of the behaviors of an asynchronous
                reactive program. A delaying explorer stratifies
                the search space using a custom strategy, and a
                delay operation that allows deviation from that
                strategy. We show that prioritized search with a
                delaying explorer performs significantly better
                than existing prioritization techniques. We also
                demonstrate empirically the need for writing
                different delaying explorers for scalable
                systematic testing and hence, present a flexible
                delaying explorer interface. We introduce two new
                techniques to improve the scalability of search
                based on delaying explorers. First, we present an
                algorithm for stratified exhaustive search and use
                efficient state caching to avoid redundant
                exploration of schedules. We provide soundness and
                termination guarantees for our algorithm. Second,
                for the cases where the state of the system cannot
                be captured or there are resource constraints, we
                present an algorithm to randomly sample any
                execution from the stratified search space. This
                algorithm guarantees that any such execution that
                requires $d$ delay operations is sampled with
                probability at least $1/L^d$, where $L$ is the
                maximum number of program steps. We have
                implemented our algorithms and evaluated them on a
                collection of real-world fault-tolerant
                distributed protocols.},
      URL = {http://terraswarm.org/pubs/572.html}
  }
  

Posted by Ankush Desai on 11 May 2015.
Groups: tools