Using Multi-Viewpoint Contracts for Negotiation of Embedded Software Updates

TL;DR

This paper presents a contract-based negotiation methodology for safely updating embedded software in safety-critical systems, enabling in-field formal analysis to replace traditional lab verification.

Contribution

It introduces a novel multi-viewpoint contract approach for automated update negotiation, integrating multiple verification perspectives for embedded systems.

Findings

Effective in-field update negotiation demonstrated on automotive example

Contracts facilitate separation of verification efforts between lab and field

Method leverages existing viewpoint-specific verification techniques

Abstract

In this paper we address the issue of change after deployment in safety-critical embedded system applications. Our goal is to substitute lab-based verification with in-field formal analysis to determine whether an update may be safely applied. This is challenging because it requires an automated process able to handle multiple viewpoints such as functional correctness, timing, etc. For this purpose, we propose an original methodology for contract-based negotiation of software updates. The use of contracts allows us to cleanly split the verification effort between the lab and the field. In addition, we show how to rely on existing viewpoint-specific methods for update negotiation. We illustrate our approach on a concrete example inspired by the automotive domain.