Checking properties of safety critical specifications using efficient decision procedures

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 it is error-prone and time consuming to check large specifications manually, 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 (air) Traffic alert and Collision Avoidance System (TCAS II). SVC was extended to produce a counter-example 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 mate-of-the-art formal methods and tools. The logic of SVC was sufficiently expressive for the properties that we checked, but more work is needed to extend the class of formulae that SVC decides to cover the properties found in other parts of the TCAS II specification.