Reasoned modelling: harnessing the synergies between reasoning and modelling

Conventional formal modelling requires a designer to have expertise in formal reasoning as well as design. We describe an approach to formal modelling called reasoned modelling that aims to allow the designer to focus on their design, with the low-level formal reasoning hidden from view. The approach builds directly upon the ideas of proof plans in that we make explicit use of modelling knowledge and patterns. This enables us to harness the synergies that exist between modelling and reasoning. A number of aspects of reasoned modelling have been investigated. Here we summarise the key contributions that have been previously published. First, when faced with low-level reasoning failures, we illustrate how modelling knowledge can be used to constrain the search for high-level design guidance. Second, we describe how common patterns of refinement can be used to help guide a designer. Third, we outline how common patterns of modelling can be used in suggesting design abstractions. Finally, as is the case with proof plans, reasoned modelling requires a mechanism for instantiating patterns. We describe how automated theory formation was used to instantiate patterns that arose within reasoned modelling.