Extension of Contracts for Variability Modeling and Incremental Update Checks of Cyber Physical Systems

Due to the increasing electronic and software portions in Cyber Physical Systems (CPSs), such as highly automated cars, and their safety-criticality, thorough verification and validation activities are an essential part of their development process. Meanwhile, software life cycles are getting shorter, and Over The Air updates are becoming state of the art, even in safetycritical domains. However, validating each software update for a wide range of system variants and versions is a challenging task, which requires efficient verification methods to reduce time, effort and costs. Contract-based Design (CBD) is a design paradigm to handle the complexity of safety-critical CPSs. Though, due to the multitude of maintained variants and versions, using CBD for continuous products improvement in form of updates may rapidly become challenging. In this paper, we integrate CBD into a product line development approach by mapping variant and fine-grained contracts to reusable components. Applying our approach to a case study from the automotive domain showed a significant reduction of the effort for contractifying the systems. Besides, it offers a basis for conducting incremental analysis and verification of modular updates.