Case Study about Formal and Informal Specifications through an Industrial
Abstract: 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. The object of our case study is the teletext module of a new generation TV. We have discussed our experience, and presented an analysis of both the specifications. We found 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 their specification process basedon our findings.
Introduction: In this paper, we perform a comparative study of formal specifications and informal specifications. We have taken a medium size system from a project in industry, and have specified it both formally and informally. For the formal specification, we used B [Abr 96] as the specification language, and for the informal specification, we used UML [Boo 99]. Our most important conclusion is that UML is not sufficient to specify requirements, which may be complex and rigorous in nature. Some amount of formality is necessary to take care of particularly complex issues. Conversely we found that the UML was helpful for visualising the structure of the models compared with a formal specification. keep reading..
