Computer Science

Colloquium Details

Managing Change in Evolving Specifications: Practical and Theoretical Issues

Abstract

Flight software has become the critical cost factor for the new generations of aircraft and spacecraft. Accordingly, NASA is investigating ways to reduce cost and increase quality in the development of real-time embedded software. In particular, the use of formal methods is being studied as a promising approach for automated early lifecycle analyses. However, a number of factors currently limit the practical application of formal methods. In particular, the current generation of formal methods are weak at handling evolution in specifications and reasoning about change.

In this talk, I will discuss the problems of reasoning about evolving specifications, covering both the short term and long term research questions. To motivate the work, I will briefly summarize a recent case study that we conducted for NASA, in which we analyzed a Change Request (CR) for the Space Shuttle Flight Software to automate the East Coast Abort Landing (ECAL) guidance functions. Currently, Shuttle change requests are verified using manual consistency checking and inspection. The case study examined the use of the SCR method to automatically check the correctness, consistency and completeness of the specification, as well as to simulate the behavior of the system for validation. The case study revealed a number of ambiguities and minor errors in the specifications.

Two key research issues have arisen in this work. The first is the critical role that structure plays in the evolution of specifications. Structure is important both for isolating change, and as a basis for comparison between different versions of a specification. The second issue is toleration of inconsistency: for practical reasons it is desirable to be able to perform some analysis even in the presence of known inconsistencies in a specification. To address these issues we have been exploring the use of specification morphisms in a category theoretic framework to capture and reason about the structure of specifications. We are also exploring the use of lazy consistency checking over partial specifications in a distributed software development environment. I will briefly explain the theory behind this work, and then demonstrate how this might be applied to support practical formal analysis in evolving specifications.

Biography

Dr. Steve Easterbrook is a Research Associate Professor at the Institute for Software Research in West Virginia, USA. For the past three years he has managed a team of research staff and graduate students, pursuing a mixture of basic and applied research in software verification and validation, at the NASA IV&V facility in Fairmont, WV. 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.

Dr. Easterbrook's research interests are in requirements engineering, lightweight formal methods and software specification, and he has published over 30 papers in refereed international journals and conferences. He is editor of a book CSCW: Co-operation or Conflict? (Springer) and is currently Editor-in-Chief of Requirenautics Quarterly, the Newsletter of the BCS Requirements Engineering Specialist Group. He has served on numerous international conference program committees, including those of both the annual symposium and the annual conference on requirements engineering, the international workshop on software specification and design, and the international conference on software engineering and knowledge engineering. He also serves on the editorial board of the Automated Software Engineering Journal (Kluwer).