Sciweavers

Share
ISSTA
1998
ACM

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

8 years 7 months ago
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.
William Chan, Richard J. Anderson, Paul Beame, Dav
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 1998
Where ISSTA
Authors William Chan, Richard J. Anderson, Paul Beame, David Notkin
Comments (0)
books