Solving model-based constraint satisfaction problems using SMT prover

OData support
Supervisor:
Szatmári Zoltán
Department of Measurement and Information Systems

Complex design environments based on Domain-Specific Languages (DSLs) are widely used in various phases of model driven development from specification to testing in order to capture the main concepts and relations in the application domain. A precise system model captured in a DSL enables formal analysis and automated code or test generation of proven quality. Unfortunately, the specification of DSL may itself contain conceptual flaws, which invalidates the results of subsequent formal analysis of the system model. The main objective of the current report is to provide formal analysis of a DSL itself to highlight inconsistency, incompleteness or ambiguity in DSL specifications.

However, the consistency analysis of DSLs is a difficult task due to (i) decidability problems of handling complex DSLs, (ii) theoretical challenges of supporting well-formedness constraints and derived features and (iii) the engineering problem of providing a DSL validation tool that is operable by the DSL developer without any extra validation skills.

In this report, I address these challenges by providing

(i) a mapping of well-formedness rules and derived features formulated in different constraint languages into first order logic theories processed by SMT-solvers,

(ii) powerful approximations to map complex structures into an efficiently analysable fragment of first order logic,

(iii) a DSL validation tool seamlessly integrated into industrial modeling frameworks (EMF) where inconsistencies retrieved by SMT-solvers are available as regular DSL instance models.

The DSL validation framework is based on a mapping, which takes an EMF metamodel with derived features, a set of well-formedness constraints (captured in OCL) and a partial model as input. This partial model is completed by introducing new model elements to it which are compliant with the DSL specification using the generated axioms and underlying theories of the Z3 SMT-solver in the background.

The work presents the successful using of the validation framework in R3COP ARTEMIS case study which has industrial requirements. The case study aims to develop safety critical autonomous systems like industrial robots. The validation framework supported the automatic generation of concrete test cases from abstract test properties defined in standard OCL.

Downloads

Please sign in to download the files of this thesis.