{"id":{"repo_id":"njit","oai_identifier":"oai:digitalcommons.njit.edu:dissertations-1786"},"canonical_url":"https://search.dev.ndltd.org/etd/njit/oai:digitalcommons.njit.edu:dissertations-1786","repository":{"repo_id":"njit","name":"NJIT","base_url":"https://digitalcommons.njit.edu/do/oai/"},"display":{"title":"An automata-based automatic verification environment","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 Buchi 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.","abstract_html":"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 Buchi 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.","abstract_has_math":false,"creators":["Meng, Yi"],"institution":null,"degree_name":"Doctor of Philosophy in Computing Sciences - (Ph.D.)","degree_level":null,"degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Elsa L. Gunter","Narain Gehani","Ali Mili"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2005,"date_issued":"2005-08-31T07:00:00Z","date_published":"2005-08-31T07:00:00Z","updated_at":"2026-07-24T03:23:04Z","subjects":["Software engineering","Formal method","Formal verification","Linear temporal logic","Buchi automata","Model checking and theorem proving","Computer Sciences"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://digitalcommons.njit.edu/dissertations/731","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Elsa L. Gunter","Narain Gehani","Ali Mili"]},{"key":"dc:creator","label":"Author","values":["Meng, Yi"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:type","label":"Dc Type","values":["Dissertation"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctor of Philosophy in Computing Sciences - (Ph.D.)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Software engineering","Formal method","Formal verification","Linear temporal logic","Buchi automata","Model checking and theorem proving","Computer Sciences"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://digitalcommons.njit.edu/dissertations/731"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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 Buchi 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."]},{"key":"dc:title","label":"Title","values":["An automata-based automatic verification environment"]}]}],"canonical_facts":{"dc:contributor":["Elsa L. Gunter","Narain Gehani","Ali Mili"],"dc:creator":["Meng, Yi"],"dc:description.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 Buchi 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."],"dc:identifier":["https://digitalcommons.njit.edu/dissertations/731"],"dc:subject":["Software engineering","Formal method","Formal verification","Linear temporal logic","Buchi automata","Model checking and theorem proving","Computer Sciences"],"dc:title":["An automata-based automatic verification environment"],"dc:type":["Dissertation"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_name":["Doctor of Philosophy in Computing Sciences - (Ph.D.)"]},"updated_at":"2026-07-24T03:23:04Z"}