Information Technology Reference
In-Depth Information
2.3 Event-B Models as Syntactic Objects
To define refinement patterns, we now consider an Event B model as a syntactic math-
ematical object. For brevity, we omit representations of some model elements here,
though they are supported in our tool implementation [13]. The subset of Event B mod-
els used in this paper can be described by the following data structure:
event ::
name
: EVENT
param
:PARAM
∗
guards
:PRED
∗
actions
:action
∗
model ::
var
:VAR
∗
inv
:PRED
∗
evt
:event
∗
action ::
var
:VAR
style
:STYLE
expr
:EXPR
Here
VAR
,
PRED
,
EXPR
,
EVENT
,
PARAM
are the carrier sets reserved corre-
spondingly for model variables, predicates, expressions, event names and parameters.
An event is represented by a tuple containing the event name, (a list of) its parameters,
guards, and actions. The reserved event name
init
denotes the initialisation event.
An action, in its turn, is a tuple containing a variable, an action style and an expression,
where an action style denotes one of the assignment types : i.e.,
STYLE =
{
:=
,
:
∈
.
Sub-elements of a model element can be accessed by using the dot operator:
act.style
is the style of an action
act
. Instances of the models, events and actions are constructed
using a special notation
,
:
|}
a
1
| ··· |
a
n
. The following example shows how an Event B
model is represented in our notation:
MACHINE
m
0
VARIABLES
x
INVARIANT
x
|
”
x
x
∈
Z
INITIALISATION
x
:= 0
EVENTS
count
=
BEGIN
x
:=
x
+1
END
∈
Z”
|
init
|−|−|
x
|
:=
|
”0”
,
|
:=
|
”
x
+1”
In the example,
x
is an element of
VAR
,
init
and
count
are event names from
EVENT
,
”
x
count
|−|−|
x
∈
Z”
is a predicate, and
”0”
,
”
x
+1”
are model expressions.
Now we have set a scene for a formal definition of refinement patterns that aim at
automating refinement process in general and Event B in particular.
3
Refinement Patterns
In this section we give formal definitions of transformation rules and refinement pat-
terns. Moreover, we propose a special language allowing us to construct transformation
rules, illustrating it by simple examples.
3.1
Definitions
Definition 1.
Let
S
be a set of all well-formed models defined according to the syntax
of Event B. Then a transformation rule
T
is a function computing a new model for a
given input model:
S
where
C
contains a set of all possible configurations (i.e., additional parameters) of a
transformation rule.
T
:
S
×
C
→
