基于状态转换系统的Z语义模型扩充

Extensions of Semantic Model of Z Based on Status Transition System

利用状态转换系统对 Z语义模型进行分析 ,指出其三种不足 ;然后利用状态转换系统、有限状态转换系统和时序状态转换系统 ,对 Z语义模型分别进行多样性、有效性和时序性扩充 ,定义多种数据实现关系和时序实现关系 ,导出相应的求精关系 ;并通过一个简单的实例说明

Using status transition system, we analysis the semantic model of Z and point out three kinds of shortages. Then we extend the semantic model of Z on diversity, validity and temporality by using status transition system, finite status transition system and temporal status transition system. Some kinds of often-used data implementation relations and temporal implementation relations are defined, and corresponding refinement relations are developed. A simple example is forwarded to illustrate the usage of extensions of semantic model of Z in multiple viewpoints requirements engineering.