Abstract
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.
Recommended Citation
D. Cape et al., "Verifying Noninterference in a Cyber-Physical System the Advanced Electric Power Grid," Proceedings of the 7th International Conference on Quality Software, Institute of Electrical and Electronics Engineers (IEEE), Jan 2007.
The definitive version is available at https://doi.org/10.1109/QSIC.2007.4385521
Meeting Name
7th International Conference on Quality Software
Department(s)
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
text
Language(s)
English
Rights
© 2007 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.
Publication Date
01 Jan 2007
