Automated Analysis of Software Frameworks
(Position Paper)

Matthew B. Dwyer
Dept. of Computing and Information Science
Kansas State University
234 Nichols Hall
Manhattan, KS 66506 USA
Tel: (913) 532-6350
Fax: (913) 532-7353
Email: dwyer@cis.ksu.edu

Abstract:

Domain-specific frameworks provide significant leverage for reusing design, implementation, validation and verification artifacts. The primary focus of most framework developers and consumers has been on leveraging implementations contained in a framework. Developers of high-assurance and safety-critical systems require more than just an implementation; they require very high degrees of confidence in the correctness of any software component they use. Traditional validation techniques, such as testing, cannot provide for such high-assurance.

In this paper, we discuss research issues in applying automated finite-state verification techniques to this problem. These techniques can be applied to verify properties of a framework without considering the details of how the framework is used in any particular application. The same techniques can, in turn, be used to verify that a framework is used correctly in an application. To do this requires the availability of precise partial specifications of properties of framework parameters. These parameter specifications allow verification of frameworks to be isolated from verification of applications, thereby enabling modularity in the verification process.

Keywords: Software frameworks, formal specification, static analysis, compositional and modular analysis, model checking

Workshop Goals: Develop a deeper understanding of the kinds of component-based reuse frameworks that are being developed, used, and researched. Open a dialog between the automated static analysis community and the frameworks community.