Keywords

1 Introduction

The demand for software in electronic devices is rapidly increasing, also including safety-critical applications like in the automotive, medical, or avionic field [13]. Correctness-by-Construction (CbC) as proposed by Dijkstra [9], Gries [10], or Kourie and Watson [12] gives a guarantee for functionally correct software which is crucial for safety-critical applications. CbC follows an incremental approach of program construction based on a formal specification in form of pre- and postcondition pairs. The specification is refined into an implementation using a set of refinement rules. To guarantee the correctness of these refinement steps, each rule defines specific side conditions for its applicability. In comparison to CbC, classical post-hoc verification offers an approach where a program is specified and verified after implementation. As a result, when using CbC errors are likely to be detected earlier in the design process [14]. CorC [18] is a tool that supports CbC to develop single algorithms. First evaluation results show decreased verification effort compared to post-hoc verification [6, 18].

Our long-term vision is to make the construction of correct software using CbC applicable for large-scale systems, such as software product lines (SPLs). SPLs [17] enable the implementation of product families that share a common code base by managed reuse [8], therefore lowering costs and effort in producing custom-tailored software. The common and varying parts of an SPL are called features. The relationship of these features are modeled in feature models and variability realization mechanisms are used to implement their functionality. In the end, software variants can be created according to a certain selection of features. Many implementation techniques for SPLs, such as FeatureHouse [4] or DeltaJ [11], rely on object-oriented design since it is well suited to model large software systems. However, object-orientation poses some challenges for verification as fields can be globally accessed and concepts like inheritance increase the complexity of dependencies between classes. The complexity even increases for SPLs since variability is added to the code by variability realization mechanisms. Besides CbC as we pursue it, there are also other tools that implement different refinement-based approaches, such as Event-B [1] and its platform Rodin [2], ArcAngel [15], and SOCOS [5]. However, Event-B works on automata-based systems rather than on code and specifications and they all do not support the development of SPLs.

In this tool paper, we present VarCorC as an extension of CorC to develop object-oriented SPLs using CbC. In previous work, VarCorC has been developed from single variational methods [6], to feature-oriented SPLs with methods as simple procedures [7]. In this tool paper, we focus on the integration of object-orientation into VarCorC to enable the development of large-scale SPLs, since object-orientation allows for more complex projects and feature interactions over fields and objects. As specification, we use pre- and postconditions for methods and class invariants. Besides technical details of VarCorC, we also provide a workflow description from user-perspective to highlight VarCorC’s usability features. Lastly, we present a short feasibility evaluation on three case studies.

Fig. 1.
figure 1

Development process in VarCorC

Full size image

2 The Development Process with VarCorC

In this section, we describe the development process in VarCorC as shown in Fig. 1 from the perspective of developer Alice. Alice develops an SPL that implements a bank account system and has already created a feature model  . A feature model defines all features and their relationships in a tree structure. For the BankAccount SPL, Alice defined the features BankAccount (provides a base implementation of an account), DailyLimit (adds a limit that can be withdrawn from the account per day), and Interest (adds an interest to the account). Apart from the root feature BankAccount, all of the features are optional, which means that the user can select them individually. A valid selection of features is also called feature configuration and is used to form a software variant. Alice already implemented the features BankAccount, Interest, and DailyLimit in separate feature modules using feature-oriented programming (FOP)  . A feature can add new classes or extend already existing classes by adding fields, class invariants, and methods or by refining existing methods. When a method is refined, its implementation is overridden with the option for reuse by using the FOP-specific keyword original to call the implementation of that method in another feature. Analogously, the specification of a method is overridden and the predicates original_pre and original_post can be used. In previous work [7], we already proposed an extension of CbC for original calls to implement methods in an SPL.

Alice now wants to add feature Transaction to enable a transfer of money between accounts  . Therefore, she inserts a new class called Transaction which is displayed as UML-like class diagram in VarCorC  . She defines the fields src and dest of type Account, a class invariant, and methods transfer and lock to transfer money between two accounts and to lock an account such that the balance is unmodifiable. She defines these two methods with a signature and a method contract consisting of a first-order logic pre- and postcondition. Afterwards, she implements method transfer in the corresponding cbcmethod file  starting with the defined pre- and postcondition from the method contract. For the implementation, she uses the basic set of CbC refinement rules as defined by Kourie and Watson [12] and our refinement rules for method calls and original calls [7] which we display in Fig. 2. For example, to apply the assignment refinement rule a Hoare triple of the form {P} S {Q} with precondition P, postcondition Q and abstract statement S can be refined to an assignment \(\mathtt {x := E}\) with x being a variable and E an expression of the same type or subtype if and only if the side condition that precondition P implies postcondition Q where variable x has been replaced by expression is fulfilled. All of the listed refinement rules are implemented in VarCorC. For each applied refinement rule, the side condition is checked in the background by generating a proof file which is (semi)-automatically proven by the program verifier KeY [3]. Therefore, the method under development is guaranteed to be correct.

