Formal methods have come into use for the construction of real systems as they help to increase software quality and reliability, and even though their industrial use is still limited, it has been steadily growing (Bowen & Hinchey, 2006; van Lamsweerde, 2000). When used early in the software development process, they can reveal ambiguities, incompleteness, inconsistencies, errors, or misunderstandings that otherwise might only be discovered during costly testing and debugging phases. A well-known formal method is the RAISE Method (George et al., 1995), which has been used on real developments (Dang Van, George, Janowski, & Moore, 2002). One tangible product of applying a formal method is a formal specification. A formal specification serves as a contract, a valuable piece of documentation, and a means of communication among stakeholders and software engineers. Formal specifications may be used throughout the software lifecycle and they may be manipulated by automated tools for a wide variety of purposes such as model checking, deductive verification, animation, test data generation, formal reuse of components, and refinement from specification to implementation (van Lamsweerde, 2000). However, one of the problems with formal specifications is that they are hard to master and not easily comprehensible to stakeholders, and even to non-formal specification specialists. This is particularly inconvenient during the first stages of system development when interaction with stakeholders is very important. In practice, the analysis often starts from interviews with the stakeholders, and this source of information is heavily based on natural language as stakeholders must be able to read and understand the results of requirements capture. Then specifications are never formal at first. A good formal approach should use both informal and formal techniques (Bjorner, 2000). The requirements baseline (Leite, Hadad, Doorn, & Kaplan, 2000), for example, is a technique proposed to formalize requirements elicitation and modeling, which includes two natural language models, the language extended lexicon (LEL) and the scenario model, which ease and encourage stakeholders’ active participation. However, specifying requirements in natural language has some drawbacks related to natural language imprecision. Based on the previous considerations, we proposed a technique to derive an initial formal specification in the RAISE specification language (RSL) from the LEL and the scenario model (Mauco, 2004; Mauco & Riesco, 2005a; Mauco, Riesco, & George, 2004). The technique provides a set of manual heuristics to derive types and functions and structure them in modules taking into account the structured description of requirements provided by the LEL and the scenario model. But, for systems of considerable size this manual derivation is very tedious and time consuming and may be error-prone. Besides, maintenance of consistency between LEL and scenarios, and the RSL specification is a critical problem as well as tracking of traceability relationships. In this article, we present an enhancement to this technique, which consists in the RSL-based formalization of some of the heuristics to derive RSL types from the LEL. The aim of this formalization is to serve as the basis for a semiautomatic strategy that could be implemented by a tool. More concretely, we describe a set of RSL-based derivation rules that will transform the information contained in the LEL into abstract and concrete RSL types. These derivation rules are a useful starting point to deal with the great amount of requirements information modeled in the LEL, as they provide a systematic and consistent way of defining a tentative set of RSL types. We also present some examples of the application of the rules and discuss advantages and disadvantages of the strategy proposed.
A Modular Architecture for Multi-Purpose Conversational System Development
