"Model Checking Control Communication of a FACTS Device" by Bruce M. McMillin, J. K. Townsend et al.
 

Abstract

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.

Meeting Name

2006 International Conference on Parallel Processing Workshops (ICPPW'06)

Department(s)

Computer Science

Keywords and Phrases

DSP; FACTS; FACTS Device; RT-SPIN Model Checker; SPIN Model Checker; Communication; Control; Controller Area Networks; Digital Signal Processing Chips; Embedded Computer; Field Buses; Flexible AC Transmission Systems; Formal Verification; Lossy; Model Checking Control Communication; Model-Checking; Protocols; Real-Time; Realtime Communication Protocol; Sensor Data Collection; Sensor Data Processing; Telecommunication Control; Temporal Verification; Transmission Delay; Verification

Document Type

Article - Conference proceedings

Document Version

Final Version

File Type

text

Language(s)

English

Rights

© 2006 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.

Publication Date

01 Jan 2006

Plum Print visual indicator of research metrics
PlumX Metrics
  • Usage
    • Downloads: 32
    • Abstract Views: 3
  • Captures
    • Readers: 3
see details

Share

 
COinS
 
 
 
BESbswy