{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/17790"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/17790","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"The VAT tool : automatic transformation of VHDL to timed automata","abstract":"Embedded systems have become an integral part of the systems we use today. These types of systems are constrained by both stringent time requirements and limited resource availability. Traditionally, high-integrity embedded systems operated on well understood hardware platforms. The emergence of inexpensive FPGAs (Field Programmable Gate Arrays) and ASICs (Application Specific Integrated Circuits) as operational platforms for embedded software, has resulted in the system developer having to verify both the hardware and the software components. The stringent processes used over the system development lifecycle have to be augmented to account for this paradigm shift. One possible approach is to create a homogenous formal model that accounts for both the hardware and the software components of the system. This thesis focuses on making a contribution to the extraction of formal models from the VHDL specification of the operational platform. The research underlying this thesis was driven by the goals of: a) augmenting the system developer's verification and validation toolbox with a powerful yet easy-to-use tool; b) developing a tool that is modular, extensible, and adaptable to changing customer requirements; c) providing a transparent transformation process, which can be leveraged by both academia and industry. The thesis discusses in detail, the design and development of the VAT tool, that transforms VHDL specifications into finite state machines. It discusses the use of model checking on the extracted formal model and presents a visualization technique that enables manual inspection of the formal model.","abstract_html":"Embedded systems have become an integral part of the systems we use today. These types of systems are constrained by both stringent time requirements and limited resource availability. Traditionally, high-integrity embedded systems operated on well understood hardware platforms. The emergence of inexpensive FPGAs (Field Programmable Gate Arrays) and ASICs (Application Specific Integrated Circuits) as operational platforms for embedded software, has resulted in the system developer having to verify both the hardware and the software components. The stringent processes used over the system development lifecycle have to be augmented to account for this paradigm shift. One possible approach is to create a homogenous formal model that accounts for both the hardware and the software components of the system. This thesis focuses on making a contribution to the extraction of formal models from the VHDL specification of the operational platform. The research underlying this thesis was driven by the goals of: a) augmenting the system developer's verification and validation toolbox with a powerful yet easy-to-use tool; b) developing a tool that is modular, extensible, and adaptable to changing customer requirements; c) providing a transparent transformation process, which can be leveraged by both academia and industry. The thesis discusses in detail, the design and development of the VAT tool, that transforms VHDL specifications into finite state machines. It discusses the use of model checking on the extracted formal model and presents a visualization technique that enables manual inspection of the formal model.","abstract_has_math":false,"creators":["Nehme, Carl, 1981-"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics.","school":null,"contributors":[],"advisors":["I. Kristina Lundqvist."],"committee_chairs":[],"committee_members":[],"year":2004,"date_issued":"2004","date_published":"2004","updated_at":"2026-07-22T22:21:26Z","subjects":["Aeronautics and Astronautics."],"languages":["eng"],"rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/17790","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["I. Kristina Lundqvist."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics."]},{"key":"dc:creator","label":"Author","values":["Nehme, Carl, 1981-"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2005-06-02T18:39:51Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2005-06-02T18:39:51Z"]},{"key":"dc:date.issued","label":"Date","values":["2004"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Aeronautics and Astronautics."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/17790"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Aeronautics and Astronautics, 2004.","Includes bibliographical references (leaves 61-66)."]},{"key":"dc:description.abstract","label":"Abstract","values":["Embedded systems have become an integral part of the systems we use today. These types of systems are constrained by both stringent time requirements and limited resource availability. Traditionally, high-integrity embedded systems operated on well understood hardware platforms. The emergence of inexpensive FPGAs (Field Programmable Gate Arrays) and ASICs (Application Specific Integrated Circuits) as operational platforms for embedded software, has resulted in the system developer having to verify both the hardware and the software components. The stringent processes used over the system development lifecycle have to be augmented to account for this paradigm shift. One possible approach is to create a homogenous formal model that accounts for both the hardware and the software components of the system. This thesis focuses on making a contribution to the extraction of formal models from the VHDL specification of the operational platform. The research underlying this thesis was driven by the goals of: a) augmenting the system developer's verification and validation toolbox with a powerful yet easy-to-use tool; b) developing a tool that is modular, extensible, and adaptable to changing customer requirements; c) providing a transparent transformation process, which can be leveraged by both academia and industry. The thesis discusses in detail, the design and development of the VAT tool, that transforms VHDL specifications into finite state machines. It discusses the use of model checking on the extracted formal model and presents a visualization technique that enables manual inspection of the formal model."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["S.M."]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["The VAT tool : automatic transformation of VHDL to timed automata"]}]}],"canonical_facts":{"dc:contributor.advisor":["I. Kristina Lundqvist."],"dc:contributor.department":["Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics."],"dc:contributor.other":["Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics."],"dc:creator":["Nehme, Carl, 1981-"],"dc:date.accessioned":["2005-06-02T18:39:51Z"],"dc:date.available":["2005-06-02T18:39:51Z"],"dc:date.issued":["2004"],"dc:description":["Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Aeronautics and Astronautics, 2004.","Includes bibliographical references (leaves 61-66)."],"dc:description.abstract":["Embedded systems have become an integral part of the systems we use today. These types of systems are constrained by both stringent time requirements and limited resource availability. Traditionally, high-integrity embedded systems operated on well understood hardware platforms. The emergence of inexpensive FPGAs (Field Programmable Gate Arrays) and ASICs (Application Specific Integrated Circuits) as operational platforms for embedded software, has resulted in the system developer having to verify both the hardware and the software components. The stringent processes used over the system development lifecycle have to be augmented to account for this paradigm shift. One possible approach is to create a homogenous formal model that accounts for both the hardware and the software components of the system. This thesis focuses on making a contribution to the extraction of formal models from the VHDL specification of the operational platform. The research underlying this thesis was driven by the goals of: a) augmenting the system developer's verification and validation toolbox with a powerful yet easy-to-use tool; b) developing a tool that is modular, extensible, and adaptable to changing customer requirements; c) providing a transparent transformation process, which can be leveraged by both academia and industry. The thesis discusses in detail, the design and development of the VAT tool, that transforms VHDL specifications into finite state machines. It discusses the use of model checking on the extracted formal model and presents a visualization technique that enables manual inspection of the formal model."],"dc:description.degree":["S.M."],"dc:format.mimetype":["application/pdf"],"dc:identifier.uri":["http://hdl.handle.net/1721.1/17790"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Aeronautics and Astronautics."],"dc:title":["The VAT tool : automatic transformation of VHDL to timed automata"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:21:26Z"}