It is obvious that the growing demand for high quality, safety, and security of software systems can be met by rigorous application of formal methods during software design. However, tools for formal methods in general do not provide a sufficient level of automatic processing. This book methodically investigates the potential of first-order logic automated theorem provers (ATPs) for applications in the area of software engineering. The book consists of a preface, an introduction, and six chapters.
In the introduction, some aspects of application of formal methods during all phases of the software life cycle are considered. The general properties of model checkers, interactive theorem provers, and ATPs are briefly discussed.
In the chapter “Formal Methods in Software Engineering,” a short overview of the role of formal methods in the area of software engineering is presented. It is explained that the use of formal methods is very important in order to avoid incomplete, inconsistent and ambiguous requirements, specifications or system descriptions.
In the chapter “Processing in Logic,” the basic notations for first-order logic are introduced and the ATP SETHEO is described. The prover SETHEO is a high-performance ATP for first-order logic in clausal normal form. It is based on the model elimination method.
In the chapter “Characteristics of Proof Tasks,” the essential characteristics of proof tasks in any application of an ATP are presented. Three application systems that use ATPs to process their proof tasks are considered: AMPHION (a system for automatic synthesis of FORTRAN programs), ILF (an interactive theorem prover), and KIV (an interactive verification system).
In the chapter “Requirements,” some requirements that an ATP should fulfill for its successful application are presented. The following requirements are considered:
- (1) expressiveness of the underlying logic;
- (2) soundness and completeness of the underlying calculus (though all practical implementations of ATPs are incomplete);
- (3) reliability of automated prover under consideration; and
- (4) ability to combine with other artificial intelligence methods.
It is desirable that an automatic prover’s capabilities should include:- (1) some forms of inductive reasoning;
- (2) equality and arithmetic;
- (3) logic simplification;
- (4) recognition of non-theorems; and
- (5) controlling of the prover.
If an ATP is to be applied successfully, it also must fulfill requirements concerning pragmatic issues like availability, support, and stability. In the chapter “Case Studies,” two case studies concerning the application of the ATP SETHEO are described:- (1) verification of cryptographic and communication protocols; and
- (2) logic-based component retrieval.
Reuse of approved software components is certainly one of the key factors for successful software engineering. Retrieving appropriate software components from a reuse library is a central task. This case study concentrates on a deduction-based approach.In the chapter “Specific Techniques for ATP Applications,” some techniques for translating non-first-order problems (inductive problems and modal logics), simplification, and handling of sorts are described.
To summarize, as the author points out, although the book is intended to facilitate practical usability of automated theorem proving in software engineering, it serves only as a single step in this direction. In the near future, all applications will need close cooperation between the designers of formal methods tools and ATPs. Only then will tools that are powerful and usable by software engineers be designed and implemented.
