Prof Andrew Ireland – Heriot-Watt University
Reasoned Modelling: Towards Decision Support for System Designers
Formal modelling and reasoning are closely related activities. In particular, modelling decisions are typically informed by the analysis of failed proofs. While such analysis is not intellectually challenging from the perspective of mathematical reasoning, it does represent a major barrier to the uptake of formal design methods by mainstream software engineers – whose intuitions lie in modelling and not proof. This problem is exacerbated by the huge
number of proof obligations that arise during industrial scale developments. Overcoming this barrier would increase the accessibility and productivity of formal design methods, and ultimately the dependability and security of software intensive systems. My talk will describe a programme of research called reasoned modelling which aims to reduce this barrier. In essence we are focused on the development of techniques that abstract away from the complexities of low-level proof obligations, in particular proof-failures, and provide designers with high-level modelling guidance. Our approach is based upon a classification of common modelling patterns. Combined with automatic proof-failure analysis, we use these patterns to automatically generate modelling guidance. Complementing this top-down process, we are experimenting with bottom-up AI theory formation techniques. Specifically, we are exploring how the HR automated theory formation system can be used to increase the flexibility of our modelling patterns. I will report on progress within the context of Event-B, a refinement based modelling formalism. Our longer-term vision for reasoned modelling will also be outlined. This talk is based upon joint work with Gudmund Grov, Maria Teresa Llano and Alison Pease.
Professor Andrew Ireland BSc PhD CEng FBCS CITP
Andrew Ireland is a Professor of Computer Science within the School of Mathematical and Computer Sciences at Heriot-Watt University. He studiedat the University of Stirling where he graduated with a First Class Hons degree in Computing Science and then went on to gain his PhD sponsored by a Carnegie Scholarship. Moving to the University of Edinburgh, he took up the post of teaching assistant within the then Department of Artificial Intelligence, before joining the Mathematical Reasoning Group as Research Associate –during this period he worked on techniques for automating the search for formal proofs, in particular proof by mathematical induction.
In 1995 he became a lecturer in Computer Science at Heriot-Watt University, and was promoted to Professor in 2010. He is a founder member of the Dependable Systems Group at Heriot-Watt, and has maintained close collaborative links with the Mathematical Reasoning Group. He has substantial research experience in the areas of automated reasoning and automated software engineering on which he has published widely. He has played a central role in the development of a technique called proof planning – which uses high-level patterns of reasoningin order to automate the search for mathematical proofs. He also has a strong track-record in terms of applied research in the area of software verification. Most recently he has been collaborating with BAE Systems on reasoned modelling – a formal approach to system development which extends proof planning to incorporate design knowledge — and forms the basis for his IDEAS Research Seminar. Other industrial collaborators include Altran Praxis, QinetiQ and Lemma 1. He has held numerous EPSRC grants, and is currently the PI on a Platform Grant that supports a collaborative programme of research entitled “The Integration and Interaction of Multiple
Mathematical Reasoning Processes”, which spans three sites – Heriot-Watt, Edinburgh and Imperial College.
He has wide ranging experience in organising workshops and conferences, and currently is a member of the steering committees for two internationally leading conferences, i.e. Verified Software: Theories, Tools and Experiments (VSTTE) and the IEEE/ACM International Conference on Automated Software Engineering. Most recently, he Chaired VSTTE 2010 at Heriot-Watt. He is also a member of IFIP Working Group 1.9/2.14 (Verified Software) and Co-Chairs the international Microsoft Verified Software Milestone Award Committee. More locally, he has co-ordinated the Scottish Theorem Proving seminar series since 2005 – a forum that brings together automated reasoning researchers from around Scotland, with the aim of supporting young researchers.
School of Computing, Robert Gordon University, St Andrew Street, Aberdeen, Lecture Room C48, 14:15 – 15:15.