Informatica 40 (2016) 29–42 29
Expressing GMoDS Models into Object-Oriented Models Using the Event-B
Language
Marius Brezovan, Liana Stanescu and Eugen Ganea
University of Craiova, Romania
E-mail: {mbrezovan, lstanescu, eganea}@software.ucv.ro
Keywords: multi-agent systems, goal-oriented specification, object-oriented specification, Event-B
Received: July 24, 2015
Among the agent-oriented methodologies that use goals for specification of multi-agent systems, the Goal
Model for Dynamic Systems (GMoDS) method allows to specify goals during requirements engineering
process and then to use them throughout the system development and at runtime. Because the semantics of
the GMoDS models involves the use of object-oriented concepts we choose to express a GMoDS model in
an object-oriented specification. We use Event-B as a method for both specifying the GMoDS models and
implementing the semantics of the runtime model of GMoDS. Because Event-B is not an object-oriented
language, the goal of our research is to add support to Event-B for object-oriented modeling by using the
modularization plug-in of the Rodin framework. This aim of paper is twofold: (a) to describe an object-
oriented specification in Event-B, and (b) to express a GMoDS model into an object-oriented Event-B
specification.
Povzetek: Razvit je agentni sistem z dodatnimi lastnostmi objektnih sistemom.
1 Introduction
In recent years the domain of multi-agent systems (MAS)
is perceived as generating a new paradigm in order to
cope with the increasing need for dynamic applications that
adapt to unpredictable situations. This new software engi-
neering domain, agent-oriented software engineering, pro-
vides the tools and techniques to use in designing complex,
adaptive systems.
Several frameworks for multi-agent system specifica-
tion have been proposed to deal with the complexity of
large software systems, such as Tropos [22], Gaia [5],
MaSE [11], and ROADMAP [21]. To reduce the com-
plexity of a correct and effective design for such sys-
tems, Organization-based Multi-Agent Systems (OMAS)
have been introduced as an effective paradigm for address-
ing the design challenges of large and complex MAS [18].
In OMAS there is a clear separation between agents and
system, allowing a reduction in the complexity of the sys-
tem. To support the design of OMAS, several methodolo-
gies have been proposed [16].
Among these proposals, the Organization-based Multi-
agent Systems (O-MaSE) methodology [12] seems to be
the only framework which integrates a set of concrete tech-
nologies aimed at facilitating industrial acceptance through
situational method engineering. In O-MaSE methodology,
goals are specified using Goal Model for Dynamic Systems
(GMoDS) [13], a methodology that provides a set of mod-
els for capturing system level goals, for using them during
both the design and runtime phases, in order to allow the
system to adapt to dynamic problems and environments.
The development of correct/safe complex MAS is dif-
ficult with traditional software development methods.
Hence, formal methods are needed in order to ensure their
correctness and structure their development from specifi-
cation to implementation. To that end, formalization is
needed, which has begun to receive a substantial amount of
interest. Several approaches for formalizing MAS develop-
ment are proposed. For instance, in [19] a general frame-
work for modelling MAS based on Object-Z and state-
charts is proposed, which focuses on organizational aspects
in order to represent agents and their roles. Similarly, in
[24] Z notations are combined with linear temporal logic
to specify the internal part of agents and the specification
of the communication protocols between agents. In [8], an
approach based on capturing interaction protocols between
requesters, providers and middle-agents as finite state pro-
cesses represented using FSP process algebra is proposed,
and the resulting specifications are formally verifiable us-
ing FLTL temporal logic.
However these approaches do not address the the prob-
lem of using formal methods within a well-defined MAS
development methodology. This is the reason for our at-
tempt to use the Event-B both as a method to specify the
O-MaSE models, and as a tool to implement the seman-
tics and the runtime model of O-MaSE. Event-B is a state-
based formal method that supports a refinement process in
which an abstract model is elaborated towards an imple-
mentation in a step-wise manner. In addition Event-B is
proven to be applicable in a wide range of domains, includ-
ing distributed algorithms and multi-agent system develop-
ment. Its deployment is supported by the Rodin toolset,
30 Informatica 40 (2016) 29–42 M. Brezovan et al.
which includes proof obligation generation and verifica-
tion through a collection of mechanical provers. Rodin was
used in several academic and complex industrial size sys-
tems.
We started our research with the study of the GMoDS
methodology, an important part of O-MaSE, by translating
GMoDS models in object-oriented specifications in Event-
B. GMoDS represents a framework for developing com-
plex multi-agent systems using goals to capture require-
ments, the same set of goals being used for MAS design,
and at runtime. In GMoDS, goals are organized in a goal
tree such that each goal is decomposed into a set of sub-
goals using AND/OR decomposition. Leaf goals are simple
goals that must be achieved by agents. Within O-MaSE,
each MAS contains a set of roles that it can use to achieve
its goals. The roles for MAS can be derived from the goal
tree, each leaf goal should have at least one role that can
achieve it. For simplicity, we assume that is an one-to-one
mapping between the set of goals and the set of roles. Each
agent from a MAS is capable of playing at least one role,
with the property that at every moment, an agent can have
only one role. Thus, at every moment, an agent from MAS
is related to a leaf goal from the goal tree of the GMoDS
framework.
In GMoDS, there are two types of goals: goal classes
and goal instances. Goal classes define templates from
which goal instances are created. A goal class contains a
set of goal attributes that are used to define the state od a
goal instance. When a goal is instantiated, all its attributes
must be given explicit values. While goal classes are used
in the design process of MAS, the goal instances are used at
runtime, or during a simulation process. Goal classes and
goal instances are analogous to object classes and object
instances from the object-orientation paradigm. This is the
reason for using an object-oriented framework to specify
the GMoDS models.
Event-B extended with several facilities, such as mod-
ularity, decomposition, the use of records and generic in-
stantiation, shows a good potential for the use in the indus-
trial practice. Unfortunately the Event-B language is not
object-oriented because it does not support the main object-
oriented concepts, such as inheritance, subtyping, class in-
stantiation, calling of public methods of class instances,
and polymorphism. Some approaches, such as records
[17], modularisation [20], generic instantiation [26], and
especially the UML-B method [27], bring closer Event-
B to an object-oriented language. The UML-B graphical
modelling notation provides four kind of diagrams: pack-
age, context, class and state machine diagrams. However,
UML-B does not address some important object-oriented
concepts, such as subtyping, polymorphism, and calling
public methods of the class instances. Because GMoDS
models involve the use of calling operations of some ob-
jects within the plans from the plan models, we use in-
terfaces and modules from the modularisation plug-in of
the Rodin framework, and the principles from the UML-
B method for managing classes, class instances, class at-
tributes and associations, in order to allow appropriate
object-oriented specifications in Event-B. In addition we
model in Event-B specifications other two main object-
oriented concepts: inheritance and polymorphism. Inheri-
tance is needed for creating dynamic trees of goal instances
from the GMoDS runtime model, while polymorphism is
needed for calling the appropriate operation, when a class
hierarchy is used.
In conclusion, the aim of this paper is twofold: (a) to
propose an extension of the Event-B method that allows the
creation and destruction of class objects, as well the call of
public methods of classes, inheritance, and polymorphism,
as well as (b) to use this extension for translating GMoDS
models into Event-B object-oriented specifications.
The rest of this paper is organized as follows. Section
2 presents the O-MaSE methodology framework, and its
associated GMoDS methodology. Section 3 presents the
main concepts of the Event-B method, and some of its ex-
tensions that will be used in the paper. Section 4 presents
a proposal for constructing an object-oriented specification
in Event-B that allows calling public methods of class in-
stances. In Section 5 this proposal is used to express the
main GMoDS models using object-oriented Event-B spec-
ifications. Finally, conclusions are given in Section 6.
2 O-MaSE and GMoDS
methodologies
The Organization-Based Multiagent System Engineering
[12] methodology extends the original MaSE [11] method-
ology to allow the design of organizational multi-agent sys-
tems. The definition of O-MaSE consists of three main
components: the O-MaSE meta-model, method fragments,
and guidelines.
The O-MaSE Meta-Model is based on an organizational
approach, which extends the organization model for adap-
tive computational systems (OMACS) [10]. OMACS de-
fines an organization as a set of Goals that the organization
is attempting to accomplish, a set of Roles that must be
played to achieve those goals, a set of Capabilities required
to play those roles and a set of Agents who are assigned to
roles in order to achieve organizational goals. The environ-
ment is modeled using the Domain Model, which defines
the types of objects in the environment and the relations
between them. In addition to OMACS, the O-MaSE meta-
model adds new concepts, such as: Plans that capture al-
gorithms that agents use to carry out specific tasks, Actions
that allow agents to perceive or sense objects in the en-
vironment, Organisational agents that capture the notion
of organizational hierarchy, and Protocols that define in-
teractions between roles or between the organization and
external actors. Figure 1 shows a simplified OMACS meta-
model.
In a multi-agent organization (MAO), organizational
goals are typically organized in a goal tree. In OMACS,
and thus in O-MaSE, goals are specified using GMoDS
Expressing GMoDS Models into. . . Informatica 40 (2016) 29–42 31
possesses
Organization
Capability
capableachieves
Goal Role Agent
requires
Figure 1: Simplified OMACS metamodel.
[13]. The GMoDS specification model includes the notions
of goals, goal decomposition, events, precedence, and goal
instantiation. The GMoDS instance model captures the dy-
namics of the system state while maintaining the structure
of the specification model. The execution model imple-
ments these models in an efficient manner. The GMoDS
specification model is used in the design process of a MAO,
while the GMoDS instance and execution models are used
in execution, or simulation processes of MAOs. Both in
the design process, and in the execution process, the leaf
goals are directly related to the agent plans. A GMoDS
goal specification tree is presented in Fig. 2 (from [13]).
Legend:
g2
P
<<or>>
g1
g3 g4
P
g6
x:X
g7
y:Y
e1(x:X)
<<and>>
g0
<<or>>
y:Y
g8
e2(y:Y)
g5
Create instance:
Precedes:
Subgoal:
Figure 2: A GMoDS Goal specification tree.
A basic O-MaSE process is presented in Fig. 3.
A centralized Organization-based agent architecture is
presented in Fig. 4 [12]. The Control Component con-
tains Goal Reasoning and the Reasoning Algorithm that use
specifications of the organisation goal, role, and agent mod-
els to perform reasoning about goals, and the assignment
of agents to roles. The Execution Component contains the
agents of the MAO specified by their roles and capabilities.
From the Control Component, Goal Reasoning is the
module that implements the GMoDS framework. In this
paper we describe a specification of the Goal Reasoning
module using an object-oriented extension of the Event-B
method.
Model agent classes
SRS
Model goals
AND/OR Goal tree
Goal refinement
Refined GMoDS
Model plan
Agent plan model
Model protocol
Protocol model
Design
Requirements
Agent class model
Figure 3: A basic O-MaSE Process.
3 Event-B method
Event-B [2] is a formal method for modelling concurrent
systems by adopting a top-down development process. The
Event-B method is influenced by the B Method [1] by using
typed set theory as the mathematical language for defining
state structures and events. However there is a conceptual
difference between these two formal methods: while the B
Method is aimed at software development, the Event-B is
aimed at system development.
In order to support construction and verification of
Event-B models, RODIN, an open toolset implemented on
the top of the Eclipse platform, was constructed. The
RODIN tool was initially developed as part of the European
Union ICT Project RODIN (2004 to 2007) [25], and then
continued by the EU ICT research projects DEPLOY (2008
to 2012) [14] and ADVANCE (2011 to 2014) [3]. The tool
is implemented in Java and it uses several plug-ins that ex-
tend the basic functionality of the Event-B framework.
Event-B models are described in terms of two basic com-
ponents: contexts, which contain the static part of a model,
and machines, which contain the dynamic part. Contexts
may contain carrier sets, constants, axioms, and theorems,
where carrier sets are similar to types, while machines,
which provide behavioral properties of Event-B models,
may contain variables, invariants, theorems, and events.
The state of a machine is described by its variables, which
are constrained by invariants.
Each machine may contains a set of events, which de-
scribe possible state changes. Each event is a specialized B
operation, and it is composed of a guard G(t, v) and an ac-
tion A(t, v), where t represents parameters the event may
contain, and v a subset of the variables of the machine. A
32 Informatica 40 (2016) 29–42 M. Brezovan et al.
Agent Control Algorithm
events
Reasoning Algorithm
Goal Reasoning
Role A
Role X
Capability A
Capability Y
eventsassignments
Control Component
Execution Component
Figure 4: Organization-based agent architecture.
special event, initialisation, is used for describing the initial
state of the machine. A machine can see multiple contexts.
During the development, a context can extend one or more
contexts by declaring additional carrier sets, constants, ax-
ioms or theorems.
The refinement is the only operation that can be applied
to a machine. If a machine N refines another machine
M , then M is called the abstract machine, while N is a
concrete machine. Event-B uses two principal types of re-
finement: superposition refinement [6] and data-refinement
[7]. Superposition refinement corresponds to a spatial and
temporal extension of a model, while data refinement is
used in order to modify the state of the machine.
The Event-B language does not allow a modular devel-
opment of a system. In order to manage this development
method some plug-ins have been added to the RODIN plat-
form. In the following we shortly present the Modular-
isation plug-ins that we use for constructing our proposal.
The Modularisation plug-in allows a modular development
of a specification by defining modules [20], a new type of
Event-B components containing groups of callable opera-
tions. A module description consists of two parts, module
interface and module body. A module interface is a sep-
arate Event-B component that consists of a set of external
module variables (v), constants (c), and sets (s), the exter-
nal module invariant, and a description of module opera-
tions, specified by their pre- and post-conditions. In ad-
dition, an interface can see its context. Denoting by M a
module, by MI its interface, and by MI_ctx the context of
MI , the interface MI has a structure as follows:
INTERFACE MI
SEES M_ctx
VARIABLES v
INVARIANT M_Inv(c, s, v)
INTIALISATION M_Init(v)
OPERATIONS
oper1 =̂
ANY par1
PRE M_Pre1 (c, s, par1, v)
RETURN res1
POST M_Post1 (c, s, par1, v, v′, res′1)
END
. . .
END,
where the primed variables of the interface and the vari-
ables representing the result of the operation, specified in
the predicates representing the postcondition of the opera-
tion, stand for the variable values after operation execution.
A module body is an Event-B machine, where the op-
erations specified in its interface are implemented. Each
operation is implemented by a group of events, one group
for each operation. Some events from a group play a spe-
cial role of operation termination events and are called final
events. A final event returns the control to a caller.
An operation defined into a module M can be invoked
into a Event-B machine, which can be another module,
only if the module M is imported into this machine. The
inclusion of a module into a Event-B machine is specified
by a clause USES in the importing machine. This clause
specify the interface of the imported module, and a prefix
that is used to emulate a dedicated namespace for the im-
ported module. All the names of the imported module are
modified by adding this prefix.
The syntax for an operation invocation is similar to a
function call. The semantics of an operation invocation is
also similar to the standard semantics of a function call as
in the most programming languages. Because an operation
invocation is atomic, the events from the group correspond-
ing to the operation in the module body run until termina-
tion without interference from other groups.
4 Writing object-oriented
specifications in event-B
Because B and Event-B methods are not object-oriented,
there are several proposals in the last years to bring object-
oriented concepts into these methods. First of all, both B
and Event-B have only static structuring mechanisms: they
allow to define abstract machines with a static architectural
structure that do not change at run-time [15]. In [4] an ex-
tension of the syntax of B is proposed for supporting the
management of dynamic populations of components. In
this proposal a population manager is associated to a ma-
chine for managing its instances. Although this extension is
not object-oriented, the population manager for a machine
M is a machine which represents a dynamic set of M in-
stances, including operations for the creation and deletion
of machine instances.
Expressing GMoDS Models into. . . Informatica 40 (2016) 29–42 33
A similar mechanism is used also in the UML-B method:
for each machine representing a class hierarchy, an implicit
context is generated, which defines the set of all instances,
A_SET , for each class A from the class hierarchy. As
opposed to the B method, where an abstract machine can
represent a class, and a hierarchy of classes is constructed
by several machines that use the clause USES to include
other the classes from the hierarchy, the Event-B method
does not have USES and INCLUDE clauses, thus a hier-
archy of classes must be defined in a single machine. An-
other weakness of the UML-B method is the absence of
the method calls of the class instances, because an Event-
B machine has only events (or transitions in UML-B), not
operations as in the case of the B abstract machines.
The aim of this Section is to bring some object-oriented
concepts into Event-B modelling, without changing the
syntax of Event-B, and thus allowing the Event-B speci-
fications to be realized and verified with the Rodin tool.
We do not use the UML-B method because of the weak-
ness above mentioned, related to the absence of the method
calls. In fact, we use the modularization approach [20] in
order to allow this action, while preserving some object-
oriented elements from the UML-B, such as management
of class instances, attributes, associations, and inheritance.
We use interfaces for describing class hierarchies and the
methods (operations) of the classes, and modules for im-
plementing the class methods. For a hierarchy H contain-
ing the classes, A1, . . . , Ak, the following Event-B compo-
nents are defined:
– A context, H_Ctx , which contain: the set INST of all
instances of all class from the H hierarchy, the con-
stant Void representing the null instance, and the set
of all instances of the classes A1_Inst , . . . ,Ak_Inst
respectively, with the property that:
INST =
⋃k
i=1 Ai_Inst ∪ {Void},
Ai_Inst ∩Aj_Inst ,∀i 6= j.
– An interface, H_Intf , having:
– as variables, the sets Ai ∈ P(Ai_Inst) repre-
senting the set of active objects of the class Ai,
i = 1, . . . , k, and relations and functions repre-
senting attributes of these classes and the associ-
ations between some classes,
– as operations, the constructor and the destructor
for each class, and other operations representing
the methods of the classes Ai, i = 1, . . . , k
– A module, H_Impl , where the operations defined in
H_Intf are implemented.
As an example, we consider two classes, Node and List ,
where each list is an ordered sequence of nodes, and each
node has as attribute with an integer value. The context
related to classes Node and List is defined as follows:
CONTEXT H_Ctx
SETS INST
CONSTANTS Void , Node_Inst , List_Inst
AXIOMS
Void ∈ INST
Node_Inst ⊆ INST
List_Inst ⊆ INST
partition(INST , {Void}, Node_Inst , List_Inst)
END
From the interface H_Intf , the variables, their invariants
and initializations are defined as follows:
INTERFACE H_Intf
SEES H_Ctx
VARIABLES Node, value, List , first, next
INVARIANTS
Node ∈ P(Node_Inst ∪ {Void})
value ∈ Node_Inst → N
List ∈ P(List_Inst ∪ {Void})
first ∈ List_Inst →Node_Inst ∪ {Void}
next ∈ List_Inst → (Node_Inst → (Node_Inst ∪ {Void}))
INTIALISATION
Node := ∅, value := ∅
List := ∅, first := ∅, next := ∅
OPERATIONS
. . .
From the operations related to the Node class we present
only the constructor newNode , and the function getValue:
newNode =̂
ANY self , v
PRE
self ∈ Node_Inst \Node
v ∈ N
RETURN ret
POST
Node ′ = Node ∪ {self }
value′ = value ∪ {self 7→ v}
ret′ = self
END
getValue =̂
ANY self
PRE self ∈ Node
RETURN ret
POST ret′ = value(self )
END
From the operations related to the List class we present
only the the destructor deleteList and the operation
34 Informatica 40 (2016) 29–42 M. Brezovan et al.
insertFront :
deleteList =̂
ANY self
PRE self ∈ List
RETURN ret
POST
first′ = (dom(first) \ {self }) 
 first
