Model checking large software specifications

TLDR

Symbolic model checking has been highly successful for hardware systems, but its applicability to newer software specifications remains uncertain. The paper investigates whether symbolic model checking can be applied to large software specifications, specifically by studying an aircraft collision avoidance system, and aims to characterize features suitable for software-oriented model checkers. The authors translated a 1993 version of the TCAS II finite‑state requirements into SMV, then used a model checker to evaluate dynamic properties, reporting on translation techniques and performance‑improving methods. The study demonstrates that symbolic model checking can successfully analyze dynamic properties of a large software specification, offering optimism for broader application and identifying features that favor software‑oriented model checkers.

Abstract

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.