Safety Analysis of Over-the-Air Updates for CPS: A Contract-Driven Approach

Over-the-air (OTA) updates are becoming a standard practice for upgrading Cyber-Physical Systems (CPS) software, allowing software systems to be modified through a wireless network. They are beneficial in several contexts. For example, in the automotive domain, OTA updates enable manufacturers to update vehicle software without physical access. However, the considerable number of products (e.g., vehicles within the fleet) and frequent changes and updates to software components can generate many software configurations that are impossible to analyze beforehand without any automated support. This problem hampers the verification of the system’s safety. This paper proposes a contract-driven framework for reasoning about the safety of OTA updates. Our framework supports (a) <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">contract composition</i>, which enables reasoning about the behavior composition of different software components, and (b) verification of <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">component substitutability</i>, which allows checking if the software component deployed by an OTA update can replace another component without generating any safety breach.We rigorously define our framework and formally prove that if the OTA update ensures the satisfaction of its contract, the system (safety) properties are preserved. We propose an instance of our solution that targets CPS designed with Simulink<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">®</sup> System Composer, a widely used tool for modeling the different components of the system architecture and their interaction. We propose using Simulink<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">®</sup> Requirements Tables to express the contracts of CPS components, as they enable engineers to model the system requirements using pre/post-conditions within their Simulink<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">®</sup> models. We implemented our solution as a software prototype that extends THEANO, a tool that enables engineers to verify the consistency and completeness of Requirements Tables. We evaluated our solution by considering the Ten Lockheed Martin Cyber-Physical Problems. We defined 20 OTA updates and effectively identified issues in 9 of them. We analyzed and fixed the problems, inspecting each unsafe OTA update to understand the causes of the safety breaches. After fixing the problems, THEANO confirmed the safety of all OTA updates. THEANO required less than a minute to analyze each OTA update, making it practical for industrial applications.