Model Checking Control Communication of a FACTS Device

This paper concerns the design and verification of a realtime 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 define and verify the correctness in the presence of these lost data frames under real-time constraints. This paper 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.

• Type: Conference
• Year: 2006
• Where: ICPPW
• Authors: David A. Cape, Bruce M. McMillin, James K. Townsend
• Keywords: Data Frames, Distributed And Parallel Computing, ICPPW 2006, Realtime Communication Protocol, Sensor Data Collection