Abstract
In Cyber-physical systems, which are the integrations of computational and physical processes, it is hard to realize certain security properties. Fundamentally, physically observable behavior leads to violations of confidentiality. We focus on analyzing certain non-interference-based security properties to ensure that interactions between the cyber and physical processes preserve confidentiality. a considerable barrier to this analysis is representing the physical system's interactions. in this paper, these physical system properties are encoded into a discrete event system and the combined Cyber-physical system is described using the process algebra SPA. the model checker, CoPS shows BNDC (Bisimulation based Non-Deducibility on Compositions) properties, which are a variant of non-interference properties, to check the system's security against all high-level potential interactions. We consider a model problem of invariant pipeline flow to examine the BNDC properties and their applicability for cyber-physical systems. © 2009 IEEE.
Recommended Citation
R. Akella and B. M. McMillin, "Model-checking BNDC Properties in Cyber-physical Systems," Proceedings - International Computer Software and Applications Conference, vol. 1, pp. 660 - 663, article no. 5254191, Institute of Electrical and Electronics Engineers, Nov 2009.
The definitive version is available at https://doi.org/10.1109/COMPSAC.2009.101
Department(s)
Computer Science
International Standard Book Number (ISBN)
978-076953726-9
International Standard Serial Number (ISSN)
0730-3157
Document Type
Article - Conference proceedings
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2024 Institute of Electrical and Electronics Engineers, All rights reserved.
Publication Date
23 Nov 2009
