Improving Traceability between KAOS Requirements Models and B Specifications

The aim of this paper is to give some feedback about the B specification [1] of a localization software component which is one of the most critical parts in the land transportation system. The main difficulties when we develop a localization component is: (i) to find the correct algorithm that merges positioning data (ii) to take into account all the properties we have to deal with. At this stage, we think that a semi formal model such as KAOS [2], a goal-based requirements engineering method, will be very useful in order to have guidelines on how to do. For that, we will just focus on the architecture of the B specifications and how using KAOS help us to build it. Since goals play an important role in requirements engineering process, rather than establishing traceability from the KAOS requirements model as a whole, we propose to establish traceability from individual goals that are part of the KAOS goal model. The main idea is to specify a correspondence rule between each concept of the goal model and B elements. Up to now, we consider only functional goals of type Achieve [2]. A B machine is associated to each goal. This machine contains an operation that “realizes” the goal; i.e. it describes the “work” to perform to reach the goal, in terms of generalized substitutions. The refinement of a goal is represented by a B refinement machine that refines the machine; the abstract operation is refined by a concrete one. This operation is built by combining operations of the machines that correspond to the sub-goals of the more abstract goal and are included in the B machine via the inclusion relationship. The nature of the combination depends on the goal refinement pattern (Milestone, AND, OR). The reader can refer to [3] for more details. The main contribution of our approach is that it establishes the first brick toward the construction of the bridge between the nonformal and the formal worlds as narrow and concise as possible. Furthermore, by discharging the proof obligations generated by the B refinement process, we can prove some properties of consistency on the goal model. Regarding the different KAOS goal model concepts, we need now to consider the translation of the concepts of domain properties and non functional goals.