The VAT tool : automatic transformation of VHDL to timed automata
Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Aeronautics and Astronautics, 2004.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2005
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/17790 |
| _version_ | 1826200000437157888 |
|---|---|
| author | Nehme, Carl, 1981- |
| author2 | I. Kristina Lundqvist. |
| author_facet | I. Kristina Lundqvist. Nehme, Carl, 1981- |
| author_sort | Nehme, Carl, 1981- |
| collection | MIT |
| description | Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Aeronautics and Astronautics, 2004. |
| first_indexed | 2024-09-23T11:29:09Z |
| format | Thesis |
| id | mit-1721.1/17790 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T11:29:09Z |
| publishDate | 2005 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/177902019-04-11T11:17:11Z The VAT tool : automatic transformation of VHDL to timed automata Nehme, Carl, 1981- I. Kristina Lundqvist. Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics. Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics. Aeronautics and Astronautics. Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Aeronautics and Astronautics, 2004. Includes bibliographical references (leaves 61-66). 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. by Carl Nehme. S.M. 2005-06-02T18:39:51Z 2005-06-02T18:39:51Z 2004 2004 Thesis http://hdl.handle.net/1721.1/17790 56548635 eng 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. http://dspace.mit.edu/handle/1721.1/7582 154 leaves 6248321 bytes 6265711 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Aeronautics and Astronautics. Nehme, Carl, 1981- The VAT tool : automatic transformation of VHDL to timed automata |
| title | The VAT tool : automatic transformation of VHDL to timed automata |
| title_full | The VAT tool : automatic transformation of VHDL to timed automata |
| title_fullStr | The VAT tool : automatic transformation of VHDL to timed automata |
| title_full_unstemmed | The VAT tool : automatic transformation of VHDL to timed automata |
| title_short | The VAT tool : automatic transformation of VHDL to timed automata |
| title_sort | vat tool automatic transformation of vhdl to timed automata |
| topic | Aeronautics and Astronautics. |
| url | http://hdl.handle.net/1721.1/17790 |
| work_keys_str_mv | AT nehmecarl1981 thevattoolautomatictransformationofvhdltotimedautomata AT nehmecarl1981 vattoolautomatictransformationofvhdltotimedautomata |