摘要
带数据约束的概率系统是指一种既带有概率约束,又带有数据变量约束的计算系统,应用非常广泛.对这类系统而言,确保其正确性和可靠性是至关重要的.目前对带数据约束的概率系统模型的规范及验证研究较少,本文提出了一种针对概率系统的带数据约束的规范.对于传统的时序逻辑如计算树逻辑和概率计算树逻辑来说,尽管这些逻辑很强大,但是只能反映系统的时序性质,为了解决这些局限性,本文提出一个新的形式化语言来表达度量性质查询,同时保留表达时序性质的能力.最后,文章给出针对概率系统度量性质的检测算法并通过实例说明本文提出的方法可行有效.
Probabilistic system with data constraints which is widely used refers to computing systems both with probabilistic-bound and data variables constraints. For such system it is crucial to ensure its accuracy and reliability. Now there are few studies about the specification and verification of probabilistic system with data constraints. In this paper we present a specification with data constraints for probabilistic system. As for traditional temporal logic like CTL and PCTL, the logic is powerful, but only reflecting the temporal properties. To address these limitations, in this work we propose a new, formal language to express performance queries, while retaining the ability to express temporal properties. Finally,we give a checking algorithm for performance queries of probabilistic systems.
出处
《小型微型计算机系统》
CSCD
北大核心
2015年第3期550-555,共6页
Journal of Chinese Computer Systems
基金
航空科学基金项目(20128052064)资助
国家"九七三"计划重点基础研究发展计划项目(2014CB744900)资助
中央高校基本科研业务费专项资金(NZ2013306)资助
