Report on Analysis and Verification Techniques	(*)

Peter Herrmann, Heiko Krumm

Forschungsbericht/Research Report 485/1993

Universit"at Dortmund, Fachbereich Informatik, D-44221 Dortmund, Germany
Phone +49 231 755-4836, Fax -4730
{herrmann|krumm}@ls4.informatik.uni-dortmund.de

November, 1992

        * This work was funded by Digital Equipment Corporation
          under contract EERP GY-037 A

(no explicit abstract available, therefore contents and introduction follows)

Contents

1  Introduction                                                       2
2  Survey on Analysis and Verification Techniques                3
   2.1  Life Cycle Position  : : : : : : : : : : : : : : : : : : : : : : : :   4
   2.2  Modelling  : : : : : : : : : : : : : : : : : : : : : : : : : : : : :   6
   2.3  Notation  : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :  7
   2.4  Reasoning  : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 11
   2.5  Specific approaches  : : : : : : : : : : : : : : : : : : : : : : : : 16
3  TLA                                                              19
4  Work done                                                       22
   4.1  Refinement Mapping-Searcher  : : : : : : : : : : : : : : : : : : 23
   4.2  Theorem prover utilization  : : : : : : : : : : : : : : : : : : : : 25
   4.3  Examples   : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 27
   4.4  Prepared Work   : : : : : : : : : : : : : : : : : : : : : : : : : : 27
5  Experiences                                                      28
   5.1  Theorem prover based verification  : : : : : : : : : : : : : : : : 31
   5.2  OTTER-based verifications   : : : : : : : : : : : : : : : : : : : 32
   5.3  TOAST   : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 34
   5.4  RM-Searcher   : : : : : : : : : : : : : : : : : : : : : : : : : : : 37
6  Conclusion                                                       39
References                                                           42
A  Schemes for Proof Reductions                                  55
   A.1  Safety properties   : : : : : : : : : : : : : : : : : : : : : : : : : 55
   A.2  Fairness Properties  : : : : : : : : : : : : : : : : : : : : : : : : 56
   A.3  Simple Lemmata   : : : : : : : : : : : : : : : : : : : : : : : : : 57
B  "On the fly" proof algorithm                                   58


Introduction

The project `Tools for Transition Axioms Based Specifications' (EERP GY-
037) is a cooperation project between Digital Equipment Corporation and
the faculty of computer science of the University of Dortmund.  Initially,
the objections were to investigate, how computer assistance can be provided
for the application of the formal specification language TA [Har89 ].  TA is
based on the TLA-approach [Lam91  ]. After the occurence of the specification
language TLA+   [Lam92d  ], the project was redirected to this more powerful
language, that also is based on the TLA-approach.

The project has been structured into two fields:
   o construction and design (CD)
   o analysis and verification (AV)

In the CD-field more traditional types of tools are under study which support
the editing and testing of specifications (e.g.  syntax-directed editor, inter-
preter, animator).  In the AV-field we investigate, how the theory of TLA
can be utilized to provide computer assistance for the different AV-tasks of
a product development.

This report concentrates on the AV-field.  It summarizes the different AV-
methods in Chapter 2 in order to support the classification of the work done
so far. Chapter 3 gives a short overview on TLA. Chapter 4 then describes
this work which follows the two approaches of utilizing first-order logic the-
orem provers and of finite state methods, especially reachability analysis.
Chapter 5 is devoted to the experience gained by the application of tool-
prototypes to example specifications.  Chapter 6 concludes the report in
outlining the objectives of future work.

[Har89]     Paul K. Harter Jr.  Writing formal specifications using Transi-
            tion Axioms. Technical report, DEC, October 1989.
[Lam91]     Leslie Lamport.  The temporal logic of actions.  Technical Re-
            port 79, DEC Digital Systems Research Center, Palo Alto, May
            1991. Research Report.
[Lam92d]    Leslie Lamport. TLA+: Syntax and Semantics. to appear, pre-
            liminary version, DEC Digital Systems Research Center, Palo
            Alto, February 1992. Research Report.