Emphasizing Formal Analysis In a Software Engineering Curriculum

	©2001 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
Return to Table of Contents

Emphasizing Formal Analysis In a Software Engineering Curriculum

Ann E. Kelley Sobel

Abstract - The integration of formal method application throughout a six course software engineering curriculum is outlined. Formal analysis skills were included in order to increase the complex program solving skills of the student. The five instruction-oriented courses presented highlight how formal analysis was introduced in and applied to the corresponding subject material. The materials presented, along with an accounting of the experiment, provide a basis for other academicians to teach formal analysis at their own institutions.

1. Introduction

A project that integrated formal methods into a software engineering curriculum[1] at Miami University’s Computer Science and Systems Analysis Department is outlined. This project endeavored to address the numerous articles in the current literature expressing the belief that the current educational program offered for a computer science degree does not stress the fundamental mathematical and engineering principles that should form the basis of software engineering [5,6,8,10,11]. A survey of computer science faculty attitudes toward formal methods found that faculty believe that formal methods are not only important, due to their disciplined approach to computer science, but are feasible to teach [9]. Among formal methods advocates, a common belief that the use of formal analysis during software development produces programs that have fewer errors is held. Despite this evidence, few undergraduate courses exist that teach the formal analysis of software and virtually no programs exist that attempt to base several standard core curriculum courses on the understanding and application of formal analysis during the construction of software.

It is for these reasons that an undergraduate software engineering curriculum would benefit from the integration of formal analysis. The experimental curriculum included the previously existing core curriculum courses of data structures, object-oriented software design, software engineering, and a senior capstone course that were modified to include formal analysis application. This curriculum also included two new courses designed to teach the skills necessary to apply formal methods; one emphasizing program derivation and the other emphasizing the analysis of concurrent programs. Students were required to have taken a discrete mathematics course at the end of their freshman year before they entered the experimental curriculum.

Two different formal methods were used throughout the experimental curriculum. The formal analysis of strictly sequential code followed Dijkstra’s weakest precondition semantics [3], while the analysis of concurrent programs used a trace-based operational formal method [12]. The latter formal method was chosen since it is relatively easy to learn, due to its operational nature and reliance on only prior knowledge of first-order logic. These characteristics were particularly important given the student’s lack of software development experience and their limited exposure to only first-order logic.

This paper provides only a sampling of examples, examination questions, and programming assignments. The full accounting of all materials can be found at http://www.eas.muohio.edu/san/formal. The evaluation of the experimental curriculum provides evidence of the benefits of undergraduate students learning to use formal analysis during software construction. The materials presented along with an accounting of the experiment provide a basis for other academicians to teach formal analysis at their own institutions.

Evidence was gathered throughout the three-year period in order to establish the goals of the experiment; namely, undergraduate students are able to learn formal analysis techniques, the feasibility of teaching formal analysis, and the use of formal analysis increases the student’s complex problem solving skills. In order to control as many variables as possible, the experimental and standard core courses were taught by the same instructor using a common text. Mentors were given strict instruction to aid students only in the understanding of formal methods and its application. Students in the standard and experimental versions of a particular course experienced the same examinations and programming assignments. The analysis of the evidence establishes that all three goals of the experiment were met.

An overview of the experimental curriculum is presented in section 2 and expanded in sections 3,4,5, and 7. The basics of formal specification and program derivation are outlined in section 3. The use of coupling invariants to establish a valid implementation of an ADT is presented in section 4. Section 5 highlights the application of formal analysis during object oriented development. The introduction of the trace-based specification model used in the subsequent courses appears in section 6. The application of this specification model in the context of concurrent software systems is presented in section 7. Section 8 discusses the senior year software development project. The qualitative and quantitative results that assess the success of meeting the goals of the experimental curriculum are listed in section 9. Lastly, a summary is presented in section 10.

2. Overview of the Curriculum

