Model checking control communication of a FACTS device
"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 RE-SPIN"--Abstract, leaf iii.
McMillin, Bruce M.
Wilkerson, Ralph W.
M.S. in Computer Science
University of Missouri--Rolla
vii, 80 leaves
© 2006 David Andrew Cape, All rights reserved.
Thesis - Citation
Library of Congress Subject Headings
Computer software -- Verification
Flexible AC transmission systems
Print OCLC #
Link to Catalog Record
Full-text not available: Request this publication directly from Missouri S&T Library or contact your local library.http://laurel.lso.missouri.edu/record=b5771794~S5
Cape, David, "Model checking control communication of a FACTS device" (2006). Masters Theses. 4098.