A Design Language and Tool for X-Machine Specification
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.
Keywords: X-Machines, Description Language for Specification,
Test-Completeness, Output-Distinguishability
Appeared in: Proceedings of the 7th Panhellenic Conference on
Information Techology, Ioannina, August 1999.
Available: Hardcopy on request from the authors. .
Back
to Dept. of Computer Science, CITY Liberal Studies
Back
to Petros Kefalas home page