David Notkin

Despite its tremendous success in locating bugs in hardware circuits, symbolic model checking has rarely been applied to software. The prevalent view is that the symbolic representations used in model checking, such as binary decision diagrams (BDDs), cannot capture the complexity inherent in most software systems. Contrary to this belief, we will present some results and experience in applying the technique to the statecharts specifications of two industrial software systems: a collision-avoidance system used on most commercial aircraft and an electrical power distribution system on Boeing 777. Using symbolic model checking, we have discovered subtle but important errors not found in prior verification efforts. Although the final results are encouraging, initially many of the analyses were infeasible because of the huge BDDs generated. We have developed intuition about some factors that can cause BDD blowup, and based on the insights, devised optimization techniques to improve the efficiency of the analyses by orders of magnitude. These optimizations have made feasible certain analyses that were previously intractable. This is primarily the work of William Chan, with involvement from Richard Anderson, Paul Beame, David Notkin, David Jones, and Bill Warner.