A process algebraic mutation framework with application to a vehicle charging protocol

Modern day renewable and smart energy systems are increasingly playing an important role in our societies. Electric vehicle charging services infrastructures are becoming ever more popular and accessible, although at a pace that we argue is not well understood yet in terms of the reliability and security of this new paradigm. Often solutions are rolled out to the market with little or no analysis of their resilience and even at the standards level, specifications of systems and protocol often omit or skim over the question of reliability. In this paper, we propose a new formal approach for analysing the effects of single failures on process algebraic specifications used often in specifying communication protocols. We apply this new approach to one part of an international standard protocol, the Open Charge Point Protocol, for electric vehicle charging, and demonstrate how the effects of specification faults can impact the safety and security of the protocol.