A main challenge in the design of wireless-based Cyber-Physical Systems consists in balancing the need for security and the effect of broadcast communication with the limited capabilities and reliability of sensor nodes. We present a calculus of broadcasting processes that enables to reason about unsolicited messages and lacking of expected communication. Moreover, standard cryptographic mechanisms can be implemented in the calculus via term rewriting. The modelling framework is complemented by an executable specification of the semantics of the calculus in Maude, thereby facilitating solving a number of simple reachability problems.
Lecture Notes in Computer Science: 10th International Conference, Ifm 2013, Turku, Finland, June 10-14, 2013. Proceedings, 2013, p. 412-427
Cyber-Physical Systems; Broadcast communication; Denial-of-Service; Process calculus; Security protocol verification
Main Research Area:
Lecture Notes in Computer Science
10th International Conference on integrated Formal Methods (iFM 2013)Integrated Formal Methods