Model checking software with well-defined APIs: The socket case

The application of model checking technology to real software seems to be a promising and realistic approach to increase its quality. There are some successful examples of tools for this purpose, mainly working with self-contained programs. However, verifying software that uses external functionality provided by the operating system via API s is currently a challenging trend.In this paper, we give a method for using the tool SPIN to verify distributed software systems that use the API Socket and the network protocol stack TCPIP for communications. Our approach consists in building a model of the underlying operating system to be joined with the original C code in order to obtain the input for the model checker. We define and use a formal semantics of the API to conduct the correct construction of models. The whole modelling process is transparent to the C programmer, because it is performed automatically and without special syntactic constraints in the input C code. Regarding verification, we consider optimization techniques suitable for this application domain, and we ensure that the system only reports potential (non-spurious) errors.