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
- The final exam is now online.
- Homework assignment 3 part B is now online.
- Someone asked for a clarification regarding data flow criteria.
It appears I mis-spoke in discussing a hint on collecting data for
assignment 3, part A. Here is the clarification:
- I know that some of you are having significant technical problems
with the course. By this I mean delays in receiving tapes, receiving
blank tapes and variability in the audio quality of tapes. I'd
like to try to assess how wide-spread this is. If I find that
it is a problem for a significant number of you I plan on
complaining to NTU. I'm not sure if it will do any good, but its
worth a try. So, send me your feedback.
- If you have any other comments on the way the course is being
taught please feel free to let me know (it will not affect your grade).
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.
- There are a number of general software engineering
text. This text does a good job with software quaility issues:
Fundamentals of software engineering,
C. Ghezzi, M. Jazayeri and D. Mandrioli,
Prentice-Hall
- The following two texts cover a broad range of
testing techniques and contain significant practical
information for testers.
Software Testing Techniques,
B. Beizer,
Van Nostrand Reinhold,
The Craft of Software Testing,
B. Marick,
Prentice-Hall
- Representations and algorithms for data flow analysis are
covered in most compiler books. A good example is:
Compilers : Principles, Techniques, and Tools,
A.V. Aho, R. Sethi and J.D. Ullman,
Addison-Wesley
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