Information Technology Reference
In-Depth Information
process and before using formal methods can be interesting since these meth-
ods provide a rich way of structuring and documenting the entire requirements
documents. Among them, the GORE paradigm is particularly well-suited for
requirements engineering since it is nearer to the way humans think and it is
easy to understand by all stakeholders. Moreover, it offers some benefits such as
(i) providing the rationale for requirements and explaining them to stakeholders;
(ii) identifying the responsibilities and the system boundaries.
In RE methods, two kinds of requirements are identified. Functional require-
ments specify the functions that the system-to-be must be able to perform and
non-functional requirements capture properties or constraints under which the
system-to-be must operate, such as performance, quality, security concerns. Gen-
erally existing RE methods build models where functional and non-functional
requirements are closely related. However it appears in practice that these two
kinds of requirements do not evolve over time in the same way and that func-
tional requirements are more stable than non-functional ones. This is why our
method is based on the definition of three models. The first one describes func-
tional requirements and is the base for deriving formal specifications in Event-B.
The second one describes non-functional requirements and the last one describes
the impacts of non-functional requirements on functional requirements. In this
paper, we focus on the functional requirements model and the derivation of for-
mal specifications. We have chosen the KAOS [4] GORE method to specify this
model, mainly because both KAOS and Event-B advocate the use of refinement
techniques and have the ability to model both the system and its environment.
This article describes the application of our method in the framework of a
research project, called TACOS [11]. We present here an experience with the
specification of a localization software component that used GPS, Wifi and sen-
sors technologies. The remainder of this paper is organized as follows. Section 2
overviews the KAOS concepts that we consider in our approach and the Event-
B formal method. Sections 3 presents and illustrates our proposed approach
through the specification of a localization software component. Relevant issues
and related work are discussed in Sections 4 and 5. We conclude our paper in
Section 6 with an outline of future work.
2 Background
In this section, we briefly introduce KAOS and Event-B.
2.1 KAOS Method
KAOS (Keep All Objectives Satisfied) [4] is a goal-based requirements engineer-
ing method. It provides five complementary sub-models describing the system
and its environment: a goal model, an agent model, an operation model, a be-
havior model and an object model. In this article, we focus on the goal model
where the main concept is the concept of goal. A goal is a prescriptive state-
ment of intent the system should satisfy through cooperation of its agents[4].
Search WWH ::
Custom Search