Logic Verification of ANSI-C Code with SPIN

We describe a tool, called AX, that can be used in combination with the model checker SPIN to efficiently verify logical properties of distributed software systems implemented in ANSI-standard C [18]. AX, short for Automaton eXtractor, can extract verification models from C code at a user level of abstraction. Target applications include telephone switching software, distributed operating systems code, protocol implementations, concurrency control methods, and client-server applications. This paper discusses how AX is currently implemented, and how we plan to extend it. The tool was used in the formal verification of two substantial software applications: a commercial checkpoint management system and the call processing code for a new telephone switch.

• Type: Conference
• Year: 2000
• Where: SPIN
• Authors: Gerard J. Holzmann
• Keywords: Model Checker Spin, SPIN 2000, Substantial Software Applications, Telephone Switching Software, Theoretical Computer Science