Decoupling synchronization from local control for efficient symbolic model checking of statecharts

Symbolic model checking is a powerful formal verification technique for reactive systems. We address the problem of symbolic model checking for software specifications written as statecharts. We concentrate on how the synchronization of statecharts relates to the efficiency of model checking. We show that statecharts synchronized in an oblivious manner, such that the synchronization and the local control are decoupled, tend to be easier for symbolic analysis. Based on this insight, the verification of some non-oblivious systems can be optimized by a simple, transparent modification to the model to separate the synchronization from the local control. The technique enabled the analysis of the statecharts model of a fault tolerant electrical power distribution system developed by the Boeing Commercial Airplane Group. The results disclosed subtle modeling and logical flaws not found by simulation.