Guided Requirements Clarification for Automatic Formalization

Automatic transformation from informal requirements to formal specifications is an important but challenging topic in software engineering. The major challenge stems from the fact that informal requirements are usually too abstract to provide sufficient information required for completing the formal specification. In this paper, we propose an approach to guiding the clarification of requirements to prepare for their automatic formalization on the basis of specification patterns. Each pattern provides a template for clarifying one kind of requirement by showing how it is decomposed into a set of requirement elements. Each element is formally defined to denote one of the attributes of the requirement. Clarifying a requirement is actually a process of assigning values to the relevant elements according to their formal definitions. An example of Automated Teller Machine (ATM) system is presented to illustrate the approach.