Research Seminar - March 10, 2003

Integrating Formal Methods

Abstract:

Formal methods is a field comprising a range of techniques for mathematically modelling, analysing and assisting the development of software and software-based systems. Most existing techniques focus on one aspect of such systems such as data structures and their manipulation, or concurrency and distribution, or real-time constraints. Real systems, however, generally have a combination of these aspects and, consequently, there is a growing research trend in integrating various formal methods.

This seminar will present an overview of approaches to integrating formal methods, and focus on the speaker's work on semantic integration. A simple case study will be used to demonstrate how formal languages for modelling data, concurrency and real-time can be integrated in one model while still allowing existing analysis techniques and tools to be used.

Biography: In addition to his work on integrating formal methods, Graeme Smith is one of the originators of the Object-Z formal modelling language: one of the first formal languages incorporating object orientation. He is author of the first and most comprehensive book on Object-Z (The Object-Z Specification Language, Kluwer Academic Publishers, 2000).