'

Extensions of standard Z refinement relation for multiple viewpoints oriented requirements method

He Yanxiang, Song Qiang, Huang Qian Wuhan University, China

qe extend the standard Z refinement relation for multiple viewpoints oriented requirements method (MVORM). The original motivation is that we found the standard Z refinement is not adequate or correct when considering specifications that have temporal relationships of operations. We do our work under a generic framework of MVORM. The concept of temporal state variables is introduced into Z. Then new implementation relations are defined and new refinement relations are deduced, mainly for temporal state variables to process temporal relationships of operations. We use state transition system to abstract temporal state transitions. A simple example is used to show the usage of MVORM. Finally some directions of further work are forwarded.'