Constraint Modelling and Data Validation Using Formal Specification Languages
David Clayton Schneider · Univ. Duesseldorf: Duesseldorfer Dokumenten- und Publikationsserver · 2017
Formal methods provide rich and expressive specification languages to reason about and to describe systems at a high abstraction level. These methods are usually supported by powerful tools to verify the correctness of the specifications by different means such as proof or model checking. But is it possible to express non-trivial constraint satisfaction problems in these specification languages and to use such a formal model at runtime for problem solving and data validation? Are languages and the tools powerful enough to enable this usage scenario? These are the central questions we explore in this thesis. We look at these questions with a particular focus on the B Method – a state based formal method for software development – and the ProB tool – an animator and model checker for the B Method. We begin by studying the use of the B language, a part of the B method, not only as a specifications language but also as a modelling language for a wide range of challenging constraint based problems. We show on several puzzles and case studies that it is possible to formalize these problems elegantly using B. We also show that for many problems it is possible to solve these formalizations using ProB. We use our results on a larger case study about performing data validation of university curricula using a formal specification. In this case study we use the B language to model and validate the feasibility of university curricula from a students’ perspective and show that ProB can efficiently solve this validation problem. In particular, we show that it is possible to embed ProB in an application and solve this validation problem at runtime using our B model. Afterwards, we will present a general structure of a data validation project in B and outline common challenges along with various solutions. This discussion is rooted in the results and experiences gathered on our case study and on a second independent one. We also discuss possible evolutions of the B language to make it (even) more suitable for such projects. In the course of this thesis we discuss several alternative modelling approaches and how they relate to B and ProB. To conclude, we perform an in-depth evaluation where we compare our B and ProB based approach to several other tools and languages that can be used for this kind of validation task. We conclude that our approach of using B not only as a formal specification language but also as a constraint modelling language can be applied successfully in this scenario. Nevertheless, there are areas where this approach could be improved or extended to better suit this kind of application. We also conclude that ProB produces very good results for the high abstraction level of the language, that it is in many cases faster than brute force solutions and that it is comparable to dedicated constraint solving approaches.