More Abstraction

Abstract

Based on 10+ years of formal modelling in industry, I advocate the use of domain theories and modelling patterns in system modelling. When modelling a system, one has to somehow encode some domain data structures into some mathematical notation (e.g., set-theory for Event-B). This encoding is not trivial, except for very simple case studies. Inlining this encoding within a model makes it difficult to read and consequently difficult to prove. It is much better to separate the encoding in a separate file (i.e., a theory) which will describe the data structure, provide operators for updating it together with proof rules for reasoning about them. The model is then free from clutter and can be expressed at the same level of discourse as domain experts. I think that AI could provide significant benefits by detecting when a model is not at the correct level of discourse and contains too much encoding. This could be detected by inspecting the model and assessing its intrinsic complexity. This would be particularly useful for beginners who usually have difficulty to separate concerns. Another use of AI is to implement refinement plans (see paper by Grov, Ireland and Llano presented at ABZ 2012). In this setting, a failing proof is analysed with respect to some refinement patterns and the tool suggests amendment to the model that would allow to fix its proof. I think that it would be much more valuable if the refinement patterns would be in the form of generic models. The tool would then propose to instantiate the generic pattern and suggest ways to instantiate it (e.g., provide actual parameters). This would reuse not only the pattern but also its associated proof. The user would only have to prove that the actual parameters fulfill the pattern pre-conditions. More generally, AI could be used to mine existing models to extract generic patterns from them. This would allow to build a library of recurring patterns. As for refinement plans, AI could also be used for guiding users within the library and help them select the appropriate patterns with respect to their modelling needs. In conclusion, using both theories and generic model patterns makes models more easy to develop, read and prove, by allowing better reuse. AI could be of great help in assisting users for making the better use of these tools.