Whereas in the past engineers were able to reuse standard designs that had been perfected over many years, most of the new systems using computer control require new designs. The complexity of these systems, furthermore, does not usually allow us to build physical prototypes and experiment with them enough to learn how to improve our designs. Instead, mathematical models must be used to verify certain required properties. An important research topic involves defining powerful and efficient modeling languages and analysis techniques to allow prediction and accumulation of information that will aid in the system and software design and verification process. Although many modeling techniques have been proposed, most consider only very limited aspects of the computer and do not adequately handle such things as timing, failures, and hazards.
Analysis is an intrinsic part of any engineering discipline--no bridge or space vehicle is constructed without enormous amounts of modeling, calculation, checking, and revision. Today's software engineer simply lacks the theory to bring to bear on engineering problems. Gerhart has suggested that the scientific basis that currently exists is a collection of micro-theories, each reasonably well understood but isolated by its own notation, techniques, and world view. Most models are related to single qualities, such as security or reliability. A few general models exist with extensive theories, such as Petri nets, but these models often lack the power to provide the required information to designers or to address the variety of qualities required in large and complex systems. Most notably lacking is knowledge of how to design systems to achieve multiple properties and an understanding of the relationships among properties including conflicts and the tradeoffs that may be required in system design. Most models also provide little help in comparing alternative system designs.
Not only do we need better formal methods, but we need ways to interface them to human abilities and to informal methods. The techniques and tools we develop must be usable by software developers and not just by the researchers that developed them, and they must be integratable into normal software development environments.