Transforming X-Machines to Z Specifications
Abstract: Specification methods describe either
the dynamic or the static aspect of a system, or both. The dynamic part
represents the system’s control and is usually defined in terms of states,
transitions, event triggering etc., whereas the static part represents
the system’s data and is usually defined in terms of data structures, tables
and data processing functions for retrieving, updating and checking data.
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. In contrast, Z is a popular formal notation for
specifying only the static part of a system, in terms of system state and
operations on it. This report is addressing the issue of converting a X-Machine
specification to Z notation. The methodology of deriving a Z specification
from a X-Machine definition is given as well as further directions for
automating this process are discussed.
Keywords: Formal specification, Automatic Translation
Appeared in: Techical Report WP-CS06-00
Available: Hardcopy on request from the authors.
Back
to Dept. of Computer Science, CITY Liberal Studies
Back
to Petros Kefalas home page