Introduction to Formal Modeling

Tuesday, September 10^th from 14⁰⁰ - 17³⁰

The aim of this tutorial is to introduce a number of practical formal techniques for modeling and analyzing requirements. We will discuss the role of formal modeling in RE; introduce a number of specific techniques for formal modeling; compare such techniques, and provide some criteria for when and how to apply them. The aim of the tutorial is purely practical: the tutorial will demonstrate how to select and apply an appropriate modeling and analysis technique, irrespective of whether the project to which it is to be applied routinely uses any formal specification languages. Along the way, the tutorial will explain why some formal methods are inappropriate for requirements engineering.

The tutorial draws on our experiences with lightweight formal techniques applied to NASA programs, in which we demonstrated that formal techniques offer a great deal of value as a modeling tool for analysis of mission critical software requirements, without incurring the expense of writing complete formal specifications. However, we will not focus exclusively on real time embedded systems. For example, we will also illustrate how formal techniques can be used to model features and analyze feature interaction in desktop application software.

The tutorial is aimed primarily at practitioners involved in requirements analysis. The emphasis is on practical techniques that are suitable for immediate application on large-scale software development projects. The tutorial is suitable for all levels of experience, but primarily targeted at intermediate and advanced level software engineering practitioners. Beginners will find the tutorial useful in shaping their ideas of what the requirements process is, and how various techniques can be applied. Advanced practitioners of requirements analysis will find the techniques we cover to be a useful complement to the range of analysis techniques available to them. No prior experience is assumed of requirements engineering, formal methods, nor the particular techniques covered.

Steve Easterbrook is an associate professor in the Department of Computer Science, University of Toronto, Canada, where he teaches courses in Software Engineering and Requirements Engineering, and conducts research into requirements modeling, management of inconsistency in specifications, requirements negotiation, and multi-valued model checking. Dr Easterbrook received his B.Sc. in Computer Science from the University of York, UK, in 1986, and his Ph.D. in Software Engineering from Imperial College London in 1991. He was a lecturer in computer science and artificial intelligence at the University of Sussex in the UK for five years, where he pioneered a number of innovative teaching methods for software engineering. He was then appointed research lead at the NASA Independent Verification and Validation Facility in West Virginia, where he conducted applied research into requirements engineering, software V&V, and formal methods, as part of a NASA-wide program of research and development in software engineering, aimed at improving the current state of practice in the development and assurance of high-risk, high assurance software systems. He moved to Toronto in 1999. He has published over 35 papers in the field of requirements engineering, and has edited a book on Computer Supported Collaborative Work. He has served on the program committee for the international symposia and conferences in Requirements Engineering, as well a number of other international Software Engineering conferences. In 2001, he served as General Chair for the International Symposium on Requirements Engineering, which was held in Toronto.

Back to overview