Jouke Harmen Stoel
Promotores: prof. dr. J.J. Vinju (CWI & TU/e), prof. dr. T. van der Storm (CWI & University of Groningen)
Co-promotor: prof.dr. M.G.J. van den Brand (TU/e)
Eindhoven University of Technology
Date: 8 November, 2023
Large enterprises such as banks face many challenges when it comes to controlling the every growing complexity of their systems. These systems are never created in one go, they are the result of many iterations during many decades of development. Since techniques evolve, so do these software systems. Controlling this complexity is a wicked problem since all the separate sub-systems influence each other in ways often not foreseen upfront.
One way to increase the confidence of correctness in such a system is to apply Formal Methods such as the B-method, VDM of mCRL2. Applying a formal method requires to specify the intended behavior of a system in some precise and formal notation. In turn, these specifications can be used to reason about properties of the system (such as safety properties) using theorem proving or model checking.
However, the drawback that is often mentioned on the use of such formal method in industry scale projects is that the cost of use (both in time and expertise) is conceived as too high.
A variation on the use of formal methods is to make use of a so called lightweight formal method. A lightweight formal method builds on the same principals as the earlier mentioned formal methods but with emphasis on partiality. This can either be partiality in modeling (e.g., model the core design instead of the whole system), partiality in analysis (e.g., perform model checking on a subdomain of the problem),
partiality in language (e.g., prohibit a specification language to those constructs which allow for automatic reasoning) and partiality of composition (e.g., allow for the composition of specifications focusing on different aspects for a single system). This emphasis on partiality offers trade-offs to influence the breath and depth of the applied specification and verification technique. In this thesis we explore some of
these trade-offs in the context of developing and maintaining enterprise software systems.
Firstly, we explore the impact of supporting automatic verification of a specification has on the design of such a specification language. A very expressive specification language allows for the definition of a large class of problems but will be very hard to automatically verify. We experiment with two different designs in which we balance this trade-off.
Secondly, we focus on partiality of analysis by contributing to the state-of-the-art in relational model finding. Relational model finding is a technique which allows for the definition of problems using a specification language build on a rich relational logic. In existing work of Torlak et al. such a problem is automatically translated into a boolean satisfiability problem which in turn can be solved by an off-the-shelf SAT solver. Our work generalizes this idea by extending the relational input language to contain definitions and constraints of non-relational data types (such as integers) and by translating this to a Satisfiability Modulo Theories (SMT) problem which
in turn can be solved by an off-the-shelf SMT solver. This generalization increases the expressiveness of the relational specification language while still preserving the ability for automatic verification.
Thirdly, we explore partiality of modeling and composition by designing and implementing a specification language and verification method that allows users to perform bespoke specification compositions that allow for partial model checking. These bespoke compositions allow for a modeling technique in which it is possible to specify a complete system while being able to verify parts of it. To offer these partial verification technique we draw upon well known concepts from software testing, mocking. To facilitate the verification of these partial system specifications, the specifications are translated to the language of our generalized relational model finder. We apply this new specification technique to a case study from our problem domain, banking systems, and we find that it is expressive enough to specify such a real-world problem while still retaining the possibility to perform checking of user defined properties on a subset of the specifications.
We conclude that the use of lightweight specification and verification techniques can hold value for domains that are currently not quick to adept formal methods.