Components and links

We extend the same set of figures denoting components of KAOS goal model to denote Event-B components in the refinement tree diagram and relationship among them. In the refinement tree diagram, a parallelogram denotes an Event-B event, a trapezoid denotes an Event-B invariant, and an arrow denotes a refinement from an abstract event to a concrete event. The extension parts are a bold line denoting a relationship between two events, and a dashed line denoting a relationship between an event and an invariant.

Each figure representing either an event or an invariant is described with natural lan-guage corresponds to the description of the Event-B component. The natural lanlan-guage acts as identifiers for formal descriptions in Event-B specifications. Even if it acts only as the identifiers, the meaning of the natural language should conform to the semantic of the corresponding predicate. Therefore, the natural language that can be used in the diagram is limited to what the first-order predicate logic of Event-B can describe. For examples, if a predicate in Event-B is written as (P =T RU E∧Q=T RU E) => R=F ALSE where P, Q, R are Boolean variables, one possible identifier of this predicate in the natural language is “If P and Q become true then R becomes false”. This is up to what P,Q, R represent in the specification.

The latter parts of this subsection describe these components and links.

Event

An event of Event-B is denoted by a parallelogram with the written description of the event. Figure 4.1 shows the general form denoting event in the refinement tree diagram.

The description of an event is written in the same way the event is described when modeling an Event-B model:

evt=ˆ anyp when Gwith W then S end

Event_name Any parameter When guards With witnesses Then actions

Figure 4.1: An event

This means that the description is composed of name, parameters, guards, witnesses, and actions of the event. The parts, which do not present in the description of an event, can be omitted. We allow using natural language as identifiers for the Event-B description of each event.

Because the refinement tree diagram is in the form of tree, we need to define a root node of the tree. According to semantics of Event-B specification, all events refine from an event named ’skip’. Thus, we define skip as the root node of every tree. Figure 4.2 shows the appearance of a root node.

skip

Figure 4.2: A root node

Invariant

Invariant_name:

predicate

Figure 4.3: An invariant

An invariant in Event-B is denoted by a trapezoid with the predicate form of the invariant. Optionally, one may also include the name of the invariant into the figure. We also allow using natural language instead of formal predicate to describe an invariant.

Figure 4.3 shows the general appearance of an invariant.

In all Event-B models, there are invariants which are for variable typing. These kind of invariants can be omitted when drawing a refinement tree diagram.

Refinement of event

A refinement of event is represented by an arrow with a small circle for linking all concrete events refine the same abstract event through lines. Here, we specify that ‘refinement of

Abstract_event When guards Then actions

Concrete_event_1 When guards’

Then actions’

Concrete_event_2 When guards’’

Then actions’’

Figure 4.4: Refinements of event

event’ means there is some changes in the description of a concrete event comparing to its abstract event. The appearance of refinements of event in a refinement tree diagram is shown in Figure 4.4. Because abstract events belong to an abstract machine and concrete events belong to a concrete machine, this means that the arrow can separate level of the refinement tree diagram. For a refinement, if the proof obligations GRD and F IS as defined in Section 2.1 are successfully discharged, the refinement is valid.

Event When guards Then actions

Event When guards Then actions

Figure 4.5: Copy of event

If the description of a concrete event is the same with its abstract event, we regard the event as a ‘copy’ of the abstract event. In this case, we use a plain arrow to show the copy as in Figure 4.5.

Both the refinement and the copy of event can be written into Event-B specification as

‘REFINES’ relationships between abstract events and concrete events.

Event-event relationship

There might be some relationships among two or more events in the same machine which we want to explicitly describe. These relationships are needed because they can help stakeholders understand how events interact with each other. The relationships can be shown through lines among events. We allow writing type and name of the relationship

Event_1 When guards_1 Then actions_1

Event_2 When guards_2 Then actions_2 [Relation_type]

Relation_name

Figure 4.6: Event-event relationship

on the line. Figure 4.6 shows the general appearance of the relationship between events.

For the scope of this thesis, we define only two types of relationships: parallel and be-fore. The detailed explanations about these two types of relationships are provided in Section 4.4. Even though these relationships are explicit in our diagram, they are implicit when written in Event-B specification. In facts, Event-B does not provide notations for explicitly denoting these relationships.

Event-invariant relationship

Event When guards Then actions

Invariant:

predicate

Figure 4.7: Event-invariant relationship

Invariants are needed for restricting possible values of variables. They can show rela-tionship among variables in a system. Thus, invariants also restrict the possible results of events. Conversely, events might provide us some idea about important invariants needed to be include in a specification. These relationships between events and invariants can be shown in a refinement tree diagram through dashed lines between them. Figure 4.7 shows how to link an invariant to an event. We encourage linking an invariant to all events which it is related to. However, this might reduce increase the complexity of a refinement tree diagram. For convention, if an invariant is related to a lot of events of an Event-B machine, we allow omitting all dashed lines for linking them, or showing only some necessary links. Another way to link an invariants to a set of concrete events which refines the same abstract event is to link the invariant to the small circle representing refinement as in Figure 4.8.