Using Multi-Viewpoint Contracts for Negotiation of Embedded Software Updates

• Published in: Electronic Proceedings in Theoretical Computer Science
• Main Authors: Holthusen, Sönke, Quinton, Sophie, Schaefer, Ina, Schlatow, Johannes, Wegner, Martin
• Other Authors: Institute of Software Engineering and Automotive Informatics (ISF), Technische Universität Braunschweig = Technical University of Braunschweig Braunschweig, Sound Programming of Adaptive Dependable Embedded Systems (SPADES), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes 2016-2019 (UGA 2016-2019 )-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes 2016-2019 (UGA 2016-2019 ), Institute of Computer and Network Engineering Braunschweig (IDA), Institut für Betriebssysteme und Rechnerverbund Braunschweig (IBR)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2016
• Subjects: [INFO]Computer Science [cs]; [INFO.INFO-ES]Computer Science [cs]/Embedded Systems; Iceland
• Online Access: https://inria.hal.science/hal-01426654; https://inria.hal.science/hal-01426654/document; https://inria.hal.science/hal-01426654/file/2016-PrePost.pdf; https://doi.org/10.4204/EPTCS.208.3

International audience 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.