Incremental Contract-based Verification of Software Updates for Safety-Critical Cyber-Physical Systems

Software updates are indispensable for the continuous development of Cyber Physical Systems (CPS): They allow for low-cost bug-fixing, fast adaptation to new or changing environments, or adding new functionality throughout the CPS’s life-cycle. Due to the urgent need for some safety-critical updates, their verification and validation may need to happen as fast as possible without loss of quality. For this reason, incremental checks targeting specifically the introduced changes and their impact on the system are essential as they speed up the validation process. In this paper, we introduce a concept for such an incremental verification for different types of updates by using contract-based design and verifying the integration of the introduced changes by checking their compliance with the contractually agreed assumptions and guarantees. We demonstrate our approach by applying two update types to an Adaptive Cruise Control (ACC) system and verifying the impact of the changes within the environment of the changed module(s).