In this paper we develop several new refinement relations of Z for multiple viewpoints oriented requirements method (MVORM). The original motivation is that we found the standard Z refinement relation is not adequate ...In this paper we develop several new refinement relations of Z for multiple viewpoints oriented requirements method (MVORM). The original motivation is that we found the standard Z refinement relation is not adequate or correct when considering specifications that have temporal relationships of operations. 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 systems to abstract the temporal state transitions. A simple example is used to show the procedures of MVORM. Finally some directions of further work are forwarded.展开更多
Traditional requirements method has some problems when it is used for large distributed systems. Multiple viewpoints oriented requirements method (MVORM) is a new method for resolving these problems. This paper develo...Traditional requirements method has some problems when it is used for large distributed systems. Multiple viewpoints oriented requirements method (MVORM) is a new method for resolving these problems. This paper develops two generic formal frameworks of MVORM, framework based on refinement relation (FBRR) and framework based on implementation relation (FBIR). They are generic, because no assumptions are made about the development process or the formal description languages to be used. Three kinds of specification relations and three kinds of specification transformations are discussed over FBIR and FBRR. This paper also compares the equivalence between FBIR and FBRR. We point out that an equivalent FBIR can be found for any FBRR, but reverse transformation is not always possible. We think FBIR is better than FBRR on most cases.展开更多
基金Supported by Natural Science Foundation of Hubei Province (98J0 75 ) Ziqiang Technical Innovation Foundation ofWuhan Universi
文摘In this paper we develop several new refinement relations of Z for multiple viewpoints oriented requirements method (MVORM). The original motivation is that we found the standard Z refinement relation is not adequate or correct when considering specifications that have temporal relationships of operations. 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 systems to abstract the temporal state transitions. A simple example is used to show the procedures of MVORM. Finally some directions of further work are forwarded.
基金Supported by Natural Science Foundation of Hubei Province (98J0 75 ) Ziqiang Technical Innovation Foundation ofWuhan Universi
文摘Traditional requirements method has some problems when it is used for large distributed systems. Multiple viewpoints oriented requirements method (MVORM) is a new method for resolving these problems. This paper develops two generic formal frameworks of MVORM, framework based on refinement relation (FBRR) and framework based on implementation relation (FBIR). They are generic, because no assumptions are made about the development process or the formal description languages to be used. Three kinds of specification relations and three kinds of specification transformations are discussed over FBIR and FBRR. This paper also compares the equivalence between FBIR and FBRR. We point out that an equivalent FBIR can be found for any FBRR, but reverse transformation is not always possible. We think FBIR is better than FBRR on most cases.
