As software continues to grow in size and complexity, software programmers continue to make mistakes during development. These mistakes can result in defects in software products and can cause severe damage when the software goes into production. Through the Personal Software Process (PSP), the Carnegie Mellon University Software Engineering Institute has long advocated incorporating discipline and quantitative measurement into the software engineer's initial development work to detect and eliminate defects before the product is delivered to users. This blog post presents an approach for incorporating formal methods with PSP, in particular, Verified Design by Contract, to reduce the number of defects earlier in the software development lifecycle while preserving or improving productivity.

Formal Methods and PSP

Created by Watts Humphrey, PSP incorporates process discipline and quantitative management into the software engineer's individual development work. PSP promotes the exercise of careful procedures during all stages of development, with the aim of increasing the individual's productivity and achieving high-quality final products. PSP emphasizes the measurement of software development work using simple measures, such as source lines of code (SLOC). These measures allow software developers to evaluate the effectiveness of their approach and answer the following questions:

• How is the process working?
• Is my process effective?
• If it is not effective, and I need to make a change, what should I change?
• What were the impacts of that change?

In essence, PSP is a scientific approach that software developers can use to evaluate their effectiveness. The Team Software Process (TSP) applies the same measurement principles in a team environment, and has been found by Capers Jones to produce best-in-class productivity and early defect removal.

Research conducted by my collaborator in this research, Diego Vallespir, director of the Postgraduate Center for Professional Development, University of the Republic Uruguay (CPAP), found that removing defects in the unit testing phase can still be expensive, costing five to seven times more than if they were removed in earlier phases of PSP. Dr. Vallespir's research also found that 38 percent of the injected defects are still present at unit testing. In addition to myself, a team of researchers led by Vallespir along with doctoral student Silvana Moreno (Universidad de la República), and professor Álvaro Tasistro (Universidad ORT Uruguay)--theorized that opportunities existed for improvement in the early detection of defects using TSP. Our team felt that the answer might lie in formal methods. Formal methods use the same methodological strategy as PSP: emphasizing care in development procedures, as opposed to relying on testing and debugging. They can also rigorously establish that the programs produced satisfy their specifications.

Formal methods hold fast to the tenet that programs should be proven to satisfy their specifications. Proof is the mathematical activity of arriving at knowledge deductively, starting with postulated, supposed, or self-evident principles and performing successive inferences, each of which extracts a conclusion out of previously arrived-at premises.

Verified Design by Contract (VDbC) is a technique devised and patented by Bertrand Meyer for designing components of a software system by establishing their conditions of use and behavior requirements in a formal language. With VDbC, software developers metaphorically set up a contract to define certain expectations of their software.

In particular, VDbC has been proposed in the framework of object-oriented design (and specifically in the language Eiffel), and, therefore, the software components to be considered are usually classes. The corresponding specifications are pre- and post-conditions to methods, respectively establishing their terms of use and corresponding outcomes, as well as invariants of the class (i.e., conditions to be verified by every visible state of an instance of the class). In the original VDbC proposal, all specifications were written in Eiffel and are computable (i.e., they are checkable at runtime).

VDbC involves software developers, essentially, setting up a contract to define certain expectations of how the software will behave. VDbC is compatible with test-driven development, which requires defining test cases prior to developing code. This aspect of VDbC is also compatible with PSP, which has always emphasized developing some test cases early on in the software development lifecycle as part of the design process. It is important to note that developing test cases is not the sum of design, but rather the development of test cases is an aspect of design.

Our Approach

Designs are most effective if you have some way of verifying the design formally. Different types of design representations, for example, pseudo-code to represent logic or module decompositions to represent structure, support different levels formality. The leverage of additional formality comes from the rigor with which the design can be verified.

