Consistency management of contexts and features in context-oriented programming language with SAT solving

Details

Supervisors

Mens, Kim ; Legay, Axel ; Duhoux, Benoît

Faculty

Ecole polytechnique de Louvain

Degree label

Master [120] en sciences informatiques

Abstract

We extended the feature-based context-oriented programming language with the usage of a SAT solver. It provides us a new way to verify at run time if the current configuration of our models is valid and if any modification we want to apply to the configuration is valid. The other reason we decided to use this SAT solver is that it allows us to detect anomalies inside our models. After the presentation of some concepts used throughout this thesis such as feature model, feature-based context-oriented programming, SAT solvers and anomalies, we will show how we implemented the use of the SAT solvers inside the feature-based context-oriented programming, what are its performance compared to the already existing configuration verification strategy and finally how the SAT solver can help us detect anomalies. We will see how we can convert the different models of the language to the CNF format needed by the solver, how we can concretely detect the anomalies and all the formulas we used. We also implemented a fuzzer to help us benchmark the performance. He can automatically creates models with given parameters and also provides the possibility to automatically create anomalies inside the models.