The New Jersey Institute of Technology's
Electronic Theses & Dissertations Project

Title:	An automata-based automatic verification environment
Author:	Meng, Yi
View Online:	njit-etd2005-132 (x, 92 pages ~ 4.5 MB pdf)
Department:	Department of Computer Science
Degree:	Doctor of Philosophy
Program:	Computer Science
Document Type:	Dissertation
Advisory Committee:	Gunter, Elsa L. (Committee co-chair) Gehani, Narain (Committee member) Mili, Ali (Committee member) Nakayama, Marvin K. (Committee member) Slind, Konrad (Committee member)
Date:	2005-08
Keywords:	Software engineering Formal method Formal verification Linear temporal logic Buchi automata Model checking and theorem proving
Availability:	Unrestricted
Abstract:	With the continuing growth of computer systems including safety-critical computer control systems, the need for reliable tools to help construct, analyze, and verify such systems also continues to grow. The basic motivation of this work is to build such a formal verification environment for computer-based systems. An example of such a tool is the Design Oriented Verification and Evaluation (DOVE) created by Australian Defense Science and Technology Organization. One of the advantages of DOVE is that it combines ease of use provided by a graphical user interface for describing specifications in the form of extended state machines with the rigor of proving linear temporal logic properties in a robust theorem prover, Isabelle which was developed at Cambridge University, UK, and TU Munich, Germany. A different class of examples is that of model checkers, such as SPIN and SMV. In this work, we describe our technique to increase the utility of DOVE by extending it with the capability to build systems by specifying components. This added utility is demonstrated with a concrete example from a real project to study aspects of the control unit for an infusion pump being built at the Walter Reid Army Institute of Research. Secondly, we provide a formulation of linear temporal logic (LTL) in the theorem prover Isabelle. Next, we present a formalization of a variation of the algorithm for translating LTL into Büchi automata. The original translation algorithm is presented in Gerth et al and is the basis of model checkers such as SPIN. We also provide a formal proof of the termination and correctness of this algorithm. All definitions and proofs have been done fully formally within the generic theorem prover Isabelle, which guarantees the rigor of our work and the reliability of the results obtained. Finally, we introduce the automata theoretic framework for automatic verification as our future works.