Contract-based Specification and Description-Logic-Based Validation of Product Lines

The complexity of critical systems is constantly increasing. Consequently, assuring properties like safety or security of such systems is increasingly difficult. The difficulties are only intensified in the Product-Line Engineering (PLE) context, where properties of a complete family of systems, i.e. a Product Line (PL), must be assured. Contract-Based Specification and Design (CBSD) paradigm is a promising approach for alleviating these difficulties because it is a general-purpose, formal paradigm, developed purposely to support structured development of complex systems which are correct-by-design. Starting from a general CBSD framework, we present an extension that supports using CBSD in PLE, and prove that the extension preserves the properties of the original framework. Then, as a step towards providing tool-support for CBSD specification of PLs, we define the encoding of an arbitrary CBSD model of a PL, together with the constraints which define a proper CBSD model, as a Tbox of a description logic knowledge base. Finally, we show how verification of these constraints can be reduced to satisfiability verification of the corresponding knowledge base. In order to validate the presented approach, a CBSD specification of a small, but real, industrial PL is created, implemented as an OWL ontology, and an off-the-shelf reasoner was used to verify if the provided CBSD model is proper.QC 20180731