Information Technology Reference
In-Depth Information
Fig. 3.
Verification and validation of an
sp
X-machine
(DCG) notation [10], which apart from the syntax errors, output as warnings any kind of
logical errors or omissions. The semantic analysis and the rules for transformation are
being checked by the compiling component, with the aid of defined rules under which
the specification is translated into the equivalent Prolog code. This Prolog code is after
utilised by an animation tool, which simulates the computation of an X-machine. Fur-
thermore, the model checking component defines a new logic, XmCTL [16], and with
the implementation of a model checking algorithms can determine whether a property
is true or false. And finally, XMs are supported with automatic generation of test cases,
which is proved that finds all faults in the implementation [17].
Taking
sp
XMs into consideration, the following discussion will concentrate on in-
vestigating whether they inherit the mentioned verification and validation techniques of
XMs. An informal proof that an
sp
XM is equivalent to any XM could be derived by
investigating:
-
The memory
M
of a normal XM is equivalent to the structure of memory
M
, posi-
tion
Π
and direction
Θ
within an
sp
XM. In other words, the position and direction
can either become members of the memory tuple in a normal XM model, or they
can be excluded from the model without loss of its integrity.
-
Anyfunctioninan
sp
XM model can be translated into a function of the normal
XM. More particularly, the predefined spatial operations of a function in an
sp
XM
model can be omitted or replaced with the standard XMDL syntax to preserve the
logic flow.
Along these lines, by removing the newly defined components that in essence define
an
sp
XM, what we get is still a completely valid skeleton of a normal XM model.
Therefore,
sp
XMs tend to provide a standardised way of representing some properties
