Date: Wed, 20 Nov 1996 22:38:33 GMT Server: NCSA/1.5.1 Last-modified: Fri, 10 May 1996 21:55:42 GMT Content-type: text/html Content-length: 8890 CIS 841 (SE 750-KS) Software Validation and Verification Spring 1996

CIS 841 (SE 750-KS)
Software Validation and Verification Spring 1996



What's New on these Web Pages


OVERVIEW

As software systems increase in size and complexity the difficulty of assuring that they function as intended increases rapidly. A variety of approaches have been proposed that have the potential to enable development organizations and individual developers to produce higher quality software.

In general, no single technique is capable of providing incontrovertable proof that software always behaves as intended.

In this course we will examine different verification and validation approaches that are capable of providing us with evidence of software quality. Using a combination of these techniques can provide a high-degree of confidence in the quality of the software we construct.


LECTURES

Durland 164
MW 3:30-4:45 pm
Exams held in Nichols 236


INSTRUCTOR

Prof. Matt Dwyer


PREREQUISITES

CIS 740


REQUIREMENTS

The course will consist of lectures, readings, homework assignments and examinations. The bulk of the concepts in the course will be presented, explained and illustrated by way of extended examples in the lectures. The readings serve to provide more details and depth on selected concepts. Homework is designed to develop student's abilities to apply concepts and synthesize solutions to new problems based on those concepts.

Lectures and Readings
Lectures and readings function as an integrated presentation of the course material. It is expected that readings will be read prior to the appropriate lecture.
Homework
There will be four homework assignments. The assignments will involve applying and extending the concepts presented in the lectures and readings. For some of the homeworks you will be required to apply specific techniques to actual code. For these assignments I will make samples of code available that you can use; alternatively you can use a piece of code that you have developed.

Homeworks should be completed individually. Do not work with any other person. Assignments are due at the beginning of class 10%will be deducted for late assignments (an additional 10% for each day late). Off-campus students may either email their solutions to me or fax their solutions using (913)532-7353.

Examinations
There will be a comprehensive take-home final exam.

Final grades will be assigned based on the following weighting: homeworks (40%), mid-term (20%), and final (40%).


READINGS

The required readings for this course are selected papers from the literature.

If you do not have access to these papers, they have been collected and are available from Copy Co., phone number (913) 537-2679. The cost is ~$50.

In addition to the required readings you may find the following texts useful as they contain some of the material in the course. They range from general software engineering texts to in-depth treatments of issues related to particular verification and validation approaches.


ADDITIONAL RESOURCES

Web pages for course (linked off of my home page) will include assignments, solutions, lecture notes, and links to other validation and verification pages.


ORGANIZATION & SCHEDULE

The course is broken up into the following parts:

foundations
of program analysis. We cover mathematical preliminaries. How validation and verification activities relate to other software development activities. We present and discuss a variety of models that are used to represent and reason about the possible behavior of a program.

specification
of intended program behavior. How do we say what a program should do?

While there are a variety of different specification formalisms, in this course, we will focus on finite state automata specifications.

static techniques
examine the text of designs, specifications or code. One can view static techniques as a kind of abstract execution of the program. This execution produces different kinds of output than the normal program execution and that output is used to drive validation and verification efforts. This execution can be accomplished on a variety of different substrates. We will study both:
manual
techniques that use developers to perform program analyses.
automated
techniques that algorithmically perform program analyses.

dynamic techniques
involve executing an implementation with respect to the semantics of the language in which it is written. Validation and verification efforts are based on observing the behaviour of the software as it executes. This can include observing normal program output as well as probing the state of the software during different points in its execution. Well look at techniques based on both of these:
assertion based
analyses involve periodic checking of intended behavior during program execution.
testing
involves checking of software input/output relationships.

software processes
that support verification and validation provide an infrastructure in which quality assurance activities can be organized, monitored, and controlled.

software safety
in life-critical systems is emerging as an increasingly important area of quality assurance.

concurrency
is being used increasingly in distributed and parallel software. Along with increased performance comes an increase in the complexity of the already difficult problem of quality assurance. We will consider the impact of concurrency on both static and dynamic analysis approaches.


dwyer@cis.ksu.edu