This is a technical paper that discusses the empirical studies and
controlled experiments of the integration of formal methods into an
undergraduate software engineering curriculum. The experiment is
motivated, for the most part, by evaluating the application of formal
analysis techniques and its influence in increasing the efficiency and
the understandability of undergraduate students toward complex problem
solving skill at Miami University of Ohio. The experimental results
are based on two group of students: one group, formal group, composed
of the students who have been exposed to both object-oriented design
and formal methods; and the other group, control group, are students
who taken only a course in object-oriented design using UML. Each
group, in turn, is subdivided into the two-people teams of
students. 

The student population of the control group consists of a random
sample of system analysis majors, whereas the students population of
the formal methods group is self-selected. Both groups are assigned to
develop and implement same project, namely, an elevator system. The
investigators believed that they had paid special care to make both
group the same in terms of learning skills and competitiveness using
ACT tests. The tests did not show any statistical difference between
the learning capabilities of both group of students. The investigators
concluded the superiority of formal method techniques using the
systems produced by formal group. They have shown that the formal
group had produced a perfect system in terms of functional correctness
(100 percent program correctness) and a better design.  

I have found a number of problems, which undermine my
confidence. Problems include the experience, the understandability,
and the skills of the formal group; the students in the formal group
have received much more challenging assignments, training, and
instructions compared with the control group. Therefore, it is hard
for me to believe that both groups are equivalent in terms of skill,
exposure and competitiveness. The validity of this experiment and its
complete weakness have already been discussed in details by Berry and
Tichy.