A critical component of any engineering discipline is a collection of formal
techniques for development and analysis of the artifacts produced by engineers.
Civil engineers use structural analysis based on formalisms for characterizing
strength of materials. Chemical engineers use formalisms based on unit
operations.

What, then, do software engineers use? The sad fact is that there is little in
the way of routine formalism that is applied throughout the industry. By and
large, software engineers develop systems using informal methods and procedures
based on accumulated experience building similar systems.

The situation can be partly explained by the fact the state of the science
under-lying large-scale, commercial software development is relatively immature
[Sha90]. While there are many proposals for formal software development methods,
(such as program verification [Hoa72], rigorous programdevelopment [Gri81,
Jon86], abstract specifications of modules [GH80], and modeling of concurrency
[Hoa78]) there is no well-established body of formal foundations that are
uniformly recognized as fundamental to industrial software development. There
are, of course, notable successes of formal methods in industry (such as [Bar89,
NC88, DG90]). However, the fact remains that the primary proponents of
systematic application of formal development have been academicians and those
working in the areas of secure and safety-critical systems.

But a lack of widely-accepted, scientific underpinnings is (at best) only partly
the reason. Indeed, the emerging examples of successful development and the
application of special-purpose formalisms (eg., in areas such as protocol
verification [MS91], testing, and real-time scheduling [SG90]) indicate that the
benefits of existing formal methods are simply not being exploited.

For educators this presents both a problem and an opportunity. It is a problem
because the lack of a coherent body of widely-applicable, formal methods makes
it difficult for educators to know what and how to teach existing techniques. It
is an opportunity because it allows educators to advance the state of practice
by helping to produce fresh practitioners who are equipped with a new set of
practical, formal skills, and who can speed the broader dissemination and
adoption of formal methods in industry.

In response to this situation, the usual approach to the introduction of formal
methods in software engineering curricula is to provide a special course in
which a variety of formal techniques are surveyed, and perhaps partially
mastered by the students. Such a course satisfies the need to make students
aware of some formal approaches to software development. But it also has a
number of problems, detailed later, the most serious of which is that it tends
to isolate the use of formal methods from the main-stream activities of software
development emphasized in the rest of the curriculum.

In this paper we describe a different approach. Instead of segregating
instruction of formal methods, we attempt to integrate it across the curriculum.
To illustrate this approach we describe the recently redesigned Master of
Software Engineering curriculum at Carnegie Mellon University, and evaluate our
experience in using it to date.