next′(self ) = ∅
List ′ = List ∪ {self }
∀a, b · a ∈ Node_Inst ∧ a ∈ Node_Inst ∧
a 7→ b ∈ next(self ) ⇒ a /∈ Node ′
ret′ = Void
END
insertFront =̂
ANY self , n, v
PRE
self ∈ List
n ∈ Node_Inst \Node
v ∈ N
RETURN ret
POST
value′(n) = v
next′(self ) = next(self ) ∪ {n 7→ first(self )}
first′(self ) = n
ret′ = first′(self )
END
In the implementation module, H_Impl , each operation
is implemented by a group containing one or more events.
Other defined operations can be called in the action part of
these events. For example, in the implementation of op-
eration insertFront , the constructor newNode of the class
Node is called:
insertFront =̂
ANY self , n, v
WHERE
self ∈ List
n ∈ Node_Inst \Node
v ∈ N
THEN
n := newNode(v)
next(self ) := next(self ) ∪ {n 7→ first(self )}
first(self ) := n
insertFront_ret := n
END
From all operations of the class List, only the op-
eration deleteList has a group containing two events:
deleteListNonEmpty , that occurs for each node in a non-
empty list, and deleteListEmpty that occurs when the list
is empty.
In order to describe the modeling of the inheritance and
polymorphism concepts in Event-B, we use an example of
a class hierarchy with three classes, B, D1 and D2, as in
Fig. 5, where D1 and D2 inherit the class B. In addition,
all three classes have the same operation, op.
Denoting with INST the set of all instances of the
classes form the above hierarchy, with B_Inst , B_Inst ,
D1_Inst , and D2_Inst the set of all possible instances of
the classes B, D1, and D2 respectively, the fact that D1
and D2 inherit the class B can be described as follows:
op
B
D1 D2
op
op
Figure 5: A class hierarchy with one class root.
CONTEXT Ctx
SETS INST
CONSTANTS Void , B_Inst , D1_Inst , D2_Inst
AXIOMS
Void ∈ INST
partition(INST , {Void}, B_Inst , D1_Inst , D2_Inst)
partition(B_Inst ,D1_Inst , D2_Inst)
END
The polymorphism, related to the operation op in this
case, is modeled in the interface, I , which has only one
operation, denoted by op in this case, and in its associated
module,M , which contains a group with two different final
events, denoted by op1 and op2 in this case, one event for
each each operation from a inherited class.
INTERFACE I
SEES Ctx
VARIABLES B, D1, D2
INVARIANTS
B ∈ P(B_Inst ∪ {Void})
D1 ∈ P(D1_Inst ∪ {Void})
D2 ∈ P(D2_Inst ∪ {Void})
INTIALISATION
B := ∅, D1 := ∅, D2 := ∅
OPERATIONS
op =̂
ANY self
PRE self ∈ B_Inst \B
RETURN ret
POST
B′ = B ∪ {self }
self ∈ D1_Inst \D1 ⇒ D1′ = D1 ∪ {self }
self ∈ D2_Inst \D2 ⇒ D2′ = D2 ∪ {self }
ret′ = self
END
The module M can be described as follows:
Expressing GMoDS Models into. . . Informatica 40 (2016) 29–42 35
MACHINE M
IMPLEMENTS I
SEES Ctx
. . .
GROUP op BEGIN
FINAL op1 =̂
ANY self
WHERE
self ∈ D1_Inst \D1
THEN
D1 := D1 ∪ {self }
op1_ret := self
END
FINAL op2 =̂
ANY self
WHERE
self ∈ D2_Inst \D2
THEN
D2 := D2 ∪ {self }
op2_ret := self
END
END
END
5 Expressing GMoDS models in
object-oriented specifications in
event-B
As stated in Section 2, we describe a specification of the
GMoDS framework using an object-oriented extension of
the Event-B method, which represents the Goal Reasoning
module from the Control Component of an Organization-
based agent architecture.
The GMoDS definition contains three different models
[13]: (i) a Specification model that contains a tree structure
of goal classes and their associations, and (ii) a Runtime
model that contains a tree structure of goal instances and
the actions that are executed, each action being related to
a association between classes, and (iii) an Execution model
that implements GMoDS using and updating continuously
a collection of sets of goal instances, according to the cur-
rent state of each goal instance.
5.1 GMoDS Models
The Specification model of GMoDS contains the goal spec-
ification tree, GSpec, which describes how the goal classes
are related to one another, and where upper level goals
(parents) are decomposed into lower level sub-goals (chil-
dren) and each parent has either a conjunctive or disjunctive
achievement condition as shown via the 〈〈and〉〉 and 〈〈or〉〉
decoration in Fig. 2. Goals without children are known as
leaf goals.
In addition to goals, the specification model uses an-
other concepts, such as, relations, events, and parame-
ters. The main relation type used by this model is the
goal precedence, specified by the precedes relationship,
that ensures that no agents work on a specific goal until all
goals that precede that goal have been achieved. In Fig.
2 there are two precedes relations: precedes(g2, g3), and
precedes(g6, g7). Events in GMoDS are represented by
triggers:
– a positive trigger, or simply trigger, which allows a
new goal instance of a certain class gj to be created
when and event ek occurs during the pursuit of a goal
instance of a class gi, eventually by passing some pa-
rameter values p. In Fig. 2 there are two triggers:
trigger(g1, e1, x) = {g5}, and trigger(g7, e2, y) =
{g8}.
– a negative trigger, or ¬trigger, which allows an ac-
tive goal instance of a certain class gi to eliminate an-
other active goal instance of a certain class gj from the
set of active goal instances when an event ek occurs.
There is always an initial trigger, usually denoted by e0,
that is used when the system starts, which creates an in-
stance of the root goal (and, recursively, it can create others
goal instances).
The Runtime model is represented by a dynamic tree of
goal instances, GInst that retains the structure of GSpec
while allowing dynamism by way of triggering and prece-
dence. For each goal instance from GInst, four predicates
are dynamically set:
– achieved, which determines whether a goal has been
achieved by the system. For leaf goals achieved be-
comes true when the agent pursing the goal notifies
the system of its achievement, while for parent goals,
the value of the achieved is based on the achievement
condition (conjunction or disjunction) and the state of
its children.
– obviated, which states whether a goal is no longer
needed by the system. A goal becomes obviated if it
is a child of a disjunctive goal that has been achieved
that does not precede any other system goal.
– preceded, which becomes true if a goal preceding it
has not been achieved, or if a new goal may still be
instantiated that may precede it.
– failed, which becomes true if the system has deemed
that the goal can never be achieved by the system.
For example, after the initial trigger, the instance tree,
GInst, has a structure as presented in Fig. 6. Instances of
the goals g5 (and subsequently g6 and g7) and g8 are not
created because they will be created (triggered) by g4 and
g7 when the events e1 and e2 respectively will occur.
g4(e0)
g0(e0)
g1(e0)
g2(e0) g3(e0)
Figure 6: The tree GInst associated to the tree GSpec from
Fig. 2 after the initial trigger.
36 Informatica 40 (2016) 29–42 M. Brezovan et al.
In the Runtime model there are maintained and up-
dated six sets, GI−Triggered, GI−Active, GI−Achieved,
GI−Removed,GI−Failed andGI−Obviated as shown in Fig.
7.
GI−Removed
GI−Triggered GI−Active
GI−Obviated
GI−Failed
GI−Achieved
Figure 7: Goal execution model.
Each set contains current instance goals having the same
state:
– triggered, for all instances created by a trigger event,
or, recursively, by a parent goal,
– active, for all triggered instances that are not pre-
ceded,
– obviated, that is based on the obviated predicate,
– achieved, that is based on the achieved predicate,
– failed, that is based on the failed predicate,
– removed, for all goal instances destroyed by a nega-
tive trigger.
When the state of a goal instance is one of the last three
state, this goals remains in this state until the system stops.
5.2 Expressing GMoDS Models into an
Object-Oriented Model
For specifying in Event-B the GMoDS framework (in fact
the Goal Reasoning module), all the three GMoDS mod-
els must be specified. I3n the case of the Specification
model, the goal tree GSpec is defined by using goal classes
as nodes. All classes from a goal tree will form a hierarchy
having an abstract class, denoted byGoal as the root of this
hierarchy. For the goal tree from the Fig. 2, the goal class
hierarchy is presented in Fig. 8, where the classes g0, g1,
. . ., g8 inherit the class Goal.
g8
Goal
g0 g1 g2 g3 g4 g5 g6 g7
Figure 8: Goal class hierarchy.
The main two attributes of the class Goal are
goal_state ∈ Goal_STATES and goal_type ∈
Gol_TY PE, where:
Goal_STATES = {triggered, active, achieved,
failed, obviated, removed},
Goal_TYPE = {AND ,OR,LEAF}.
In order to allow the specification of:
– the trigger events from the specification model,
– the predicates from the runtime model,
– the sets of goal instances, from the implementation
model,
the following associations between goal classes are used:
– down and right, which allows to specify the goal tree
from GSpec,
– creates, created and destroy, which allow to specify
the positive and negative triggers,
– precedes and preceded, which allow to specify the
precedence relation between goals,
– up, which allows to retrieve the parent of a goal.
These associations are presented in Fig. 9.
right
destroy up
down
g
gu
gd
gp
precedes
preceded
ge
gr
gccreates
created
Figure 9: Goal class associations.
For the specification the GMoDS runtime model, a tree
of goal instances must be specified. Because the type of
goal instances does not need to be specified, nor the associ-
ations precedes, creates and destroy, in this case only
the tree structure of the instances is specified. Unfortu-
nately the associations up, down, and right from GSpec
can not be used, because the tree structure of goal instances,
GInstances is not always identical with the tree structure
of GSpec: a positive trigger event can create multiple in-
stances of the same goal that are "sibling" nodes (having
the same parent). For solving this problem we use different
associations related to the sets of goal instances: upInst,
downInst, and rightInst. The class used to specify the
runtime model is Tree , a tree of goal instances, which is
related to the set G_Instance from the runtime model.
There is no need to implement the six sets of goal in-
stances from the implementation model, as presented in
Fig. 7, because the current state of each goal instance spec-
ifies exactly the set to that instance belongs to.
For translating the GMoDS framework into an object-
oriented model, we use the following classes:
Expressing GMoDS Models into. . . Informatica 40 (2016) 29–42 37
– The class G_Spec, which is the main class of the trans-
lated model, because it contains both the static tree
of goal classes, and the dynamic tree of the goal in-
stances.
– The class GName , whose elements represent the
nodes of the static static tree of goal classes.
– The class Tree , which represents the dynamic tree of
the goal instances.
– The class Goal , whose elements represent the nodes
of the dynamic tree of the goal instances.
– The class Env , that implements the rest of the
Organization-based agent architecture: the Reasoning
algorithm, and the Execution component.
In fact, GName is not really a class, because it does
not have constructors and destructors (the tree of the goal
classes from G_Spec is static). We use instead the notion of
Records for GName , an extension of the Event-B method.
The main components of GName are the following:
– state , which represents the current state of the corre-
sponding goal class, from the set Goal_STATES .
– curr_inst , which represents the set of active goal in-
stances of the corresponding goal class.
– up, down, right, precedes, and preceded that repre-
sent the relations between goal classes, as presented
in Fig. 9.
The class Goal represents the goal class hierarchy, as
presented in Fig. 8. It contains only the attributes upInst,
downInst, and rightInst, representing the relations be-
tween goal instances in a dynamic tree structure. the only
operations allowed by Goal are the constructor newGoal
and the destructor delGoal.
The singleton class Tree contains only one attribute,
rootInst , which represents the root of the dynamic tree of
goal instances. Tree is a singleton class because there is a
single object of Tree , which is an attribute of G_Spec. In
addition, Tree has three operations:
– deleteInst , which deletes all the sub-tree having as
parameter its root.
– addChildInst , which adds a new created instance as
the first child of the parent specified as parameter.
– addBrotherInst, which adds a new created instance
as the right of the goal instance specified as parameter.
The elements of Tree are instances of the class Goal.
There is only one instance of the class Tree, which is a
member of the class G_Spec.
The singleton class G_Spec contains only two attributes:
– rootG , an element of the GName set, representing
the root of the static tree of goal classes (e.g. g0 in our
example).
– tr, the unique instance of the class Tree , representing
the dynamic tree of goal instances.
In addition, G_Spec has several operations, according to
the relations between the classes G_Spec and Env , as pre-
sented in Fig. 10:
– start , representing the event that starts the execution
(or simulation) process of the MAO, and thus the Goal
reasoning algorithm.
– achivedInstGoal , which informs G_Spec that a goal
instance have been achieved.
– createInstGoal , which informs G_Spec that an in-
stance of a goal class must be created.
– deleteInstGoal , which informs G_Spec that a goal in-
stance must be deleted.
– failedInstGoal , which informs G_Spec that an active
goal has failed.
– createdInstGoal , which informs Env that a goal in-
stance has been created.
– deletedInstGoal , which informs Env that a goal in-
stance has been deleted.
The unique instance of the class G_Spec, gsp, represents
the Goal reasoning module, a part of the Control compo-
nent, from the Organization-based agent architecture.
Env represents the environment for the GMoDS frame-
work that:
– Contains the Reasoning algorithm from the
Organization-based agent architecture that per-
forms the reorganisation structure of a MAO, based
of information received from the Goal reasoning
algorithm (e.g. from the GMoDS framework).
– Contains the Execution components from the
Organization-based agent architecture, which con-
tains the agents that achieve the roles related to the
instances of the leaf goals in the goal tree, and send
messages to those instances, when a goal has been
achieved, or when it failed,
– Can send a message to the GMoDS system to start its
execution (i.e. it sends the initial trigger to the parent
goal of the goal hierarchy).
The relations between the classes Env and the G_Spec are
presented in Fig. 10, where:
– The relation start exists between Env and the root of
the goal hierarchy (e.g. g0 in our example),
– The relations achieved and failed exist between
Env and the leaves of the goal hierarchy (e.g. g2,
g3, g4, g6, and g7 in our example),
– The relation create exists between Env and some
nodes from the goal hierarchy having a positive trig-
ger (e.g. g5 and g8 in our example),
– The relation delete exists between Env and some
nodes from the goal hierarchy having a negative trig-
ger.
– Relations created and deleted exist between the goal
classes from G_Spec and the Env, indicating to the
Reasoning algorithm that some goal instances have
been created, or deleted.
All these relation represent in fact operations of the class
Env. Excepting the operations start, achieved, failed,
create and delete, the rest of the classEnv is not specified
in this paper. This will be the subject of a future research.
38 Informatica 40 (2016) 29–42 M. Brezovan et al.
G_Spec
failedcreateachieved delete start created deleted
Environment
Figure 10: Environment and Goal classes associations.
5.3 An Example of Expressing GMoDS
Models in Event-B
Using the patterns specified in Subsection 5.2 we can ex-
press the GMoDS system from Fig. 2 into an object-
oriented model in Event-B. In fact, the model specified in
Event-B encapsulates the GMoDS framework representing
the Goal reasoning module into an object, gsp, instance of
the class G_Spec, while the rest of the Organization-based
agent architecture is represented by the object env, instance
of the class Env.
The context of the modeled system will contain the sets
and the constants that follows the object-oriented patterns
specified in Subsection 5.2.
CONTEXT OBAA_Ctx
SETS
INST , GName, Goal_STATES , Goal_TYPE
CONSTANTS
Void , Goal_Inst ,G_Spec_Inst , Tree_Inst , Env_Inst
g0_Inst , g1_Inst , g2_Inst , . . . , g8_Inst
gsp, tr, env
g0, g1, g2, . . . , g8
triggered, active, achieved, failed, obviated,
removed, inactive
AND , OR, LEAF , NONE
AXIOMS
Void ∈ INST
partition(INST , {Void},Goal_Inst ,Tree_Inst ,
Env_Inst,G_Spec_Inst)
partition(Goal_Inst , g0_Inst , . . . , g8_Inst)
partition(G_Spec_Inst , {gsp})
partition(Tree_Inst , {tr})
partition(Env_Inst , {env})
partition(GName, {g0}, {g1}, . . . , {g8})
partition(Goal_TYPE , {AND}, {OR}, {LEAF})
partition(Goal_STATES , {triggered}, {active},
{achieved}, {failed}, {obviated}, {removed})
END
In the interface OBAA_Intf , the variables and their in-
variants allow to specify the main object-oriented concepts,
as defined in the Subsection 5.2:
INTERFACE OBAA_Intf
SEES OBAA_Ctx
VARIABLES
Env , G_Spec, Tree, Goal
type, state, curr_inst
creates, destroy, up, down, right, precedes, preceded
rootG, rootInst, treeInst
lastInst, lastGoalChild
goalName
INVARIANTS
Env ∈ P(Env_Inst ∪ {Void})
G_Spec ∈ P(G_Spec_Inst ∪ {Void})
Tree ∈ P(Tree_Inst ∪ {Void})
Goal ∈ P(Goal_Inst ∪ {Void})
rootG ∈ G_Spec→GName ∪ {Void}
treeInst ∈ G_Spec→ Tree ∪ {Void}
rootInst ∈ Tree→Goal_Inst ∪ {Void}
lastInst ∈ GName→Goal_Inst ∪ {Void}
goalName ∈ Goal_Inst →GName
type ∈ GName→Goal_TYPE
state ∈ Goal_Inst →Goal_STATES
curr_inst ∈ GName→ P(Goal_Inst ∪ {Void})
available_inst ∈ GName→ P(Goal_Inst ∪ {Void})
up, down, right ∈ GName→GName ∪ {Void}
creates, created ∈ GName→GName ∪ {Void}
precedes, preceded ∈ GName→GName ∪ {Void}
upInst, downInst, rightInst ∈ Goal_Inst → Goal_Inst
∪ {Void}
INTIALISATION
. . .
The initialization event means in fact the creation of the
static tree structure ofGSpec, as defined in Fig. 2, and some
other initializations, such as (a) initialization of singleton
classes, (b) defining the goal types, (c) managing the goal
instances, (d) specifying the hierarchical structure of the
goal tree, (e) specifying the positive and negative triggers,
and (f) specifying the precedence relations between goals:
Env := {env}, G_Spec := {gsp}, Tree := {tr}
rootG(gsp) := g0, treeInst(gsp) := tr
rootInst(tr) := Void
. . .
type(g0) := AND , type(g1) := OR
. . .
curr_inst(g0) := ∅, curr_inst(g1) := ∅,
. . .
available_inst(g0) := g0_Inst , available_inst(g0) := g0_Inst ,
. . .
lastInst(g0) := Void , lastInst(g1) := Void ,
. . .
up(g0) := Void , up(g1) := g0,
. . .
down(g0) := q1, down(g1) := g2, down(g5) := g6,
. . .
right(g1) := g5, right(g5) := g8,
. . .
creates(g4) := g5, created(g5) := g5,
. . .
precedes(g2) := g3, preceded(g3) := g3,
In the following we present only the operations related
to the operation create of the environment. The other op-
erations are similar. 1
1The entire Event-B model is available at http://software.
ucv.ro/~mbrezovan/fm/gmods_model.zip
Expressing GMoDS Models into. . . Informatica 40 (2016) 29–42 39
Because some of the operations, such as
createGoalInstance, of the class G_Spec creates
recursively all the nodes that from a sub-tree having a root
a goal instance, for correctly specifying the post-condition
of this operation we need to define the transitive closure
of the relation down. The same operation is needed for
createGoalInstance, when the transitive closure of
the relation up is needed. Unfortunately, the Event-B
language has a strict mathematical language, which is
based on a set-theoretic model and corresponding proofs
for modeling and refinement consistencies, and on the
First Order Predicate Calculus for decomposition. For
extending this mathematical language, the Theory plug-in
was implemented, which is a Rodin extension that provides
the facility to define mathematical extensions as well as
prover extensions. There three kinds of extension, one of
them is related to extensions of set-theoretic expressions or
predicates. One example extensions of this kind consist of
adding the transitive closure of relations or various ordered
relations.
Butler [9] proposes propose a special case of an oper-
ator defined as the solution of some predicate, namely a
fixed-point definition. For example, transitive closure of a
relation R may be defined as follows [9]:
operator tcl
prefix
args r
type parameters T
condition down ∈ T ↔ T
fixpoint y where
r ∪ r ; y
order{a 7→ b | a ∈ T ↔↔∧ a ⊆ b}
end
We can define the transitive closure of the relation down
(as well as for the relation up) following the above exam-
ple:
operator tcl
prefix
args down
type parameters GName
condition r ∈ GName↔GName
fixpoint y where
down ∪ down ; y
order{a 7→ b | a ∈ GName↔GName ∧ a ⊆ b}
end
The transitive closure of the relation down allow us to
determine all the pairs (g1 7→ g2) such that up(g1) = g2.
The operation newGoal of the class Goal class can be
defined as follows:
newGoal =̂
ANY self , g
PRE
self ∈ Goal_Inst
g ∈ Goal_Inst \Goal
RETURN ret
POST
Goal ′ = Goal ∪ {g}
ret′ = g
END
For allowing the polymorphism in this case, in the im-
plementation module there will be eight final events related
to the group newGoal: newGoal_g1 , newGoal_g2 , . . .,
newGoal_g8 .
The operation addGoalInst of the class Tree will add
a single goal instance to the tree.
addGoalInst =̂
ANY self , ge, gi
PRE
self ∈ Tree_Inst
ge, gi ∈ Goal_inst
RETURN ret
POST
ge = Void ⇒ rootInst′(self) = gi
ge 6= Void ∧ downInst(ge) = Void ⇒ downInst′(ge) = gi
ge 6= Void ∧ downInst(ge) 6= Void ⇒ lastInst′(ge) = gi
ret′ = self
END
In the implementation module there are three events in
the group addGoalInst: addRootInst, addChildInst
and addBrotherInst, corresponding to the three above
cases.
The main operations of create and destroy a goal in-
stance of the interface OBAA_Intf are related to the class
G_Spec, which contains the tree of goal instances as at-
tribute. The creation of an instance of a parent goals recur-
sively creates children to the corresponding subtree that are
non-triggered subgoals.
The operation createGoalInstance of the G_Spec class
can be defined as follows:
createGoalInstance =̂
ANY self , gc, gi
PRE
self ∈ G_Spec
gi ∈ available_inst(gc) \ curr_inst(gc)
gc ∈ GName
created(gc) 6= Void
RETURN ret
POST
curr_inst ′(gc) = curr_inst(gc) ∪ {gi}
preceded(gc) = Void ⇒ state′(gi) = active
preceded(gc) 6= Void ⇒ state′(gi) = triggered
. . .
The following two predicates specify the recursive cre-
ation of the sub-tree having gi as root for non-preceded
goals:
∀gc 7→ g ∈ tcl(down) ∧ created(g) 6= Void ∧
∃i ∈ available_inst(g) \ curr_inst(g)∧
preceded(g) = Void ∧ down(up(g)) = g
⇒ curr_inst ′(g) = curr_inst(g) ∪ {i}∧
state′(i) = active∧
downInst′(lastInst(up(g))) = i
∀gc 7→ g ∈ tcl(down) ∧ created(g) 6= Void ∧
∃i ∈ available_inst(g) \ curr_inst(g)∧
preceded(g) = Void ∧ down(up(g)) 6= g ∧
∃gl ∈ GName ∧ right(gl) = g
⇒ curr_inst ′(g) = curr_inst(g) ∪ {i}∧
state′(i) = active∧
downInst′(lastInst(right(gl))) = i
40 Informatica 40 (2016) 29–42 M. Brezovan et al.
The case for preceded goals is similar to the non-
preceded case. The last predicates specify the linking of
the sub-tree root, gi, in the tree treeInst of G_Spec:
rootInst(tr) = Void ⇒ rootInst′(tr) = gi
rootInst(tr) 6= Void ∧ down(up(gc)) = gc∧
card(curr_inst(gc)) = 1 ⇒ down(lastInst(up(gc))) = gi
rootInst(tr) 6= Void ∧ down(up(gc)) = gc∧
card(curr_inst(gc)) > 1 ⇒ right(lastInst(gc) = gi
rootInst(tr) 6= Void ∧ down(up(gc)) 6= gc∧
∃gl ∈ GName ∧ right(gl) = gc∧
card(curr_inst(gc)) = 1 ⇒ right(lastInst(gl))) = gi
rootInst(tr) 6= Void ∧ down(up(gc)) 6= gc∧
∃gl ∈ GName ∧ right(lastInst(gl)) = gc∧
card(curr_inst(gc)) > 1 ⇒ right(lastInst(gc)) = gi
ret′ = gi
END
When implementing this operation in the im-
plementation module, OBAA_Impl , the function
createGoalInstance can be recursively applied, be-
cause the two associations, down and right can be viewed
as the two links, left and right of a binary tree. There
are four events in the group createGoalInstance in the
implementation module, two related to the leaf nodes, and
two related to the non-leaf nodes:
– createGoalInstanceLeafNotPrededed,
– createGoalInstanceLeafPrededed,
– createGoalInstanceNotPreceded,
– createGoalInstancePreceded.
From the implementation module, OBAA_Impl , we
present only a single event for each described above op-
eration.
For the operation newGoal of the class hierarchy Goa
we present the event newGoal_g1 :
newGoal_g1 =̂
ANY self , g
WHERE
self ∈ G_Spec
g ∈ g0_Inst \ curr_inst(g0)
THEN
curr_inst(g0) := curr_inst(g0) ∪ {g}
newGoal_g1_ret := g
END
For the operation addGoalInst of the class Tree we
present the event addChildInst:
addChildInst =̂
ANY self , ge, gi
WHERE
self ∈ Tree_Inst
ge, gi ∈ Goal_inst
ge 6= Void
THEN
downInst(ge) = gi
addChildInst_ret := gi
END
When implementing the operation addGoalInstance of
the class G_Spec in the implementation module, the func-
tion createGoalInstance can be recursively applied, be-
cause the two associations, down and right can be viewed
as the two links, left and right of a binary tree. We present
the event acreateGoalInstanceNotPreceded.
createGoalInstanceNotPreceded =̂
ANY self , gn, gi
WHERE
self ∈ G_Spec
gn ∈ GName
gi ∈ available_inst(gn)
created(gn) = Void
down(gn) 6= Void
right(gn) 6= Void
preceded(gn) = Void
THEN
curr_inst(gn) = gi
state(gi) := active
addChild(treeInst(self ), gi,
createGoalInstance(down(gn)))
addBrother(treeInst(self ), gi,
createGoalInstance(right(gn)))
createGoalInstanceNotPreceded_ret := gi
END
Finally, the environment class, Env, has five operations
that simply call the operations of the class G_Spec: start,
create, delete, achieved, and failed. We present the op-
eration create:
start =̂
ANY self
WHERE
self ∈ Env
THEN
createGoalInstance(gsp, g0)
start_ret := Void
END
We uses the Pro-B plug-in [23] for the Rodin platform
[25] to verify the consistency of the modeled system. ProB
is an animator and model checker for Event-B. It allows
animation of Event-B specifications, and it can be used for
model-checking, and for evaluating a variety of provers or
tactics on a selection of proof obligations.
6 Conclusions
In this paper we presented an initial research related to
express Organisation-based multi-agent software engineer-
ing (O-MaSE) to an object-oriented model in Event-B.
We started to study the Goal Model for Dynamic Systems
(GMoDS), a methodology that defines the operational se-
mantics of a dynamically changing model of system goals,
which has been used as the requirements modeling for the
O-MaSE methodology.
Because the object-oriented model translated from the
GMoDS models use some object-oriented concepts, such
as inheritance, and calling of class methods, we used the
modularisation plug-in of Rodin for implementing these
concepts. We presented some pattern to translate GMoDS
models to an object-oriented specification in Event-B, and
we have illustrated these patterns for implementing an ex-
ample from [13].
Expressing GMoDS Models into. . . Informatica 40 (2016) 29–42 41
We planned to accomplish this work by testing the pro-
posed patterns on real multi-agent systems, and to extend
the research to the O-MaSE framework.
References
[1] Jean-Raymond Abrial. The B-Book: Assigning Pro-
grams to Meanings. Cambridge University Press,
1996.
[2] Jean-Raymond Abrial. Modeling in Event-B. Sys-
tem and Software Engineering. Cambridge University
Press, 2010.
[3] ADVANCE. http://www.advance-ict.eu/.
[4] Nazareno Aguirre, Juan Bicarregui, Theo Dimitrakos,
and Tom Maibaum. Towards Dynamic Population
Management of Abstract Machines in the B Method.
In ZB 2003: Formal Specification and Development
in Z and B, volume 2651 of Lecture Notes in Com-
puter Science, pages 528–545. Springer-Verlag, 2003.
[5] Michael Wooldridge ans Nicholas R. Jennings and
David Kinny. The Gaia Methodology for Agent-
Oriented Analysis and Design. Autonomous Agents
and Multi-Agent Systems, 3(3):285–312, 2000.
[6] R.-J. Back and J. von Wright. Refinement Calculus,
Part I: Sequential Nondeterministic Programs. In J.W.
deBakker, W.-P. deRoever, and G. Rozenberg, editors,
Stepwise Refinement of Distributed Systems, volume
430 of Lecture Notes in Computer Science, pages 42–
66. Springer, 1990.
[7] Ralph-Johan Back. Refinement Calculus, Part II:
Parallel and Reactive Programs. In J.W. deBakker,
W.-P. deRoever, and G. Rozenberg, editors, Step-
wise Refinement of Distributed Systems, volume 430
of Lecture Notes in Computer Science, pages 67–93.
Springer, 1990.
[8] Amelia Badica and Costin Badica. FSP and
FLTL framework for specification and verification
of middle-agents. International Journal of Applied
Mathematics and Computer Science, 21(1):9—25,
2011.
[9] Michael Butler and Issam Maamria. Mathemati-
cal Extension in Event-B Through the Rodin Theory
Component. Technical Report 251, Electronics and
Computer Science, University of Southampton, 2010.
[10] S.A. DeLoach, W. Oyenan, and E.T. Matson. A Ca-
pabilities Based Model for Artificial Organizations.
J. of Autonomous Agents and Multiagent Systems,
16(1):13—56, 2008.
[11] S.A. DeLoach, M.F. Wood, and C.H. Sparkman. Mul-
tiagent Systems Engineering. Intl. J. of Software En-
gineering and Knowledge Engineering, 11(3):231–
258, 2001.
[12] Scott A. DeLoach and Juan Carlos Garcia-Ojeda.
O-mase: A Customizable Approach to Designing
and Building Complex, Adaptive Multiagent Sys-
tems. Intl. J. of Agent-Oriented Software Engineer-
ing, 4(3):244–280, 2010.
[13] Scott A. DeLoach and Matthew Miller. A Goal Model
for Adaptive Complex Systems. Intl. J. of Computa-
tional Intelligence: Theory and Practice, 5(2), 2010.
[14] DEPLOY. http://www.deploy-project.
eu/.
[15] T. Dimitrakos, J. Bicarregui, B. Matthews, and
T. Maibaum. Compositional Structuring in the B-
Method: A Logical Viewpoint of the Static Context.
In ZB 2000: Formal Specification and Development
in Z and B, volume 1878 of Lecture Notes in Com-
puter Science, pages 107–126. Springer-Verlag, 2000.
[16] A. Estefania, J. Vicente, and B. Vicente. Multi-
Agent System Development Based on Organizations.
Electronic Notes in Theoretical Computer Science,
150(3):55—71, 2006.
[17] Neil Evans and Michael Butler. A Proposal for
Records in Event-B. In FM 2006: Formal Methods,
volume 4085 of Lecture Notes in Computer Science,
pages 221–235. Springer, 2006.
[18] J. Ferber, O. Gutknecht, and F. Michel. From Agents
to Organizations: An organizational View of Multi-
Agent Systems. In P. Giorgini, J.P. Müller, and J.J.
Odell, editors, Agent-Oriented Software Engineering,
volume 2935 of Lecture Notes in Computer Science,
pages 214—230. Springer, 2004.
[19] V. Hilaire, P. Gruer, A. Koukam, and O. Simonin.
Formal Specification Approach of Role Dynamics in
Agent Organisations: Application to the Satisfaction-
Altruism Model. Intl. J. of Software Engineering and
Knowledge Engineering, 16(3), 2007.
[20] A. Iliasov, E. Troubitsyna, L. Laibinis, A. Ro-
manovsky, K. Varpaaniemi, D. Ilic, and T. Latvala.
Supporting Reuse in Event-B Development: Modu-
larisation Approach. In Abstract State Machines, Al-
loy, B, and Z, volume 5977 of Lecture Notes in Com-
puter Science, pages 174–188. Springer, 2010.
[21] T. Juan, A. Pearce, and L. Sterling. ROADMAP:
Extending the Gaia Methodology for Complex Open
Systems. In Proc. 1st Intl. Joint Conf. on Autonomous
Agents And Multiagent Systems, pages 3–10, 2002.
42 Informatica 40 (2016) 29–42 M. Brezovan et al.
[22] J. Mylopoulos, J. Castro, and M. Kolp. Tropos: A
Framework for Requirements-Driven Software De-
velopment. In J. Brinkkemper and A. Solvberg, ed-
itors, Information Systems Engineering: State of the
Art and Research Themes, pages 261–273. Springer-
Verlag, 2000.
[23] ProB. http://www.stups.
uni-duesseldorf.de/ProB/index.php5/
ProB_for_Rodin.
[24] A. Regayeg, A. H. Kacem, and M. Jmaiel. Specifi-
cation and Verification of Multi-Agent Applications
Using Temporal Z. In Proc. Intl. Conf. on Intelligent
Agent Technology, pages 260—266, 2004.
[25] RODIN. http://www.event-b.org/.
[26] Renato Silva and Michael Butler. Supporting Reuse
of Event-B Developments through Generic Instantia-
tion. In Formal Methods and Software Engineering,
volume 5885 of Lecture Notes in Computer Science,
pages 466–484. Springer, 2009.
[27] Colin Snook and Michael Butler. UML-B and Event-
B: An Integration of Languages and Tools. In Proc.
IASTED Intl. Conference on Software Engineering,
pages 336–341, 2008.