Our approach involves using the framework and instrumentation of PSP to evaluate how the designer, in this case VDbC, affects the results. The PSP script supports consistency and measurement by defining the logical sequence of steps (for example, plan, design, code, review code, unit test) that must be followed when building code. With VDbC, we added specific phases, activities, and outcome criteria to the PSP script (For more information about PSP scripts, please see Table 2 in the following SEI technical report.) to show that we can

• measure how much effort has gone into the phase
• set up the contract requirements
• conduct verification
• check that the design is complete and that the design is correct

As explained in detail in our technical report on this approach, PSP and VDbC: An Adaption of the PSP that Incorporates Verified Design by Contract, our combined approach resulted in new phases of software development and modified other phases already present in PSP. The resulting adaptation of PSP, hereafter referred to as PSPVDbC, incorporates new phases, modifies others, and adds new scripts and checklists to the infrastructure. Specifically, the phases of formal specification, formal specification review, formal specification compile, test case construct, pseudo code, pseudo code review, and proof are added.

In the remainder of this post, we will present the phases of our combined approach, indicating the activities that are to be performed and the modifications introduced in the scripts with respect to the original PSP.

Planning. The activities in this phase of PSPVDbC are the same as in ordinary PSP. For example, Program Requirements ensure a precise understanding of every requirement. Size Estimate involves carrying out a conceptual design (i.e., producing a module [class] structure). Resource Estimate estimates the amount of time needed to develop the program. For this, the PROBE method (This SEI technical report includes a description of the PROBE method). is used, which employs historical records and linear regression for producing the new estimation and for measuring and improving the precision of the estimations.

Task and Schedule Planning is for long-term projects. These are subdivided into tasks, and the time is estimated for each task. This planning is unchanged in PSPVDbC. Defect Estimate Base is for estimating the number of defects injected and removed at each phase. Historical records and the estimated size of the program are utilized for performing this estimation. In PSPVDbC new records are needed to estimate the defects removed and injected at each new phase. Finally, the planning script in PSPVDbC is the same as in PSP, given that the corresponding activities are unchanged.

Design. This phase defines the data structures of the program as well as its classes and methods, interfaces, components, and interactions among all of them. In PSPVDbC, the elaboration of the pseudo code is postponed until the formal specification is available for each method.

Design Review. This phase is the same as ordinary PSP and uses its development script describing the steps to follow in the review. A sample development script is included in Table 13 of our technical report.

Test Case Construction. We want to investigate the cost effectiveness of test case construction and unit testing when formal methods are used. Problems with unit test include the cost of test case construction, maintenance of test cases, number of test cases required, and a failure to achieve comprehensive test coverage. We want to determine if it is practical to reduce or eliminate categories of test in the unit test phase when using these formal methods. To answer this, the following must be known:

• cost of test case construction
• cost of unit test construction
• defect density entering into unit test
• yield of the unit test phase
• types of defects entering and escaping unit test

Formal Specification. This phase must be performed after the design review. The reason for this is that reviews are highly effective in detecting defects injected during design and need to be discovered as early as possible. In this phase, we begin to use the development environment that supports VDbC. Two activities are carried out in this phase:

• Construction consists of preparing the environment and defining within it each class with its method headers.
• Specification, in which we write down in the carrier language the pre- and post-conditions of each method as well as the class invariant. Note that, within the present approach, the use of formal methods begins once the design has been completed. It consists of the formal specification of the produced design and the formal proof that the final code is correct with respect to this specification.

Formal Specification Review. Using a formal language for specifying conditions is not a trivial task, and both syntactic and semantic defects can be injected. To avoid the propagation of these errors to further stages, and the resulting increase in the cost of correction, we propose a phase called formal specification review. The script that corresponds to this phase contains the following activities:

• In the review activity, the sentences of the specification are inspected using a checklist.
• In the correction review, all defects detected during the review are removed.
• In checking, the corrections are reviewed to verify their adequacy.

