Sciweavers

Share
ICSE
1999
IEEE-ACM

A Practical Method for Verifying Event-Driven Software

8 years 11 months ago
A Practical Method for Verifying Event-Driven Software
Formal verification methods are used only sparingly in software development. The most successful methods to date are based on the use of model checking tools. To use such he user must first define a faithful abstraction of the application (the model), specify how the application interacts with its environment, and then formulate 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 software applications, securing accuracy. Interface definitions and property specifications have meaningful defaults that can be adjusted when the checking process becomes more refined. All checks can be executed mechanically, even when the ap...
Gerard J. Holzmann, Margaret H. Smith
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where ICSE
Authors Gerard J. Holzmann, Margaret H. Smith
Comments (0)
books