Background and Related Work

(Excerpt from "DevCOP: A Software Certificate Management System for Eclipse," submitted to ISSRE 2006)

Types of V&V Techniques

During the creation of software, a development team can employ various V&V practices to improve the quality of the software [1]. For example, different forms of software testing could be used to validate and/or verify various parts of a system under development. Sections of code can be written such that they can be automatically proven correct via an external theorem prover [17]. A section of a program that can be logically or mathematically proven correct could be considered more reliable than a section that has "just" been tested for correctness.

Other V&V practices and techniques require more manual intervention and facilitation. For instance, formal code inspections [7] are often used by development teams to evaluate, review, and confirm that a section of code has been written properly and works correctly. Pair programmers [19] benefit from having another person review the code as it is written. Some code might also be based on technical documentation or algorithms that have been previously published, such as white papers, algorithms, or departmental technical reports. The extent of V&V practices used in a development effort can provide information about the estimated defect density of the software prior to product release.

Balci categorized V&V techniques with regard to the how the technique's methodology for detecting defects [1]. Balci's categorization of V&V techniques includes:
Manual - includes all manual checking, such as pair programming [19] and code inspections [7];
Static - includes automatic checking of code before run-time, such as syntax and static analysis;
Dynamic - includes all automatic checking that takes place during execution, such as black-box testing;
Formal - includes all strictly mathematical forms of checking, such as lambda calculus and formal proofs [17].

Software Certificate Management Systems

Different V&V techniques produce different kinds of evidence of their execution, such as logs from test cases, written records from code inspections, or systems that can record pair programming efforts. The evidence from these V&V techniques could be stored manually in various forms of documentation. However, manually recording static documentation takes time away from development and produces documents that are often not maintained after their initial creation. If these V&V documents are not maintained, they become obsolete and the effort is wasted.

Software certificates provide a valuable resource for developers to gather V&V information, in some cases automatically, in a single format and to also increase traceability between V&V techniques and sections of code. This V&V information can be used for maintenance purposes, for analysis of the effectiveness of certain V&V practices, for future reference in reused code, or for defect density estimation purposes. Information about who performed various V&V techniques could be useful for software maintainers as they have a better idea who to talk to if they have issues with a particular system. Developers could learn about the effectiveness of their V&V practices if they compare defect reports to the coverage of particular V&V techniques. If numerous defects are found in sections of code that have all been checked with a certain V&V technique, developers might adjust the use of that technique or spend time refining it. System modules are also often reused in later projects within an organization. Having an accurate record of the V&V practices used on that code could help speed development, as teams might not spend extra time verifying a previously-verified section of code. In our research, we are developing a method of estimating defect density in a system based on its record of V&V techniques.

While the creation of software certificates allows for the collation of V&V information in a single place, these certificates must be maintained so that they accurately reflect the current code base. A SCMS provides a range of services, including automatically creating and maintaining certificates, enabling the browsing of certificates in a system, and checking the validity of certificates (e.g. automatically invalidating a certificate upon a code change) [6, 18]. The goal of a SCMS is to automate the management of certificate information so that minimal overhead is added to the development process. Research is being conducted by various groups in how SCMSs can be used in the development process [6, 8, 10, 18].

Programatica

Programatica [10, 17] is a SCMS that has been in development since 2003. This system is the inspiration for the work mentioned in the previous section and for our DevCOP work. The Programatica team at the Oregon Graduate Institute at the Oregon Health and Science University (OGI) and at Portland State University (PSU) is working on a method for high-assurance software development for the Haskell programming language [10, 17]. The goals of the Programatica team are to allow users to capture evidence of V&V and to manage this evidence to help guide future development efforts [10]. The Programatica tool is built on the concept that specified properties could be placed in the source code itself to show that certain pieces of code have been verified or validated through a particular V&V technique. These properties can be derived from several different sources, such as expert opinion, test cases, or external theorem provers. These specified properties become certificates, linking a validated property as evidence of high-assurance with a piece of code.

Programatica allows various external tools to plug-in to its certificate management module so that Programatica can leverage the V&V evidence provided by these tools. For example, Programatica gathers V&V evidence from an external testing framework called QuickCheck [4] and a theorem prover called Alfa [10]. Developers can write and then certify code as it becomes complete with these external tools.

