绿色评价模型的互模拟等价及逻辑保持  

Bisimulation Equivalence and Logical Preservation for Green Evaluation Model

作　　者：钮俊[1,2,3] 曾国荪[2,3] 王伟[2,3] 

机构地区：[1]宁波大学信息科学与工程学院,浙江宁波315010 [2]同济大学计算机科学及技术系,上海201804 [3]同济大学嵌入式系统与服务计算教育部重点实验室,上海201804

出　　处：《计算机学报》2013年第5期967-976,共10页Chinese Journal of Computers

基　　金：国家"八六三"高技术研究发展计划项目基金(2007AA01Z425;2009AA012201);国家"九七三"重点基础研究发展规划项目基金(2007CB316502);国家自然科学基金(90718015;61103068;61174158);NSFC-微软亚洲研究院联合项目(60970155);教育部博士点基金(20090072110035);上海市优秀学科带头人计划项目(10XD1404400);高效能服务器和存储技术国家重点实验室开放基金(2009HSSA06);浙江省自然科学基金项目(LY12F020031);宁波市自然科学基金(2012A610062)资助~~

摘　　要：绿色计算中,复杂系统的绿色评价是一个重要的研究课题,其核心任务是判断运行时时间、空间资源消耗是否满足环境约束或限定.设计时,采用模型检测技术,自动、完备、高效地进行绿色评价,是一种新颖且有效的解决方案,但可能出现的状态爆炸问题将影响评价成败或效率.引入随机决策过程作为绿色评价模型;用时态逻辑刻画包含行为正确性及时间、空间资源约束的绿色评价指标;定义不确定语义理解下评价模型状态的互模拟等价规则,给出互模拟商的构造方法以及商模型调度,并比较等价语义下的行为机理;运用结构化归纳法证明互模拟等价保持评价结论.分析表明,互模拟等价可用作状态约简手段,为基于模型的绿色评价提供理论支撑和技术手段.In green computing, the study of green evaluation approaches is an important area. Their main task is to validate whether the consumed time or spatial resources fall into specified bounds while the considered system running correctly. One can employ model checking, which is automatic, complete and effective, as a new green evaluation approach, but the emergence of state space explosion may result in that it is not available or ineffective when green evaluating. In this paper we model the considered systems as stochastic processes and the evaluation properties, which allowed for behavioral correctness and time or spatial resources constraints, are expressed by temporal logic. We define the bisimulation equivalence relation, which allowed for nondeter- minacy, the syntax of bisimulation quotient and the policy of quotient model, and compare the quotient behavior with the original one. We also prove that the bisimulation equivalence relation preserve evaluation result. Thus, bisimulation equivalence can be viewed as a feasible states reduction approach, and provides theoretical foundation in model-based green evaluation approaches.

关 键 词：绿色评价 模型检测 随机过程 评价指标 互模拟 绿色计算 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]