Efficient Contract-based Verification of Variant-Rich Software Systems
For the verification of a variant-rich software system, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a contract-based specification technique which facilitates modular verification of product variants. Our approach allows verifying the building blocks of the product variants in isolation, based on symbolic contracts for calls to methods which may be defined in other building blocks and are unknown at verification time. When product variants are generated, these symbolic contracts are instantiated by the actual contracts of the methods in the considered product variant and established by verification of mutual consistency.
About Ina Schaefer:
Ina Schaefer leads the Institute for Software Engineering and Automotive Informatics at Technische Universität Braunschweig, Germany. Her research interests include modular modeling, the implementation of variant-rich software systems, efficient quality-assurance techniques and formal verification of software variants. She received a PhD in computer science from Technische Universität Kaiserslautern, Germany. She was a Post-Doc at Chalmers University of Technology in Gothenburg, Sweden.