Transforming X-Machines to Z Specifications

P. Kefalas and A.Sotiriadou

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