In this paper, we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in whether model checking can be effectively applied to large software specifications. To investigate this, we translated a portion of the state-based system requirements specification of Traffic Alert and Collision Avoidance System II (TCAS II) into input to a symbolic model checker (SMV). We successfully used the symbolic model checker to analyze a number of properties of the system. We report on our experiences, describing our approach to translating the specification to the SMV language, explaining our methods for achieving acceptable performance, and giving a summary of the properties analyzed. Based on our experiences, we discuss the possibility of using model checking to aid specification development by iteratively applying the technique early in the development cycle. We consider the paper to be a data point for optimism about the potential for more widespread application of model checking to software systems.

This paper describes an integrated approach to safety analysis of software requirements and demonstrates the feasibility and utility of applying the individual techniques and the integrated approach on the requirements specification of a guidance system for a high-speed civil transport being developed at NASA Ames. Each analysis found different types of errors in the specification; thus together the techniques provided a more comprehensive safety analysis than any individual technique. We also discovered that the more the analyst knew about the application and the model, the more successful they were in finding errors. Our findings imply that the most effective safety-analysis tool will assist rather than replace the analyst.

An open question in the area of Programming by Demonstration (PBD) is how to best represent the inferred program. Without a way to view, edit, and share programs, PBD systems will never reach their full potential. We designed and implemented two graphical representation languages for a PBD desktop similar to the Apple Macintosh Finder. Although a user study showed that both languages enabled nonprogrammers to generate and comprehend programs, the study also revealed that the language that more closely reflected the desktop domain doubled users' abilities to accurately generate programs. Trends suggest that the same language was easier for users to comprehend. These findings suggest that it is possible for a PBD system to enable nonprogrammers to construct programs and that the form of the representation can impact the PBD system's effectiveness. A paper-and-pencil evaluation of the two versions of the PBD desktop prior to the study supported these finding and provided interesting feedback on the interaction between usability evaluations and user studies. In particular, the comparison of the paper-and-pencil evaluation with the empirical evaluation suggested that nonempirical evaluation techniques can provide guidance into how to interpret empirical data and, in particular, that PBD systems need to provide support for programming-strategy selection in order to be successful.

In this paper we present our results and experiences of using symbolic model checking to study the specification of an aircraft collision avoidance system. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in the question of whether or not model checking techniques can be applied to large software specifications.To investigate this, we translated a portion of the finite-state requirements specification of TCAS II (Traffic Alert and Collision Avoidance System) into a form accepted by a model checker (SMV). We successfully used the model checker to investigate a number of dynamic properties of the system.We report on our experiences, describing our approach to translating the specification to the SMV language and our methods for achieving acceptable performance in model checking, and giving a summary of the properties that we were able to check. We consider the paper as a data point that provides reason for optimism about the potential for successful application of model checking to software systems. In addition, our experiences provide a basis for characterizing features that would be especially suitable for model checkers built specifically for analyzing software systems.The intent of this paper is to evaluate symbolic model checking of state-machine based specifications, not to evaluate the TCAS II specification. We used a preliminary version of the specification, the version 6.00, dated March, 1993, in our study. We did not have access to later versions, so we do not know if the properties identified here are present in later versions.