Dr. Don Batory, University of Texas (firstname.lastname@example.org)
Dr. Helen Gill, Defense Advanced Research and Development Agency
Dr. Joseph Goguen, University of California at San Diego (email@example.com)
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:
Should architecture-based development techniques adopt a more formal framework?