This technical paper discusses several empirical studies and controlled
experiments arising from the integration of formal methods into an
undergraduate software engineering curriculum. The experiment was
motivated, for the most part, by a need to evaluate the influence of
formal analysis techniques on teaching efficiency, and on the ability
of undergraduate students to gain complex problem solving skills.
The experiments took place at Miami University of Ohio, and studied
two groups of students: the first group, the “formal
group,” was composed of students who were exposed to both
object-oriented design and formal methods. The second group, the
control group, was students who had taken only a course in
object-oriented design using Unified Modeling Language (UML). Each
group was subdivided into two-person teams. The population of the
control group consisted of a random sample of system analysis majors,
whereas the population of the formal methods group was
self-selected. Both groups were assigned a project to develop and
implement an elevator system. The investigators believed that they had
taken special care to make both groups the same, in terms of learning
skills and competitiveness, by using ACT tests. The tests did not show
any statistical difference between the learning capabilities of each
group of students. The investigators concluded the superiority of
formal method techniques, using the systems produced by the formal
group. They showed that the formal group produced a perfect system, in
terms of functional correctness (100 percent program correctness), and
had a better design.
I found a number of problems in this research, which undermine my
confidence in the results. These problems include the experience, the
understanding, and the skills of the formal group; the students in the
formal group had received much more challenging assignments, training,
and instruction as compared to the control group. Therefore, it is
hard for me to believe that both groups were equivalent in terms of
skill, exposure, and competitiveness. The validity of this experiment,
and its complete weakness, has already been discussed in detail by
Berry and Tichy.