Animating X-Machines through Prolog
Abstract: The X-Machine theory is based on Finite
State Machine theory and strongly integrates the problems of data and control
processing specification in a single formal model. X-Machines can represent
information about states, transitions, inputs, outputs, memory values and
functions, which operate on memory values and inputs. This report
is addressing the issue of animating a X-Machine specification through
Prolog. The X-Machine is represented by XMDL, a special language for describing
X-Machines and its components, which is automatically translated into Prolog
code. The animator, given a sequence of inputs, executes the Prolog code
and produces the corresponding output of the X-Machine specification. Among
others, the animator can be used as a tool in order to compare the sequence
of its outputs to the sequence of outputs produced by the real implementation,
and therefore find possible faults with regard to the specification..
Keywords: Formal specification, Automatic Translation, Specification
Animation
Appeared in: Techical Report WP-CS01-00
Available: Hardcopy on request from the authors.
Back
to Dept. of Computer Science, CITY Liberal Studies
Back
to Petros Kefalas home page