Formal methods application: an empirical tale of software development

Author

Sobel, Ann E Kelly ; Clarkson, Michael R.

Author_Institution

Dept. of Comput. Sci. & Syst. Anal., Miami Univ., Oxford, OH, USA

Volume

28

Issue

3

fYear

2002

fDate

3/1/2002 12:00:00 AM

Firstpage

308

Lastpage

320

Abstract

The development of an elevator scheduling system by undergraduate students is presented. The development was performed by 20 teams of undergraduate students, divided into two groups. One group produced specifications by employing a formal method that involves only first-order logic. The other group used no formal analysis. The solutions of the groups are compared using the metrics of code correctness, conciseness, and complexity. Particular attention is paid to a subset of the formal methods group which provided a full verification of their implementation. Their results are compared to other published formal solutions. The formal methods group´s solutions are found to be far more correct than the informal solutions

Keywords

computer science education; formal logic; formal specification; object-oriented programming; software metrics; code correctness; elevator scheduling system; first-order logic; formal methods; formal specifications; object oriented design; software development; software engineering curriculum; software metrics; undergraduate students; Application software; Programming;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.991322

Filename

991322