The established curriculum for the department that formed the basis from which the experimental curriculum was taught is a blend of computer science, software engineering, and operations research courses. The experimental course track included inserting formal analysis into four of the existing software engineering courses and two new courses that dealt solely with the teaching of formal methods. The sequence of the courses and their status was as follows.

Course Sequence and Status

Course Title New Existing

Logical Foundations of Programs *

Data Structures *

Object-Oriented Software Design (OOD) *

Formal Analysis of Concurrent Programs *

Software Engineering *

Software Engineering Senior Project *

The first course offered in the experimental curriculum emphasized program derivation. Students were taught to specify programs using first-order logic and Cohen’s specification notation [2], and to represent programs using Dijkstra’s guarded command code [3]. Proofs were created manually and used both Hoare triples and the wp predicate transformer [4]. The programs examined in this class were typically quite small, usually fewer than fifteen lines of code.

The Data Structures course taught typical abstract data types (ADTs) which included lists, stack, queues, and trees. Programming assignments were of relatively short length and emphasized the use of a particular ADT as part of the application.

The OOD course taught a variety of design methodologies (e.g., UML) and gave group projects that focused on their use. The projects are traditionally Windows-based and the size of the graphical interface code (written using Microsoft Foundation Classes) clearly dominates the total size of the application code.

The Formal Analysis of Concurrent Programs course centered on the different modes of interaction between concurrent tasks/threads/processes. For the first time, students were faced with implementation code that produced multiple execution sequences coupled with the enforcement of synchronization. Students applied the trace-based operational formal method to specify and verify general problems that relied on multiple processes communicating by means of remote procedure calls, shared variables, and message passing.

As part of the department’s core requirements, a student experiences two courses that cover the entire software engineering life cycle during their senior year. The first course, Software Engineering, addresses feasibility study, prototyping, and design of a software system. The second senior course, Software Engineering Senior Project, assigns group projects with the expectation of a demonstration of a completed prototype of a software application at the end of the course.

Any student who participated in one of the existing experimental curriculum courses had to learn both the material that was commonly taught as well as how to apply formal analysis to any software application in that course.

3. Logical Foundations of Programs

The basic skills needed to apply formal analysis were taught in a new course, Logical Foundations of Programs. This course covers mathematical induction, well-foundedness, specification, derivation, and the theory of the correctness of programs. The text of Cohen, Programming in the 1990s, was chosen because the presentation of this material was not coupled with an implemented programming language; the use of the guarded command language [3] gives the student the freedom to translate this language into a variety of contemporary programming language constructs. The students were motivated to gain experience in performing logical deduction by the assignment of Smullyan logic puzzles.

A simple example highlighting the derivation process follows. It originally appeared in an out of class quiz. Derive the guarded command code from the following specification without using the absolute value function.

var x,z: int

; z : z = |x|

We must first note that the precondition for this specification is true and the postcondition is stated in the last line. This postcondition notes that only the variable z can be modified and the program terminates with z = |x|. Using the weakest precondition semantics (wp) [4], a statement, S, must be found that satisfies the following assertion.

true wp.S.z = |x|

When deriving the statement S, comments that state the justification for each line are connoted using the notation, < comment >. Continuing with the derivation of S, if we choose S to be z := x, we get

wp.z := x.z = |x|

< definition of := >

x = |x|

< definition of absolute value >

x 0

as the precondition which is not equivalent to true. If we choose S to be z := -x, we get

wp. z := -x. z = |x|

< definition of := >

-x = |x|

< definition of absolute value >

x < 0

as the precondition which is not equivalent to true. However, we note that by combining these two assertions, x 0 x < 0, we get the equivalent of true. This observation, and the fact that we started with identical postconditions in the two statement analysis above, permits the combination of the two statements into a single if statement:

if x 0 z := x [] x < 0 z := -x fi

For a more complex example of program derivation, the following specification requires the derivation of a program that contains a loop.