Managers can decide how much of the code base needs to be certified at any given time, slowly increasing this number as the system nears completion [10, 17]. Programatica uses this idea of gradually increasing the number of certificates since code is usually more in flux at the beginning of a project, and a developer's time should not be spent recertifying code that could change soon after recertification.

The DevCOP SCMS plug-in builds on the ideas initiated in the Programatica project, but expands on them in various ways. The main difference is that DevCOP is written for Java rather than Haskell. The Programatica tool is used in conjunction with a developer's programming environment of choice. DevCOP, however, is directly integrated into the Eclipse IDE. The plug-in can also interact directly with the programming tools that the developer uses, such as test case coverage tools like jcoverage. DevCOP also adds basic reporting tools, such as views that provide information to the developer on V&V certificate coverage.

[1] Balci, O., "Verification, Validation, and Accreditation of Simulation Models," Winter Simulation Conference, 1997, pp. 125-141.
[2] Beck, K., Extreme Programming Explained: Embrace Change, Second ed. Reading, Mass.: Addison-Wesley, 2005.
[3] Boehm, B. W., "Building Parametric Models," International Advanced School of Empirical Software Engineering, Rome, Italy, September 29, 2003.
[4] Classen, K. and Hughes, J., "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs," International Conference on Functional Programming, Montreal, Canada, Sept. 18-20, 2000, pp. 268-279.
[5] Cok, D. and Kiniry, J., "ESC/Java2: Uniting ESC/Java and JML - Progress and issues in building and using ESC/Java2," Construction and Analysis of Safe, Secure and Interoperable Smart devices Workshop, Marseille, France, March 10-13, 2004, pp. 108-128.
[6] Denney, E. and Fischer, B., "Software Certificate and Software Certificate Management Systems," Workshop on Software Certificate Management, Long Beach, CA, Nov 8, 2005, pp. 1-6.
[7] Fagan, M., "Design & Code Inspections to Reduce Errors in Program Development," IBM Systems Journal, vol. 15, no. 3, pp. 182-211, 1979.
[8] Hutter, D., "Software Certification Management: How Can Formal Methods Help?" Workshop on Software Certificate Management, Long Beach, CA, Nov 8, 2005, pp. 47-50.
[9] International Society of Parametric Analysts, "Parametric Estimating Handbook," Department of Defense, Online Handbook, April 16, 2005. Available online: http://www.ispa-cost.org/PEIWeb/Third_edition/newbook.htm
[10] Jones, M., "Evidence Management in Programatica," Workshop on Software Certificate Management, Palm Beach, California, 2005.
[11] Musa, J., Software Reliability Engineering: McGraw-Hill, 1998.
[12] Sherriff, M., "Using Verification and Validation Certificates to Estimate Software Defect Density," Doctoral Symposium, Foundations of Software Engineering, Lisbon, Portugal, September 6, 2005, 2005.
[13] Sherriff, M., Boehm, B. W., Williams, L., and Nagappan, N., "An Empirical Process for Building and Validating Software Engineering Parametric Models," North Carolina State Univeristy CSC-TR-2005-45, October 19 2005.
[14] Sherriff, M. and Williams, L., "A Method for Verification and Validation Certificate Management in Eclipse," Workshop on Software Certificate Management, Long Beach, CA, Nov 8, 2005, pp. 19-22.
[15] Sherriff, M. and Williams, L., "Certification of Code During Development to Provide an Estimate of Defect Density," Fast Abstract, International Symposium on Software Reliability Engineering, Chicago, IL, Nov 8, 2005, pp. 447-448.
[16] Sherriff, M., Williams, L., "Tool Support For Estimating Software Reliability in Haskell Programs," Student Paper, IEEE International Symposium on Software Reliability Engineering, St. Malo, France, 2004, pp. 61-62.
[17] The Programatica Team, "Programatica Tools for Certifiable, Auditable Development of High-Assurance Systems in Haskell," High Confidence Software and Systems, Baltimore, MD, 2003.
[18] Whalen, M., "Certificate Management: A Practitioner's Perspective," Workshop on Software Certificate Management, Long Beach, CA, Nov 8, 2005, pp. 23-26.
[19] Williams, L. and Kessler, R., Pair Programming Illuminated. Boston: Addison-Wesley, 2002.