Animating X-Machines through Prolog

P. Kefalas

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