Font Size: a A A

Automated verification of generic computer software components

Posted on:1999-12-26Degree:Ph.DType:Dissertation
University:Rensselaer Polytechnic InstituteCandidate:Cook, Robert E., JrFull Text:PDF
GTID:1468390014970031Subject:Computer Science
Abstract/Summary:
The trend in software engineering is for larger, more complicated, systems that run critical applications. For these applications, software testing is often insufficient, and often is performed using a "hit or miss" approach. Formal verification would provide greater assurance, but is typically not applied. One reason why it is not applied is that significant knowledge of, and experience with, computer-assisted theorem provers is often required. A second reason is the amount of time required to perform a verification.; In our research, we have developed a framework for formal verification of software utilizing PVS (a formal specification and verification system developed by SRI International). We have created a set of axioms to symbolically execute functions, and have formed a representation for the formal specifications. The axioms, combined with a set of user-defined proof strategies, permit a formal verification to be performed by issuing only one command to the theorem prover. Therefore, to perform a formal verification, the engineer is not required to have extensive knowledge of the theorem prover. The framework we have developed was designed to be capable of formally verifying generic functions. Therefore, the time involved to formally specify a function can be amortized over the many expected instantiations of the generic function.; The generic functions we have formally verified come from the C++ Standard Template Library, part of the new ANSI/ISO C++ standard. Of greatest significance, we have formally verified the correctness of the insert{dollar}sb-{dollar}aux member function of the vector container class. To perform such verifications, concepts such as memory references, iterators and iterator concepts, manipulation of array data, and dynamic memory allocation needed to be addressed. While the system is not without limitations and the time involved in performing the verification can be sizable, we believe that a system specifically designed for formal verifications, based on our framework, could realistically be applied to formally verifying functions that are expected to experience significant levels of reuse or that require ultra-high assurance.
Keywords/Search Tags:Verification, Software, Formal, Generic, Functions
Related items