Research output

Technical Report ()

Push-Button Tools for Application Developers, Full Formal Verification for Component Vendors

Citation
Wilson T, Maharaj S & Clark R (2007) Push-Button Tools for Application Developers, Full Formal Verification for Component Vendors. Technical Report CSM, 167. Department of Computing Science and Mathematics, University of Stirling.

Abstract
Software developers have varying abilities and develop software with differing reliability requirements. Sometimes reliability is critical and the developers have the mathematical capabilities to perform interactive theorem proving but this is not usually the case. We believe that most software developers need easy to use tools such as run-time assertion checkers and extended static checkers that can help them produce more reliable application-specific code cheaply. However, these lightweight approaches are not sufficient to allow the safe reuse of software components. To safely reuse software components we need comprehensive descriptions and assurances of correctness. These requirements can be provided for by full formal verification with the additional costs justified by the economies of scale. Our Omnibus verification tool provides integrated support for all these different types of verification. This paper illustrates these concepts through a sorting implementation.

Keywords
Assertion-based verification; Run-time assertion checking; Extended Static Checking; Formal verification; Software Component Reuse; Tool integration

Subject headings
Computer programs Verification; Omnibus (Computer program language)

StatusPublished
AuthorsWilson Thomas, Maharaj Savi, Clark Robert
Number of pages15
Title of seriesTechnical Report CSM
Number in series167
Publication date08/2007
PublisherDepartment of Computing Science and Mathematics, University of Stirling
LanguageEnglish
© University of Stirling FK9 4LA Scotland UK • Telephone +44 1786 473171 • Scottish Charity No SC011159
My Portal