Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance

Authors
Publisher
Elsevier
Publication Date
Source
Legacy
Disciplines
• Computer Science
• Design
• Mathematics

Abstract

Science of Computer Programming 00 (2010) 1–26 Science of Computer Programming Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance Andrew Ireland1, Gudmund Grov2, Maria Teresa Llano1 and Michael Butler3 1School of Mathematical and Computer Science, Heriot-Watt University, UK 2School of Informatics, University of Edinburgh, UK 3School of Electronics and Computer Science, Southampton University, UK Abstract The activities of formal modelling and reasoning are closely related. But while the rigour of building formal models brings significant benefits, formal reasoning remains a major barrier to the wider acceptance of formalism within design. Here we propose reasoned modelling critics – an approach which aims to abstract away from the complexities of low-level proof obligations, and provide high-level modelling guidance to designers when proofs fail. Inspired by proof planning critics, the technique combines proof-failure analysis with modelling heuristics. Here, we present the details of our proposal, implement them in a prototype and outline future plans. Keywords: Reasoned modelling, formal methods, formal modelling, formal verification, automated reasoning, artificial intelligence 1. Introduction The use of mathematical techniques for system-level modelling and analysis brings significant benefits, as well as challenges. While the rigour of mathematical argument can offer early feedback on design decisions, a key challenge centres on how feedback derived from the analysis of complex proof obligations (POs) can be used to improve design decisions. Such feedback currently requires user intervention, drawing upon skilled knowledge of the subtle interplay that exists between modelling and reasoning. For example, consider a simple cruise control system with the safety requirement that the brakes (brake) cannot be on while the cruise control (cc) is enabled. This can be formalised as the following invariant: cc = on⇒ brake = off When the driver applies t

Seen <100 times