var f: array of int {F = #f}

; var s: int

; s: s = (i. 0 i < F. f[i] )

Recognizing that this summation will probably require a loop ({P} do BS od {R}), we must determine a loop invariant (P) and a guard (B). Using the technique of replacing a constant by a fresh variable, the postcondition can be rewritten as follows.

s = (i. 0 i < n. f[i] ) 0 n F n = F

The first two clauses will be used for the loop invariant and the modified last clause, n F, will represent the guard. The postcondition is partitioned in this manner so that P B R, which guarantees that the postcondition (R) holds upon termination. Next, the loop invariant must be shown to hold before execution of the loop begins. This requires finding a Q so that

Q wp. S_o . P

Clearly, S_omust containsome assignment of s and n. The weakest precondition semantics can be used to calculate the necessary values.

wp. s,n := E,G. s = (i. 0 i < n. f[i] ) 0 n F

< definition of := >

E = (i. 0 i < G. f[i] ) 0 G F

< choose G=0 to establish an empty range >

E = (i. 0 i < 0. f[i] ) 0 0 F

< empty range, F = #f from Q, therefore F 0 >

E = 0

S_o : s,n := 0,0

The final step requires the calculation of S. Again, S must contain some assignment of s and n.

wp. s,n := H,I . s = (i. 0 i < n. f[i] ) 0 n F

< definition of := >

H = (i. 0 i < I. f[i] ) 0 I F

< choose I = n+1 >

H = (i. 0 i < n+1. f[i] ) 0 n+1 F

< algebra, range split >

H = (i. 0 i < n. f[i] ) + f[n] 0 n+1 F

< s = (i. 0 i < n. f[i] ) >

H = s + f[n] 0 n+1 F

< n F 0 n F (given in precondition), algebra >

H = s + f[n]

Therefore,

S : s,n := s + f[n], n+1

Putting all the pieces together, the derived program follows.

{ F = #f }

s,n := 0,0;

do n F s,n := s + f[n], n+1 od

{ s = (i. 0 i < F. f[i] ) }

Classroom instruction was supplemented with several in class problem solving sessions that were supported by three undergraduate mentors. Students were evaluated by their performance on both in and out of class quizzes. In class quizzes predominantly tested their ability to perform textual substitution-based proofs while out of class quizzes extended their experience performing program derivation. A major project in the course centered on the derivation of a guarded command program from a first-order logic specification. Students had to verify that their program did indeed satisfy the given specification. Their programs were then translated into the C++ language. One student believed he was such a strong C++ programmer that he could generate a “better”' C++ program without using the guarded command program. Ironically, his C++ solution had several errors whereas his guarded command program had none.

4. Data Structures

The Data Structures course applied the formal analysis skills gained in the prior program derivation course to the development of abstract data types (ADT). ADT specifications were written using sequences of operations performed and the corresponding effect of performing those operations on an instance of the ADT. Correspondence between ADT operations and a sequence of implementation type operations were maintained using coupling invariants. Many implementations commonly used by software engineers, e.g., a list implemented using an array, were proven to correspond to the ADT. Both the instructor and the students were surprised to learn that the average length of proof for the correspondence of just one ADT operation was one and one half pages of hand written text. However, after completing such an exercise, there was no question as to the correctness of the implementation of a particular ADT.

Before introducing an example of establishing that a particular implementation satisfies the semantics of an ADT, the necessary sequence operations are given. For these definitions, s is a given sequence of type T (s T*).

Operation	Definition
#s	Length of s
s ^ x	x is concatenated to s where xT
s[k]	k^th element of s (zero-based)
s/<i,j>	restriction of the elements of s to the i^th through j^thelement
s^-	#s = 1 #s > 1 s/<0,...,s[#s-2]>

The following example illustrates the steps of establishing the correspondence between the operations for a stack and a list (sequence) based implementation of a stack. The axioms defining the semantics of a stack follow where T is any type.

initialize empty (A1)

x T. push[x] empty top = x (A2)

empty pop (A3)

x T. push[x]; pop skip // no op (A4)

The sequence based definitions for the referenced stack operations in the group of axioms are given as follows.

st T* := < > // st is a sequence of T values that is initialized to < >

push[x] x T st’ = st ^ x

empty # st = 0

top empty st[#st-1]

pop empty st’ = st^-

Some of these definitions use of the “tick” notation, e.g., st’, to refer to the value of the sequence st after a particular sequence operation has been applied.

To demonstrate that the list-based implementation maintains the semantics of the push axiom given above (A2), one must prove:

st’ = st ^ x #st’ 0 st’[#st’–1] = x where x T

which is the original push axiom with each stack operation replaced by its list implementation. Suppressing the details of the proof, one must establish the following first and second facts, (1) and (2) respectively, in order to verify the first and second clauses found on the right hand side of the implication.

(1) #st’ = #st + 1 #st N #st’ 0

(2) st’ = st ^ x st’/<0,…,#st’-2> = st st’[#st’-1] = x where x T

Continuing with the pop axiom (A3) and substituting each stack operation with its corresponding list implementation, we can demonstrate that the list based implementation maintains the semantics of the pop axiom by proving:

#st 0 st^-

which is true since st^- is defined for #st0.

Lastly, to demonstrate that the list based implementation maintains the semantics of A4, one must prove:

( st’ = st ^ x; st = st’ ^-) st

Establishing the following two facts allow the conclusion that the left hand side of the equivalence is indeed st.

(1) #st’ 0 st’/<0,…,#st’-2> = st st’[#st’-1] = x

(2) #st’ 0 st’ ^- = st’/<0,…,#st’-2>

All material covering the axiomatic semantics of ADTs and the use of coupling invariants had to be generated by the lecturer. Unfortunately, the formal methods students experienced less lecture time on the standard data abstraction material so that time could be spent on writing specifications. At times, we were forced to meet outside of regularly scheduled class time. Some students found this pace grueling and made their frustrations known. Evaluations consisted of take home quizzes that centered on coupling invariants, in class programming problems, and several out of class programming assignments that were based on standard applications of ADTs.

5. Object-Oriented Software Design

For the first time, students were challenged to write the formal specification of a medium-sized programming problem before writing any line of implementation code. Certainly, they already had a full year of experience doing such a task but never on a sizable problem. Students found it difficult to logically analyze nontrivial problems before writing a single line of code. After gaining more experience, they discovered that if one thoroughly analyzed the problem to a point that they could write the specification of it, the problem was indeed well understood by the developer.

A major project that was assigned during the course was the development of an elevator controller. This assignment was chosen mainly for its familiarity to most people, but it was also selected for comparison to several existing specifications of the same problem. It is included here to demonstrate the size and complexity of the programming problems that the students could formally analyze. The informal requirements consisted of a list of expected behaviors of the elevator.

1. Maintain a set of buttons that have been pushed inside the elevator (requested floor number)

2. Maintain a set of buttons that have been pushed outside the elevator (floor number at which passenger is waiting and requested direction)

3. Halt when elevator has no more requests to service

4. Service all outside requests eventually with all floors given equal priority

5. Service all inside requests eventually with all floors being serviced sequentially in the direction of travel.

The specification of the elevator scheduler follows. In words, the elevator’s new direction of movement is based on whether there exists a reason to continue in its current direction. The data structures used to maintain the current state of the elevator are the current floor (CurFloor), current direction of travel (CurDir), the set of requests internal to the elevator (InsideReqSet), and the set of requests external to the elevator (OutsideReqSet). The two predicates, ReasonToGo and PickupDropoff, evaluate whether such a reason exists. ReasonToGo determines whether it is necessary for the elevator to continue its movement in the current direction and PickupDropoff determines the necessary changes to the inside and outside request sets as passengers are picked up and dropped off at different floors throughout the building.