An Automated Verification Method for Distributed Systems Software Based on Model Extraction

(Title was originally A Practical Method for Verifying Event-Driven Software) (was for ACM Proceedings) Formal verification methods are still used only sparingly in software developments. The most successful methods to date are based on model checking tools. To use such tools, the user defines a faithful abstraction of the application (the model), defines how the application interacts with its environment, and formulates the properties that it should satisfy. Each step in this process can become an obstacle. To complete the verification process successfully often requires specialized knowledge of verification, techniques and a considerable investment of time. In this paper, we describe a verification method that requires little or no specialized knowledge in model construction. It allows us to extract models mechanically from the source of application, securing their accuracy.