Requirements Engineering Formal Analysis of the Shlaer-Mello(3)

In this paper, we define a number of tools that we think belong to the core of any toolkit for requirements engineers. The tools are conceptual and hence, they need precise definitions that lay down as exactly as possible what their meaning and possible us

d methods has resulted in some interesting and useful additions to the more classical techniques. However, it does mean that in order to define a useful toolkit, we should not forget to include the tools that have proven their value in a number of widely used methods. In addition to claiming that we need a set of methodindependent tools that are, where possible, familiar to the software engineer, we claim that the definition of these tools should be done by formal means even if the tools themselves are semi-formal. By ensuring that semi-formal notations such as diagrams have formal counterparts, we eliminate redundancy, inconsistency, and ambiguity in the semi-formal notations and this makes them easier to use in practice. For example, we will show in this paper that the specification of object behaviour and object communication by means of diagrams can be simplified considerably if we take carethat the diagrams have precisely defined counterparts in a formal specification. This use of formal specifications does not require practitioners to ever write one letter of a formal specification, but it does demand from the tool-builders that they provide a formal theory for each tool that they produce. The situation is similar with other engineering tools: the user of a hammer does not need to have any knowledge of metallurgy or classical mechanics, but the manufacturer of a hammer does. Formal techniques not only help in the definition of conceptual tools and techniques, they also help in the definition of software tools that support the use of conceptual tools. It is one of the hallmarks of engineering that the behaviour of a product is predicted before it is implemented; this in turn requires specification of external product behaviour before the product is implemented. The conceptual tools for requirements specification are used for precisely this: to specify external product behaviour. They also should allow prediction of product properties from the specification. But this ability requires that the semi-formal notations have a formal semantics. Once we have this formal semantics, we can build software tools that allow us to predict product properties by, for example, performing reachability analysis or by animation of possible product behaviours. Backing up semi-formal notations by formal semantics therefore helps us to improve the software product engineering process. The Statemate notation and tool is a good example of this mutual enhancement of formal techniques and semi-formal notations [8,19,20]. Research in the integration of formal and semiformal techniques is scarce. Most research in this area has been done on the integration of structured analysis with formal specification techniques. France and Laro rondo-Petrie [21] give a survey. In a recent paper, Bates et al. [22] present an integration of Z with Fusion. They exclude life cycle specification from their formalisation. Feijs, Jonkers and Middelburg look at a large number of semi-forma