VarCorC: Developing Object-Oriented Software Product Lines Using Correctness-by-Construction

Abstract

Functional correctness is an important concern, especially in the field of safety-critical systems. Correctness-by-Construction (CbC) is an incremental software development technique to create functionally correct programs guided by a formal specification. The specification is defined first, and then the program is incrementally created using a small set of refinement rules that define side conditions preserving the correctness. CbC is mostly used to create small algorithms. However, software in-field is often larger and more complex to meet the requirements of today’s life. Therefore, our vision is to scale the applicability of CbC to larger scale software systems, like software product lines (SPLs). SPLs are one way to implement a whole product family by managed reuse. Advanced implementation techniques for SPLs rely on object-orientation and variability realization mechanisms on the source code level. In this tool paper, we present our tool VarCorC which supports the development of correct SPLs using CbC including object-orientation and feature-oriented programming. We describe VarCorC from user-perspective and explain how it works internally. Additionally, we provide a feasibility evaluation of VarCorC on three case studies that are used as benchmarks in the field of product line verification.