BBS: A phase-bounded model checker for asynchronous programs

Abstract

A popular model of asynchronous programming consists of a single-threaded worker process interacting with a task queue. In each step of such a program, the worker takes a task from the queue and executes its code atomically to completion. Executing a task can call “normal” functions as well as post additional asynchronous tasks to the queue. Additionally, tasks can be posted to the queue by the environment. Bouajjani and Emmi introduced phase-bounding analysis on asynchronous programs with unbounded FIFO task queues, which is a systematic exploration of all program behaviors up to a fixed task phase. They showed that phase-bounded exploration can be sequentialized: given a set of recursive tasks, a task queue, and a phase bound L > 0, one can construct a sequential recursive program whose behaviors capture all states of the original asynchronous program reachable by an execution where only tasks up to phase L are executed. However, there was no empirical evaluation of the method. We describe our tool Bbs that implements phase-bounding to analyze embedded C programs generated from TinyOS applications, which are widely used in wireless sensor networks. Our empirical results indicate that a variety of subtle safety-violation bugs are manifested within a small phase bound (3 in most of the cases). While our evaluation focuses on TinyOS, our tool is generic, and can be ported to other platforms that employ a similar programming model.