Software Reliability Methods

Author: Doron Peled, Bell Labs/Lucent Technologies, Murray Hill, NJ, USA

Publisher: Springer-Verlag

Price: $59.95

ISBN: 0-387-95106-7

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 "hands-on" 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