Feature-oriented contract composition

Thomas Thüm

doi:10.1016/j.jss.2019.01.044

Feature-oriented contract composition

2019-06-01

6

PRE

AI

DOI：10.1016/j.jss.2019.01.044

原文链接

原文求助

摘要

En 中文

A software product line comprises a set of products that share a common code base, but vary in specific characteristics called features. Ideally, features of a product line are developed in isolation and composed subsequently. Product lines are increasingly used for safety-critical software, for which quality assurance becomes indispensable. While the verification of product lines gained considerable interest in research over the last decade, the subject of how to specify product lines is only covered rudimentarily. A challenge to overcome is composition; similar to inheritance in object-oriented programming, features of a product line may refine other features along with their specifications. To investigate how refinement and composition of specifications can be established, we derive a notion of feature-oriented contracts comprising preconditions, postconditions, and framing conditions of a method. We discuss six mechanisms to perform contract composition between original and refining contracts. Moreover, we identify and discuss desired properties for contract composition and evaluate which properties are established by which mechanism. Our three main insights are that (a) contract refinement is seldom but crucial, (b) the Liskov principle does not apply to features, and (c) it is sufficient to accommodate techniques from object-orientation in the contract-composition mechanisms for handling frame refinements. (C) 2019 Elsevier Inc. All rights reserved.

Keyword:

Feature-oriented programming

Software product lines

Design by contract

Deductive verification

Formal methods

Feature-oriented contract composition

摘要

AI总结

期刊

机构

引用论文