Panel I

Formal Methods and Software Architecture: Prospects for Influencing Software Development

Co-Chairs: Mark Gerken (gerkenm@rl.af.mil) and Helen Gill

Panelists:

Dr. Don Batory, University of Texas (batory@cs.utexas.edu)

Dr. Helen Gill, Defense Advanced Research and Development Agency

Dr. Joseph Goguen, University of California at San Diego (jgoguen@ucsd.edu)

Dr. Klaus Havelund, NASA/Ames

Dr. Carolyn Talcott, Stanford University

Synopsis: The growth in the use of computer systems in the home and in schools has resulted in a new generation of people to whom using a computer is second nature. This growth in the integration of computer systems into wider sectors of our society has resulted in an increased reliance on software systems, but how reliable is this software? We've all heard about the Ariane 5 Flight 501 that ended in failure as a result of software exception raised during a data conversion from a 64-bit floating point number to a 16-bit integer. Another notorious software failure occurred when recent tests on new software lead to a 16-hour collapse of the air traffic control system monitoring planes flying from the Pacific Coast of the United States to Hawaii and the Far East. The source of other software errors, such as those of the Mars Pathfider Probe, were identified through formal analysis techniques.

Partially in response to managing the complexity of large scale systems and partially in an attempt to discover the source of software errors prior to system implementation, researchers and developers have been placing an increased emphasis on architectural modeling and analysis. Several languages and analysis tools have been developed for this purpose, and some degree of success in complexity management and error elimination has been achieved through these techniques. For example, researchers at Stanford and at Carnegie Mellon Universities used architectural analysis techniques to discover problems with the High Level Architecture (HLA) standard for distributed simulation. The problems they discovered were at least partially responsible for the issuance of a revision to the standard. In addition, some researchers have had success using architectural modeling to develop powerful software generators. However, the level of formality within the software architecture community varies considerably.

As noted by Geoff Dromey, ``there is but one chance of overcoming these problems, and that is to recognize computing science for what it really is, a mathematically-based discipline concerned with the application of rigorous methods for the specification, design, and implementation of computer systems.'' This panel seeks to address the role of formal methods in software development in general, and more specifically, the role of formal methods can or should play in architecture-based modeling, analysis, and development. This panel will debate the following questions:

  • What impact has formal methods and/or architectural modeling had to date on the software development process? How far have we come with respect to generating software that meets its specifications?

  • What are the prospects for improving our ability to develop satisfactory software, and what techniques hold the most promise in this regard?

    Should architecture-based development techniques adopt a more formal framework?

  • Generally, formal, architecture-based development techniques have not seen widespread adoption among software developers. How can the utility of these techniques be improved, and how can we foster wider adoption?

  • What domains hold the most promise for adopting formal and/or architecture-based development techniques?

  • What are the future prospects of formal methods and architecture-based development for positively affecting the software development process? And finally,

  • How should future software developers be trained to take advantage of these techniques?