Fig. 2.
figure 2

List of refinement rules in correctness-by-construction [12] and method call and original call refinement rule [7]

Full size image

During this verification process, all variants of a method according to the feature model are generated into Java classes  . This has the advantage that (1) Alice can export correct code developed with VarCorC into other projects and (2) Alice can call externally implemented code in VarCorC when placed in these classes. As a result, Alice can decide about the degree of using CbC as opposed to using Java verified with a different tool or checked with testing.

One of VarCorC’s main usability features provides Alice with an overview on the verification status of all methods in the SPL and the traceability of errors down to one refinement step. The first is enhanced by the class view where Alice can see the verification status of all methods of a class with red and green borders. The latter is naturally supported by the refinement-based approach of CbC and displayed with red and green borders for refinement steps in cbcmethods. Additionally, Alice is notified by a change tracking mechanism that updates the verification status of single refinement steps that depend on the contract of other methods, such as method calls and original calls. For example, Alice calls method update to implement method transfer from class Account  . To guarantee the correctness of this refinement step, the specification of method update is checked to comply with the specification used in this refinement step. However, if Alice changes the specification of method update in another feature, the refinement step in method transfer has to be re-verified. VarCorC checks for these dependencies in the background and marks corresponding verification steps as “not verified” and notifies Alice about affected parts.

3 Object-Oriented Software Product Lines in VarCorC

In this section, we give implementation details for our tool VarCorCFootnote 1 which is an open-source Eclipse plug-in supporting the development of object-oriented SPLs using CbC and FOP. VarCorC captures the CbC structure of methods and classes through a meta-model modeled with Eclipse Modeling Framework.Footnote 2 The graphical editor visualizes the underlying meta-model in a tree-like structure for methods and UML-like class diagrams.

Fig. 3.
figure 3

Screenshot of VarCorC with class Account in feature DailyLimit

Full size image

In Fig. 3, we show a screenshot of VarCorC with class Account in feature DailyLimit. The project structure consists of a feature model, feature modules, and class folders. The cbcclass and cbcmethod files are split into a \({<}methodName{>}{\backslash }{<}classname{>}{.}diagram\) file, which contains the graphical information, and a \({<}methodName{>}{.}cbcmodel{\backslash }{<}classname{>}{.}cbcclass\) file which is an instance of the corresponding meta-model. The src-gen folder contains generated Java classes, which store composed software variants for the proofs.

In the bottom properties view, we show SPL information, such as all valid feature configurations or accessible fields and methods. The information displayed differs for classes and methods. In this case, we provide an overview on class invariants, fields, and methods of class Account in other features.

In the center of Fig. 3, class Account in feature DailyLimit adds two fields (DAILY_LIMIT and withdraw) and two methods (update and undoUpdate). As displayed in the properties view, both methods have already been defined for this class in feature BankAccount, which means that they are refined and can use an original call to call their implementation in feature BankAccount.

To guarantee the correctness of a whole SPL, every variant has to be correct. In FOP, each variant can have a different set of classes, classes can have a different sets of fields, class invariants, and methods, and methods can have different implementations and specifications. We use a product-based approach [20] for showing correctness. Once the verification of a refinement step in a method is triggered, all valid feature configurations are calculated such that original calls can be resolved. For each configuration, the corresponding variant in form of Java classes is generated. At the same time, a proof file is created which contains the side condition of the CbC refinement step. If all proofs are successful, the statement is considered to be correct.

Table 1. Metrics of the case studies
Full size table

Evaluation. We evaluate VarCorC regarding feasibility by implementing three case studies, namely BankAccount [21], IntegerList [19], and Elevator [16]. All case studies have already been used as benchmarks in SPL verification.Footnote 3 In Table 1, we show metrics for the case studies. The BankAccount SPL implements basic functions of a bank account and has been used throughout this paper as an example. The IntegerList SPL implements a list of integers with add and sort operations. The third case study, Elevator, implements basic functions of an elevator, such as the movement and entering and leaving of persons. We transferred the case studies into the object-oriented structure as introduced in this paper. For every class, we created cbcclass files with fields and class invariants. All methods are verified individually for all valid feature configurations in VarCorC, therefore showing correctness of the whole SPL.

4 Conclusion

We believe that the specification-first, refinement-based approach of CbC increases the awareness of correctness when developing safety-critical software in today’s engineered world. Until recently, CbC has only been used for independent algorithms. Therefore, we presented our tool VarCorC which enables program development with CbC for object-oriented SPLs. We showed, how we include object-orientation into CbC and highlighted usability features of VarCorC that streamline the development of SPLs. Currently, VarCorC relies on a product-based approach limiting its scalability. Therefore, in future work we want to experiment with more efficient approaches, such as family-based verification.