A Design Language and Tool for X-Machine Specification

E.Kapeti and P. Kefalas

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