XMDL USER MANUAL 1.6
Abstract: One of the most essential phases of software
development is the system specification. X-machines is an intuitive formal
method which can be easily applied at this phase and also facilitate testing
in order to prove the correctness of an implementation with respect to
the specification. Although the X-Machine theory is already defined in
detail mathematically, there is a lack of automated tools which can facilitate
its use. In this paper, a brief introduction to the X-Machine theory is
presented and a language for specifying X-Machines is defined, which could
act as a communication protocol among various X-Machine tools. In addition,
a proof tool is presented which checks special properties of X-Machines
that are defined as prerequisites for the X-Machine testing algorithm.
This is the complete manual for the syntax of XDML. A number of examples
for X-Machine specifications is also given, coded in XMDL.
Keywords: X-Machines Specification Language
Appeared in: Techical Report WP-CS07-00
Available: Hardcopy on request from the authors.
Back
to Dept. of Computer Science, CITY Liberal Studies
Back
to Petros Kefalas home page