KIT | KIT-Bibliothek | Impressum | Datenschutz

ICARUS - Incremental Design and Verification of Software Updates in Safety-Critical Product Lines

Guissouma, Houssem; Schindewolf, Marc; Sax, Eric

Abstract (englisch):
The lifecycles of software updates for Cyber Physical Systems are significantly decreasing. Especially for safety-critical functions, these must be carefully tested for compatibility to target configurations. In order to formalize the requirements of the system and to validate software changes in a modular way, contract-based design can be used for formal verification. A contract is defined as a pair of an assumption describing the required conditions for the working environment of a component, and a guarantee, which specifies its expected behavior including timing properties and value ranges of interfaces. In this work, we present a concept for efficient verification of a software update in a contract-based development environment with consideration of several system variants. The concept is based on an incremental refinement verification methodology which uses deltas, i.e. differences between variants, to automatically propagate changes and retest only the incrementally relevant contracts. By applying the methodology in a case study for a network representing a variable Adaptive Cruise Control system, we could demonstrate its applicability and its advantages in reducing the total verification effort for product line evolution.

DOI: 10.1109/SEAA53835.2021.00055
Zugehörige Institution(en) am KIT Institut für Technik der Informationsverarbeitung (ITIV)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 27.10.2021
Sprache Englisch
Identifikator ISBN: 978-1-66542-705-0
KITopen-ID: 1000139586
Erschienen in 2021 47th Euromicro Conference on Software Engineering and Advanced Applications (SEAA). Hrsg.: IEEE
Veranstaltung 47th Euromicro Conference on Software Engineering and Advanced Applications (SEAA 2021), Online, 01.09.2021 – 03.09.2021
Verlag Institute of Electrical and Electronics Engineers (IEEE)
Seiten 371–378
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page