Masters Theses
Abstract
"This thesis concerns the design and verification of a real-time communication protocol for sensor data collection and processing between an embedded computer and a DSP. In such systems, a certain amount of data loss without recovery may be tolerated. The key issue is to design and verify the correctness in the presence of these lost data frames under real-time constraints. This thesis describes a temporal verification that if the end processes do not detect that too many frames are lost, defined by comparison of error counters against given threshold values, then there will be a bounded delay between transmission of data frames and reception of control frames. This verification and others presented herein were performed with the model checkers SPIN and RT-SPIN"--Abstract, page iii.
Advisor(s)
McMillin, Bruce M.
Committee Member(s)
Wilkerson, Ralph W.
Vojta, Thomas
Department(s)
Computer Science
Degree Name
M.S. in Computer Science
Publisher
University of Missouri--Rolla
Publication Date
Spring 2006
Pagination
vii, 80 pages
Note about bibliography
Includes bibliographical references (pages 78-79).
Rights
© 2006 David Andrew Cape, All rights reserved.
Document Type
Thesis - Open Access
File Type
text
Language
English
Subject Headings
Computer software -- VerificationFault-tolerant computingFlexible AC transmission systems
Thesis Number
T 8952
Print OCLC #
82368341
Electronic OCLC #
1029557479
Recommended Citation
Cape, David Andrew, "Model checking control communication of a FACTS device" (2006). Masters Theses. 4098.
https://scholarsmine.mst.edu/masters_theses/4098