Verifying Contract-Based Specifications of Product Lines using Description Logic

The complexity of critical systems is constantly increasing and if developed as Product Lines (PLs), the number of possible system configuration can be huge. Consequently, assuring system properties such as safety or security is increasingly difficult. Assurance cases are used often to argue that a system is safe or secure and Contract-Based Specification (CBS) models are a promising foundation for assurance case argumentation. This paper defines a method for Description Logic (DL) based verification of the well-formedness constraints of an arbitrary CBS model of a PL. The paper presents the DL encoding of arbitrary CBS model, the DL encoding of the well-formedness constraints, and shows how the verification of these constraints can be reduced to satisfiability verification of the corresponding knowledge base. In order to validate the presented approach, a small, but real, industrial PL was expressed as a CBS model, implemented as an OWL ontology, and an off-the-shelf reasoner was used to verify if the CBS model is well-formed.QC 20181106