Checking properties of safety critical specifications using efficient decision procedures

David Y W Park, Jens U. Skakkebaek, Mats P E Heimdahl, Barbara J. Czerny, David L. Dill

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the Workshop on Formal Methods in Software Practice
EditorsM. Ardis
PublisherACM
Pages34-43
Number of pages10
StatePublished - Jan 1 1998
EventProceedings of the 1998 2nd Workshop on Formal Methods in Software Practice - Clearwater Beach, FL, USA
Duration: Mar 4 1998Mar 5 1998

Other

OtherProceedings of the 1998 2nd Workshop on Formal Methods in Software Practice
CityClearwater Beach, FL, USA
Period3/4/983/5/98

Fingerprint Dive into the research topics of 'Checking properties of safety critical specifications using efficient decision procedures'. Together they form a unique fingerprint.

Cite this