Towards Enhancing Security and Resilience in CPS: A Coq-Maude based approach

yber-Physical Systems (CPS) have gained considerable
interest in the last decade from both industry and
academia. Such systems have proven particularly complex and
provide considerable challenges to master their design and ensure
their functionalities. In this paper, we intend to tackle some
of these challenges related to the security and the resilience of
CPS at the design level. We initiate a CPS modeling approach
to specify such systems structure and behaviors, analyze their
inherent properties and to overcome threats in terms of security
and correctness. In this initiative, we consider a CPS as a
network of entities that communicate through physical and
logical channels, and which purpose is to achieve a set of tasks
expressed as an ordered tree. Our modeling approach proposes a
combination of the Coq theorem prover and the Maude rewriting
system to ensure the soundness and correctness of CPS design.
The introduced solution is illustrated through an automobile
manufacturing case study.