Bbs: A Phase-Bounded Model Checker For Asynchronous Programs

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.