An Event-B formalization of KAOS goal refinement patterns

Goals play an important role in requirements engineering process, and consequently in systems development process. Whereas specifications allow us to answer the question ”WHAT the system does”, goals allow us to address the ”WHY, WHO, WHEN” questions . Up to now, the main software development approaches using formal methods,such as Event-B, begins at the specification level. Our objective is to include requirements analysis within this process, and more precisely the KAOS method, which is a goal-oriented methodology for requirements engineering. The latter allows analysts to build requirements models and to derive requirements documents. Existing work that combine KAOS with formal methods generate a formal specification model from a KAOS requirements model. We aim at expressing KAOS goal models with a formal language (Event-B), hence staying at the same abstraction level. Thus we take advantage from the Event-B method: it is possible to use the method during the whole development pro-cess and (ii) we can benefit from the industrial maturity of tools supporting the method. For that purpose, we propose a constructive approach in which Event-B models are built incrementally from KAOS goal models, driven by goal refinement patterns