Improving Efficiency of Symbolic Model Checking for State-Based System Requirements

We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques in our analysis of the system requirements specification of TCAS II, a complex aircraft collision avoidance system. They together reduce the time and space complexities by orders of magnitude, making feasible some analysis that was previously intractable. The TCAS II requirements were written in RSML, a dialect of statecharts. Keywords Formal verification, symbolic model checking, reachability analysis, binary decision diagrams, partitioned transition relation, statecharts, RSML, TCAS II, system requirements specifiabstraction.

• Type: Conference
• Year: 1998
• Where: ISSTA
• Authors: William Chan, Richard J. Anderson, Paul Beame, David Notkin
• Keywords: ISSTA 1998, Model Checking, Software Engineering, TCAs, TCAS II Requirements