Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned - Formal Methods: Foundations and Applications - page 177

Specification of a Localization Component
Driven by a Goal-Based Approach: Some
Lessons We Learned

Abderrahman Matoussi, Frederic Gervais, and Regine Laleau

Universit´eParis-Est,LACL,IUTSenart Fontainebleau,
Dpt Informatique, Route Hurtault, 77300 Fontainebleau, France
{ abderrahman.matoussi,frederic.gervais,laleau } @u-pec.fr

Abstract. The transition from the requirements phase to the formal
specification phase is one of the most painful steps in software develop-
ment. Up to now, no well-defined process to build initial formal models
has been proposed. We have proposed a method in which initial formal
models are built incrementally, driven by a goal-based approach. This
paper aims at sharing the salient points of our experience to specify
a localization component. We discuss the benefit of using a goal-based
modeling to obtain an abstract Event-B specification.

Keywords: Requirements engineering, Formal specification, Event-B,
KAOS, Localization component.

1 Introduction

Employing formal methods for critical systems specification is steadily growing
from year to year. They have shown their ability to produce and improve such
systems for large industrial problems such as Paris metro line 14 [5] or Roissy
Val [6] using the B method [1]. With most formal methods, an initial mathe-
matical model can be often refined in multiple steps, until the final refinement
contains enough details for an implementation. Most of the time, the initial
model is built from the description obtained by the requirements analysis. This
requires a high level of competence and a lot of practice, especially as there is no
well-defined process to assist designers. Therefore, it is dicult to fully compre-
hend the correspondence between requirements and initial formal specifications.
Indeed, the validation of this initial formal specification is very dicult due to
the inability for customers to understand formal models. Moreover, it is hard
for designers to link them with the initial requirements. Unfortunately, an initial
formal model may not be a correct realization of the requirements.
We have defined a method [10] to cope with this problem using a Goal Ori-
ented Requirements Engineering (GORE) approach [3] and the Event-B formal
method [2]. The main objective is to propose a constructive approach in which
abstract Event-B models are built incrementally from GORE goal models. Ap-
plying Requirements Engineering (RE) methods at the very beginning of a design