A Unified Approach to Verification and Validation of Software Systems

CS378 – Fall 2005

Unique Number - 54172

J.C Browne

browne@cs.utexas.edu

1. Goal and Purpose

Correctness is the most critical concern of the software industry. The goal of this course is to make available to students in Computer Sciences at the University of Texas unique training in verification and validation across functional, security and performance properties. Students successfully completing this course will find themselves with a unique and highly valuable and saleable skill. They will also be part of an NSF project for developing and applying a unified approach to verification and validation of software systems. They will also work with state of the art tools and methods for verification and validation.

1.1 Background

The methods and tools which are available for validating and verifying software includes static analysis of program code, conventional and systematic testing, model checking for temporal properties, runtime monitoring, and formal proofs of correctness. Yet there does not exist a unified approach to verification and validation which integrates the several methods and tools for verification and validation. Teaching of verification and validation reflects this fragmentation. This course is part of an effort to provide such a unified and integrated approach. The instructor and Profess Calvin Lin have obtained funding from the National Science Foundation to develop a unified approach to verification and validation and an undergraduate course teaching this unified approach.

The two unifying concepts are a “universal” property specification language from which properties can be verified by static analysis, testing, model checking, proof methods or compiled to runtime monitors as appropriate or required and the insight that all methods of verification and validation are searches of the state space of a program for truth or falsity of specified properties. A third unifying conceptual element is the common set of component-oriented set of design principles which enable effective and scalable application of both formal and informal validation and verification.

1.2 Course Content

The lectures will cover the principles and methods. The participants in the course will follow an example through the steps in an integrated process. They will also evaluate the tools which are available for each aspect of the method. Participants will come away from this course with a unique perspective on verification and validation.

The principles and mechanisms for validation and verification are language independent but the tools implementing the mechanisms are language specific. The lectures will be largely language independent but the examples and the outside assignments will use Java and C. A substantial portion of the lectures will be devoted to design for verification and validation and an integrated and comprehensive approach to specification of properties to be verified and evaluated.

The content for the course will include:

Design for test and verification.
Unified Property Specification
Introduction to program analysis (static analysis methods).
Formal and complete approaches to testing:

Specification of properties, behaviors and assertion

Test coverage algorithms based on static analysis processes

Testing as a continuous process integrating runtime monitoring with conventional testing, model checking and proof-based verification.

Applied model checking:

Model checking as the endpoint of testing

Property formulation

Compositional reasoning

Classical Dijkstra/Hoare and other proof-based verification.

This material is already covered in other courses and will not be repeated but the role of this material in a comprehensive approach to verification and validation will be covered.

g. Run-Time Monitoring

Methods and Tools

Automated compilation of property monitors.

h. Integration of all the methods in a coherent, complete structure for validation and verification.

i. Extension of verification and validation to security policy issues such as information flow.

j. Failure analysis, fault-tolerance, practical self-stabilization, etc.

k. Verification and validation of non-functional properties such as performance.

2. Student Prerequisites

Upper division standing. CS 336, CS 337 and CS 375 are desirable. Students may wish to consult with the instructor either by email (browne@cs.utexas.edu), by telephone (471-9579) or in person before registering for this course.

3. Texts and Course Materials

The text for this course is “Software Reliability Methods” by Doron A. Peled. There are many monographs and texts focusing on each topic concerning validation and verification (particularly testing). There are survey and tutorial articles and a large amount of web-based material is available on each topic and these will be used in the class.

4. Course Work and Grading

This is mainly a project course but there will be a single examination about two-thirds of the way through the semester. Grades will be assigned on the basis of the presentation, the report and content of the project and will be based 50% on the project, 25% on the examination and 25% on outside assignments which will be given early in the semester.

5. Approximate Lecture Schedule

An approximate lecture schedule follows. The time allocated for each topic may vary. There will be several guest lectures by experts on some of the topics.

Lecture Date	Lecture Topic	Reference Material
9/1/05	Unified Approach to Verification and Validation	Lecture Notes
9/6/05	Review of Background – Sets and Logics, Searches and Proofs	Peled – Chapters 2 and 3 and Lecture Notes
9/8/05	Designing for Verification and Validation	Lecture Notes
9/13/05	Models and Abstractions	Peled – Chapter 4, lecture notes and web references
9/15/05	Property Specification and a Unified Property Specification Language	Peled – Chapter 5, Lecture Notes and Web references
9/22/05	Property Specification – Examples: Temporal Logics, Pre-conditions and Post-conditions, Design Contracts, etc	Lecture Notes, web references
9/24/05	Property Specification – Examples: Temporal Logics, Pre-conditions and Post-conditions, Design Contracts, etc	Lecture Notes, web references
9/29/05	Testing – Transition from informal to structured testing	Peled – Chapter 9, lecture notes and web references
10/4/05	Testing – Transition from informal to structured testing	Peled – Chapter 9, lecture notes and web references
10/6/05	Fundamentals of Model Checking	Peled – Chapters 4,5 and 6. lecture notes, web reference materials
10/11/05	Fundamentals of Model Checking	Peled – Chapters 4,5 and 6. lecture notes, web reference materials
10/13/05	Introduction to Runtime Monitoring	Web reference material
10/18/05	Introduction to Static Analysis	TBD
10/20/05	Introduction to Static Analysis	TBD
10/25/05	Translation/Abstraction based Unification of Static Analysis, Testing, Model Checking and Runtime Monitoring	Peled – Chapter 10, Lecture Notes
10/27/05	Class Examination
11/1/05	Hoare/Dijkstra Proof Methods	Peled – Chapter 7
11/3/05	Automated Formal Proof Methods	Guest Lecture
11/8/05	Specification and Verification of Non-functional Properties – Performance and Security	Lecture notes and web materials
11/10/05	Process Algebras and Process Calculi	Peled – Chapter 8
11/15/05	Project Presentations
11/17/05	Project Presentations
11/22/05	Project Presentations
11/29/05	Project Presentations
12/1/05	Project Presentations
12/6/05	Verification/Validation in In Practice – Case Study	TBD
12/8/05	Verification/Validation in Practice – Case Study	TBD