Information Technology Reference
In-Depth Information
associates a B machine to each KAOS agent since agents are the active entities
able to perform operations. For that, all the KAOS operations that an agent has
to perform are represented by B operations. Moreover, all maintain goals un-
der the agent responsibility are translated as invariants of the corresponding B
machine. The authors of [9] provides means for transforming the security require-
ments model built with KAOS to an equivalent one in B. This abstract B model
is then refined using non-trivial B refinements that generate design specifications
conforming to the initial set of security requirements. Recently, [15] presents a
constructive verification-based approach for operationalizing requirements into
specifications expressed in an extended Event-B formalism. We can also point
out a work [12] proposing an automatically generator that transforms an extend
KAOS model into VDM++ specifications. The generator connects operations
in KAOS to those in VDM++, and entities in KAOS to objects or types in
VDM++. The generated specification contains implicit operations consisting of
pre- and post-conditions, inputs, and outputs of operations.
Nevertheless, the reconciliation presented by all of these works remains par-
tial because they don't consider all the parts of the KAOS goal model but only
the requirements (operational goals). Consequently, the formal model does not
include any information about the non-operational goals and, more important,
the type of goal refinement. Yet, non-operational goals play an important role
for requirements completeness and pertinence and provide for example the ra-
tionale for the requirements that operationalize them. In this paper, we have
explored how to cope with this problem using an approach that transform the
whole KAOS goal model to abstract Event-B models. Our approach can be con-
sidered as complementary to existing ones. Furthermore, what we present can
be very useful in practice to systematically verify that all KAOS requirements
are represented in the Event-B model.
6 Conclusion and Further Work
This paper presents an application of our method that consists in building a
goal-oriented requirements specification to derive an Event-B specification. It
confirms that GORE methods provide a possible way of building and structur-
ing formal specifications. A number of future research steps are ongoing. We
currently develop the model to represent non-functional goals and their impacts
on functional goals [21]. It is inspired from the i* method [19] and from [23].
The complete method will be defined as an extension of SysML [22]. We have al-
ready developed a support tool [21] on the TOPCASED [8] open platform based
on Eclipse and started the development of a plug-in between this tool and the
RODIN [7] open platform.
Acknowledgment
The work in this paper is partially supported by the TACOS project [11] ANR-
06-SETI-017 founded by the french ANR (National Research Agency).
 
Search WWH ::




Custom Search