Optimizing symbolic model checking for statecharts

Symbolic model checking based on binary decision diagrams is a powerful for mal verification technique for reactive systems. In this paper, we present various optimizations for improving the time and space efficiency of symbol ic model checking for systems specified as statecharts. We used these techn iques in our analyses of the models of a collision avoidance system and a f ault-tolerant electrical power distribution (EPD) system, both used on comm ercial aircraft. The techniques together reduce the time and space requirem ents by orders of magnitude, making feasible some analysis that was previou sly intractable. We also elaborate on the results of verifying the EPD mode l. The analysis disclosed subtle modeling and logical flaws not found by si mulation.