Formal Specification Compile. Any development tool supporting VDbC will be able to compile the formal specification. Since this allows an early detection of errors, we consider it valuable to explicitly introduce this phase into PSPVDbC. In particular, it is worthwhile to detect all possible errors in the formal specifications before any coding is carried out. A further reason to isolate the compilation of the formal specification is to allow the time spent in this specific activity to be recorded.

Pseudo Code. The pseudo code phase allows software developers to understand and structure the solution to the specified problem just before coding. Describing the intent of the design in a programing neutral language helps the developer bridge the more abstract design to the concrete implementation. The documentation later supports peer review that the code actually implements the design. Thus, the pseudo code of each class method defined in the logic template is written down. Our approach advocates that the pseudo code be produced after the compilation of the specification in order for the specification to serve as a well understood starting point for design elaboration in pseudo code. Writing down the pseudo code just before coding allows us to follow a well-defined process in which the output of each stage is taken as input to the next one.

Pseudo Code Review. A checklist is used for guiding activity in this phase. The activity pseudo code review is added to the development script. The pseudo code review script is proposed for use in this activity. An example of the script follows:

• Produce a pseudo code to meet the design.
• Record the design logic specification templates.
• Record defects in the defect recording log.
• Record time in the time recording log.

Code, Code Review, and Code Compile. Just as in PSP, these phases consist of translating the design into a specific programming language, revising the code, and compiling it. The description of these activities in the PSPVDbC development script is the same as in the PSP development script.

Proof. An addition to PSPVDbC, this phase provides evidence of the correctness of the code with respect to the formal specification (i.e., its formal proof). A computerized verifying tool is used that derives proof obligations and helps to carry out the proofs themselves.

Unit Test. This phase is the same as in PSP. This phase is relevant because it detects mismatches with respect to the original, informal requirements of the program. These defects can arise at several points during the development, particularly as conceptual or semantic errors of the formal specifications. The test cases to be executed must therefore be designed right after the requirements are established (i.e., during the phase test case construct) as indicated above.

Post Mortem. This is the same as in ordinary PSP, and its description in the PSPVDbC development script. However, several modifications must be made to the infrastructure supporting the new process. For example, all new phases must be included in the support tool to keep track of the time spent at each phase, as well as to record defects injected, detected, and removed at each phase. Our intention in this research was to present the changes in the process to incorporate VbDC. The adaptation of the supporting tools, scripts, and training courses is a matter for future work.

Conclusions and Future Work

By definition, in Design by Contract (and therefore also in PSPVDbC) the specification language is seamlessly integrated with the programming language, either because they coincide or because the specification language is a smooth extension of the programming language. As a consequence, the conditions making up the various specifications are Boolean expressions that are simple to learn and understand. We believe that this makes the approach easier to learn and use than the ones that have previously been explored.

Nonetheless, the main difficulty associated with the method resides in developing a competence in carrying out the formal proofs of the written code. This is, of course, a challenge common to any approach based on formal methods. Experience shows, however, that the available tools are generally of great help in this matter. Tools used with the Architecture Analysis and Description Language (AADL) modeling notation are used to model embedded systems and is supported by tools such as Osate and TASTE. There are reports of cases in which tools have generated the proof obligations and discharged up to 90 percent of the proofs automatically.

We conclude that it is possible, in principle, to define a new process that integrates the advantages of both PSP and formal methods, particularly VDbC.

In our future work, we will evaluate the PSPVDbC in actual practice by carrying out measurements in empirical studies. The fundamental aspect to be measured in our evaluation is the quality of the product, expressed in the number of defects injected and removed at the various stages of development. We are also interested in measures of the total cost of the development.

We welcome your feedback on our work. Please leave comments below.

Additional Resources

To read the SEI technical report on which this research is based, PSP
VDbC: An Adaptation of the PSP that Incorporates Verified Design by Contract, please visit
https://resources.sei.cmu.edu/library/asset-view.cfm?assetid=47974.

To read the book, Software Engineering Best Practices: Lessons from Successful Projects in the Top Companies by Capers Jones, please visit this url.