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

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.