Classify and rank Daikon invariants on embedded systems

Program invariants disclose hidden, yet interesting program properties. These properties specify preconditions and postconditions for program methods at their entries and exits, respectively. They assist human users in a broad range of software engineering practices such as understanding program behavior and localizing program bugs. Automatic inference of these program invariants alleviates human efforts in identifying and deriving them. This is typically realized by executing programs concretely, observing the changes of, and verifying the relationships among, interesting program variables. Among various invariant inference tools, Daikon and DySy are two of those that have the widest use in analyzing traditional desktop programs. Yet many of Daikon’s inferred invariants are considered irrelevant to human interests. In this thesis, we mainly regard an application method invariant as irrelevant if it does not describe this method’s properties. Although DySy has made its efforts to reduce most of irrelevant invariants, it assumes the availability of all program source code. When we tried to deploy Daikon and DySy for the invariant inference of embedded system applications, we encountered a number of challenges that are related to irrelevant invariants, library calls and incompatible platform problems. For example, embedded system applications deal with platform-specific devices such as ultrasonic sensors and motor controllers, and invoke periodically these devices’ library calls whose source code is typically unavailable to developers. In addition, embedded operating systems typically do not share a compatible instruction set with traditional desktop operating systems, and therefore they commonly lack adequate support for programming tasks. This restricts the use of Daikon and DySy for the invariant inference of this kind of programs and the reduction of potentially irrelevant invariants. To address these challenges, we study a new approach in this thesis to classifying and ranking Daikon’s inferred invariant results according to their use in our target program methods. We also built a new C-language front end to adapt Daikon to the use on embedded systems that are Intel 386 instruction-incompatible. To evaluate the effectiveness of our approach, we selected a Minicar sensing and controlling system and its three applications as our experimental platform. The Minicar system and its three applications have the capability of perceiving surrounding environments and calculating the distances away from nearby obstacles to make smart driving to avoid potential collisions. We ran Daikon using the newly built C-language front end on the three Minicar applications and applied our classification and ranking approach to the Daikon inferred invariants. We also invited Minicar developers to mark these Daikon inferred invariants to evaluate the effectiveness of our approach. The experimental results showed that our approach can reduce 73.3% of the inferred irrelevant invariants by Daikon on these three Minicar applications