Paper Info
Title
Model-Checking BNDC Properties in Cyber-Physical Systems
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.
Year
DOI
Venue
2009
10.1109/COMPSAC.2009.101
COMPSAC
Keywords
Field
DocType
bisimulation equivalence,control engineering computing,discrete event systems,natural gas technology,pipelines,process algebra,security of data,Model checking BNDC properties,bisimulation based non deducibility on compositions,cyber-physical systems,discrete event system,security process algebra,Bisimulation based non-deducibility on compositions,Cyber-physical system,Security,model-checking
Model checking,Intelligent decision support system,Physical system,Computer science,Information security,Theoretical computer science,Cyber-physical system,Bisimulation,Application software,Process calculus,Distributed computing
Conference
Volume
ISSN
Citations 
1
0730-3157
13
PageRank 
References 
Authors
1.04
4
2
Name
Order
Citations
PageRank
Ravi Akella1525.28
Bruce McMillin226440.75