Software reliability methods. Foreword by Edmund M. Clarke (Q5942575)

The book presents algorithms and formal methods, which are used in software reliability tools. Some concepts from set theory, graph theory, complexity theory and compatibility are considered. The two main components of formal methods -- logic, especially linear temporal logic, and automata theory are used. The first-order logic, propositional logic, linear temporal logic, proof systems are studied. The use of formal methods usually starts with modeling the checked system as a mathematical object, therefore the problems of modeling software system and the formal specification of program properties are considered. To describe the execution of a program, one can use finite automata over infinite words called \(\omega\)-automata, the simplest class of them is that of Büchi-automata. Their properties are studied. The correctness of software is discussed as well as a collection of techniques for automatically verification properties of system with finitely many states. One of the model checking approach is based on automata theory. It allows bringing both the checked system and the specification into the same representation -- Büchi-automata. The complexity of model checking is examined. Some deductive software verification methods are presented and their advantages and weaknesses are discussed. Process algebras which are formalisms for modeling the behavior of systems are described. Some methods of testing are considered and their advantages and disadvantages are examined. It is showed how to combine the strength of different formal methods. The ways in which formal methods can take advantage of visual representation of software are discussed. Conclusions and some new directions in formal method techniques are exposed in the last chapter.