The objective of this research is to help engineers build confidence in the correctness of their specifications of reactive systems (such as those that appear in airplanes, automobiles, power plants, etc.). Our specific approach applies model checking---a technique that has proven to be extremely successful in the hardware domain---to the specification of systems that include significant amounts of software. A defining characteristic of the research is the use of hierarchical finite state specifications of real systems, including the specification of TCAS-II, an airborne collision avoidance system. The case studies establish the range of properties that can be evaluated using model checking, showing how model checking can be used in an iterative process to design or analyze specifications. The research defines tools (including translators from specifications to model checkers, analysis tools for interpreting counterexamples, and tools to support iterative development), as well as model checking algorithms that increase the size of the state space which is feasible to check and that extend the capabilities of model checkers for handling arithmetic operations. Improving the ability to define specifications in which there is increased confidence will improve the quality of and reduce the cost of building specifications of reactive systems that include software.
