The advanced electric power grid is a complex real-time system having both cyber and physical components. While each component may function correctly, independently, their composition may yield incorrectness due to interference. One specific type of interference is in the frequency domain, essentially, violations of the Nyquist rate. The challenge is to encode these signal processing problem characteristics into a form that can be model checked. To verify the correctness of the cyber-physical composition using model-checking techniques requires that a model be constructed that can represent frequency interference. In this paper, RT-PROMELA was used to construct the model, which was checked in RT-SPIN. In order to reduce the state explosion problem, the model was decomposed into multiple sub-models, each with a smaller state space that can be checked individually, and then the proofs checked for noninterference. Cooperation among multiple clock variables due to their lack of notion of urgency and their asynchronous interactions, are also addressed.

Meeting Name

7th International Conference on Quality Software


Computer Science

Keywords and Phrases

Decomposition; Frequency Domain; Interference; Model Checking; Real-Time System

Document Type

Article - Conference proceedings

Document Version

Final Version

File Type





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

Publication Date

01 Jan 2007