Software Reliability Methods
Author: Doron Peled,
Bell Labs/Lucent Technologies, Murray Hill, NJ, USA
Publisher: SpringerVerlag
Price: $59.95
ISBN: 0387951067
About This Book:
The book `Software Reliability Methods' presents a collection
and comparison of current methods for dealing with software
reliability. It compares between these methods, and shows their
advantages and disadvantages. The book presents a description
of the techniques, intended for a nonexpert audience with some
minimal technical background (e.g., some training in software
engineering, or basic computer science courses). It also
describes some advanced techniques, aimed at researchers and
practitioners in software engineering.
This text/reference is intended to be used as an introduction to
software methods techniques, a source for learning about
various ways to enhanced software reliability, a reference on
formal methods technique, and also as a basis for a one
semester university course in this subject. It suggests various
projects and exercises for achieving "handson" experience with
the various formal methods tools.
Course notes (powerpoint) that accompany the book can be found
here.
Table of Contents:

Introduction

Formal Methods

Developing and Acquiring Formal Methods

Using Formal Methods

Applying Formal Methods

Overview of the Book

Preliminaries

Set Notation

Strings and Languages

Graphs

Computational Complexity and Computability

Further Reading

Logic and Theorem Proving

First Order Logic

Terms

First Order Formulas

Propositional Logic

Proving First Order Logic Formulas

Properties of Proof Systems

Proving Propositional Logic Properties

A Practical Proof System

Example Proofs

Machine Assisted Proofs

Mechanized Theorem Provers

Further Reading

Modeling Software Systems

Sequential, Concurrent and Reactive Systems

States

State Spaces

Transition Systems

Granularity of Transitions

Examples of Modeling Programs

Nondeterministic Transitions

Assigning Propositional Variables to States

Combining State Spaces

The Linear View

The Branching View

Fairness

The Partial Order View

Modeling Formalisms

A Modeling Project

Further Reading

Formal Specification

Properties of Specification Formalisms

Linear Temporal Logic

Axiomatizing LTL

Examples of LTL Specification

Automata on Infinite Words

Specification using Buchi Automata

Deterministic Buchi Automata

Alternative Specification Formalisms

Complicated Specifications

Completeness of Specification

Further Reading

Automatic Verification

State Space Search

Representing States

The Automata Framework

Combining Buchi Automata

Complementing a Buchi Automata

Checking Emptiness

A Model Checking Example

Translating LTL into Automata

The Complexity of Model Checking

Representing Fairness

Checking the LTL Specifications

Safety Properties

The State Space Explosion Problem

Advantages of Model Checking

Weaknesses of Model Checking

Selecting Automatic Verification Tools

Model Checking Projects

Model Checking Tools

Further Reading

Deductive Software Verification

Verification of Flow Chart Programs

Verification with Array Variables

Total Correctness

Axiomatic Program Verification

Verification of Concurrent Programs

Advantages of Deductive Verification

Weaknesses of Deductive verification

Soundness and Completeness of Proof Systems

Compositionality

Deductive Verification Tools

Further Reading

Process Algebra and Equivalences

Process Algebras

A Calculus of Communicating Systems

An Example: Dekker's Algorithm

Modeling Issues

Equivalences between Agents

Trace equivalence

Failure equivalence

Simulation Equivalence

Bisimulation and Weak Bisimulation equivalence

A Hierarchy of Equivalence Relations

Studying Concurrency using Process Algebra

Calculating Bisimulation Equivalence

LOTOS

Process Algebra Tools

Further Reading

Software Testing

Inspections and Walkthroughs

Control Flow Coverage Criteria

Dataflow Coverage Criteria

Propagating path conditions

Equivalence Partition

Preparing the Code for Testing

Checking the Test Suite

Compositionality

Black Box Testing

Probabilistic Testing

Advantages of Testing

Disadvantages of Testing

Testing Tools

Further Reading

Combining Formal Methods

Abstraction

Combining Testing and Model Checking

Direct Checking

Black Box Systems

Combination Lock Automata

Black Box Deadlock Detection

Conformance Testing

Checking the Reliability of Resets

Black Box Checking

The Cleanroom Method

Visualization

Using Visualizations for Formal Methods

Message Sequence Charts

Visualizing Flowcharts and State Machines

Hierarchical State Graphs

Visualizing Program Text

Petri Nets

Visualization Tools

Further Reading

Conclusion