Automated verification of model-based programs under uncertainty
Thesis (M. Eng. and S.B.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_US |
| Published: |
Massachusetts Institute of Technology
2005
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/28453 |
| _version_ | 1811086850941517824 |
|---|---|
| author | Mahtab, Tazeen, 1981- |
| author2 | Gregory T. Sullivan and Brian C. Williams. |
| author_facet | Gregory T. Sullivan and Brian C. Williams. Mahtab, Tazeen, 1981- |
| author_sort | Mahtab, Tazeen, 1981- |
| collection | MIT |
| description | Thesis (M. Eng. and S.B.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004. |
| first_indexed | 2024-09-23T13:35:41Z |
| format | Thesis |
| id | mit-1721.1/28453 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T13:35:41Z |
| publishDate | 2005 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/284532019-04-11T06:37:55Z Automated verification of model-based programs under uncertainty Mahtab, Tazeen, 1981- Gregory T. Sullivan and Brian C. Williams. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis (M. Eng. and S.B.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004. Includes bibliographical references (p. 89-91). Highly robust embedded systems have been enabled through software executives that have the ability to reason about their environment. Those that employ the model-based autonomy paradigm automatically diagnose and plan future actions, based on models of themselves and their environment. This includes autonomous systems that must operate in harsh and dynamic environments, like, deep space. Such systems must be robust to a large space of possible failure scenarios. This large state space poses difficulties for traditional scenario-based testing, leading to a need for new approaches to verification and validation. We propose a novel verification approach that generates an analysis of the most likely failure scenarios for a model-based program. By finding only the lost likely failures, we increase the relevance and reduce the quantity of information the developer must examine. First, we provide the ability to verify a stochastic system that encodes both off-nominal and nominal scenarios. We incorporate uncertainty into the verification process by acknowledging that all such programs may fail, but in different ways, with different likelihoods. The verification process is one of finding the most likely executions that fail the specification. Second, we provide a capability for verifying executable specifications that are fault-aware. We generalize offline plant model verification to the verification of model-based programs, which consist of both a plant model that captures the physical plant's nominal and off-nominal states and a control program that specifies its desired behavior. Third, we verify these specifications through execution of the RMPL executive itself. We therefore circumvent the difficulty of formalizing the behavior of complex (cont.) software executives. We present the RMPL Verifier, a tool for verification of model-based programs written in the Reactive Model-based Programming Language (RMPL) for the Titan execution kernel. Using greedy forward-directed search, this tool finds as counterexamples to the program's goal specification the most likely executions that do not achieve the goal within a given time bound. by Tazeen Mahtab. M.Eng.and S.B. 2005-09-26T20:33:03Z 2005-09-26T20:33:03Z 2004 2004 Thesis http://hdl.handle.net/1721.1/28453 57029952 en_US 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 91 p. 4340049 bytes 4350214 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Mahtab, Tazeen, 1981- Automated verification of model-based programs under uncertainty |
| title | Automated verification of model-based programs under uncertainty |
| title_full | Automated verification of model-based programs under uncertainty |
| title_fullStr | Automated verification of model-based programs under uncertainty |
| title_full_unstemmed | Automated verification of model-based programs under uncertainty |
| title_short | Automated verification of model-based programs under uncertainty |
| title_sort | automated verification of model based programs under uncertainty |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/28453 |
| work_keys_str_mv | AT mahtabtazeen1981 automatedverificationofmodelbasedprogramsunderuncertainty |