A Comparative Study of Formal and Informal Specifications through an Industrial Case Study

(Preliminary draft: 16 Feb 2000)

Author(s): The EMPAF Group

Abstract

The number of studies to compare the relative merits and the demerits of formal verses informal specification is quite few. In this paper, we discuss a case study in which we have taken a problem from industry and specified it both in B and UML. We have discussed our experience, and presented an analysis of both the specifications. Our observations are many. Our most important observation is that, in order to specify a real-time event-driven system, some amount of formality is necessary, which UML does not usually provide. Our industrial collaborators are considering changing e their specification process based on our findings.