The increasing use of software in safety critical systems entails
increasing complexity, challenging the safety of these systems.
Although formal specifications of real-life systems are orders of
magnitude simpler than the system implementations, they are still
quite complex. It is easy to overlook problems in a specification,
ultimately compromising the safety of the implementation.
Since manually checking large specifications is error-prone and time
consuming, mechanical support is needed. The challenge is to find the
right combination of deductive power (i.e., how rich a logic and what
theories are decided) and efficiency to complete the verification in
reasonable time. In addition, it must be possible to explain why a
proof fails.
As an initial approach to solving this problem, we have adapted the
Stanford Validity Checker (SVC), a highly efficient, general-purpose
decision procedure for quantifier-free first-order logic with linear
arithmetic, to check the consistency of specifications written in
Requirements State Machine Language (RSML). We have concentrated on a
small but complex part of version 6.04a of the specification of the
Traffic alert and Collision Avoidance system (TCAS II). Using a
simple programming interface, SVC was easily extended to produce a
counterexample in terms of the original specification.
The efforts discovered an undesired inconsistency in the
specification, which the maintainers of the specification
independently discovered and subsequently fixed in the most recent
version.
The case study demonstrates the practicality of uncovering problems in
real-life specifications with a modest effort by selective application
of state-of-the-art formal methods and tools. Although the logic of
SVC was sufficiently expressive for the properties that we checked,
more work is needed to extend the class of formulas that SVC decides
to cover the properties found in other parts of the TCAS II
specification.