-
题名基于交互式马尔可夫链的可信动态度量研究
被引量：9
- 1
-
-
作者
庄琭
蔡勉
沈昌祥
-
机构
北京工业大学计算机学院
可信计算北京市重点实验室
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2011年第8期1464-1472,共9页
-
基金
国家“九七三”重点基础研究发展计划基金项目(2007CB311100)
国家“八六三”高技术研究发展计划基金项目(2009AA012437)
“核高基”国家科技重大专项基金项目(2010ZX01037-001-001)
-
文摘
可信动态度量为保障可信计算平台的可靠运行提供了重要支撑.根据系统的可靠性、可用性、信息和行为安全性,提出了可信度量要达到的目标.当前的可信度量集中在可信功能度量上,基于交互式马尔可夫链增加性能特征指标度量,即在预期行为描述模型中,运用变迁系统模型描述功能预期,通过将体现在可靠性上的路径概率与预期的关联,获取完成特定行为功能在时间特征上的预期,用于性能特征指标的度量.所构建的功能与性能特征预期用于对系统运行时证据实施相应的功能与性能上的可信性验证.基于交互式马尔可夫链的动态度量模型,从性能角度完善了对可靠性的保障,更全面地确保了系统的可信.
-
关键词
可信计算
可信动态度量
交互式马尔可夫链
功能度量
性能度量
-
Keywords
trusted computing
trusted dynamic measurement
interactive markov chains
functionality measurement
performance measurement
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
-
题名基于时间策略的连续时间Markov过程验证
被引量：1
- 2
-
-
作者
黄镇谨
陈波
欧阳浩
-
机构
广西科技大学计算机工程学院
-
出处
《广西科技大学学报》
CAS
2014年第3期59-62,86,共5页
-
基金
广西自然科学基金项目(2013GXNSFBA019280)
同济大学嵌入式与服务计算教育部重点实验室开放课题基金(2011-02)
广西高校科学技术研究项目(LX2014186)资助
-
文摘
对系统模型进行验证是保证系统安全的一个关键.连续时间Markov过程可以刻画复杂并发系统的随机、概率、不确定性特征.提出时间依赖策略下连续时间Markov过程验证方法,将连续时间Markov过程转换成为交互式马尔科夫链,给出模型的转换方法及不确定性选择策略的转换方法,最终通过求解交互式马尔科夫链的时间可达概率最值实现对连续时间Markov过程模型的验证.理论分析表明,提出的方法具有可行性.
-
关键词
马尔科夫决策过程
交互式马尔科夫链
时间有界可达概率
时间策略
-
Keywords
markov decision process
interactive markov chains
time -bounded reachability probability
timedschedulers
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名交互式马尔科夫链上强模拟关系的计算
被引量：1
- 3
-
-
作者
赵锡英
张明新
邢敬宏
-
机构
兰州工业高等专科学校计算机工程系
-
出处
《兰州理工大学学报》
CAS
北大核心
2008年第1期76-81,共6页
-
基金
甘肃省自然科学基金(3ZS051-A25-047)
甘肃省教育厅科研基金(0712-02)
-
文摘
对随机进程代数模型交互式马尔科夫链(IMCs)上的模拟关系进行研究,根据不动点定理和权函数的定义,给出交互式马尔可夫链模型上强互模拟等价和强模拟前序的判定算法,对算法的时间复杂度进行分析.
-
关键词
交互式马尔可夫链
强互模拟等价
强模拟前序
算法
计算复杂度
-
Keywords
interactive markov chains
strong bisimulation
strong simulation preorder
algorithm
computational complexity
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名交互式马尔科夫链上弱模拟关系的计算
- 4
-
-
作者
赵锡英
张明新
邢敬宏
-
机构
兰州工业高等专科学校软件工程系
-
出处
《兰州理工大学学报》
CAS
北大核心
2008年第2期96-100,共5页
-
基金
甘肃省自然科学基金(3ZS051-A25-047)
甘肃省教育厅项目(0712-02)
-
文摘
对交互式马尔可夫链模型(IMCs)上的弱模拟前序关系的计算算法进行讨论.在IMCs上判断弱模拟关系时,重点对概率转移关系进行弱模拟前序关系的判断,同时考虑内部动作对系统的影响.通过引入适当的变量,将IMCs上弱模拟定义中的马尔可夫转移条件转化为求解一个线性规划问题的解.利用该线性规划问题的数值求解方法,可在多项式时间内求得该线性规划问题的解.从而得到判定IMC上两个进程是否弱模拟的多项式时间算法.
-
关键词
交互式马尔可夫链
弱模拟前序
算法
计算复杂度
-
Keywords
interactive markov chains
weak simulation prelude
algorithm
computative complexity
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名随机进程代数IMCs的性能评价
- 5
-
-
作者
赵锡英
张明新
-
机构
兰州工业高等专科学校软件工程系
-
出处
《兰州理工大学学报》
CAS
北大核心
2008年第3期73-76,共4页
-
基金
甘肃省自然科学基金(3ZS051-A25-047)
甘肃省教育厅科研基金(0712-02)
-
文摘
将马尔可夫路径概率计算方法推广到随机进程代数:交互式马尔科夫链(IMCs)模型上.由于IMCs中存在动作转移和概率转移,两种不同性质的转移破坏了系统的稳定性,因此在IMCs的性能刻画中,去掉系统的稳态性刻画,给出动作和概率转移共存的IMCs模型的路径定义和基于概率转移率的路径转移发生的概率计算方法,解决了Until算子的描述.使用基于动作的逻辑aCSL给出IMCs的性能评价.证明该方法的正确性,它是纯马尔可夫链模型中性能评价方法的扩展.
-
关键词
交互式马尔可夫链
性能评价
路径
aGSL逻辑
-
Keywords
interactive markov chains
performance evaluation
path
aCSL logic
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名基于马尔可夫链的性能检测器的设计与实现
被引量：1
- 6
-
-
作者
许振兴
吴尽昭
陈剑锋
-
机构
中国科学院成都计算机应用研究所
-
出处
《计算机应用》
CSCD
北大核心
2010年第A01期215-217,共3页
-
基金
国家973计划项目(2007CB310803)
国家863计划项目(2007AA01Z143)
+1 种基金
国家自然科学基金资助项目(6087311860973147)
北京交通大学科学研究基金资助项目(2007RC110)
-
文摘
为了可视化建模和验证并发系统的性能,设计并实现了一个以交互式马尔可夫链为数学原型的性能检测器。对该软件的系统结构、数据结构和功能模块等进行了探讨和设计,并举例验证。该软件采用Java Swing界面编程技术,支持图形化建模系统和撰写逻辑公式,界面友好,易于操作。
-
关键词
模型检测
交互式马可夫链
时序逻辑
性能检测
系统结构
-
Keywords
model checking
interactive markov chains （IMC）
temporal logic
performance checking
system architecture
-
分类号
TP311.52
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于交互式马尔可夫链的模型检验
被引量：1
- 7
-
-
作者
许翔
吴尽昭
林连南
陈剑锋
-
机构
中国科学院成都计算机应用研究所
-
出处
《计算机应用》
CSCD
北大核心
2008年第7期1868-1871,共4页
-
文摘
研究了基于交互式马尔可夫链(IMC)的模型检验,IMC是集功能描述和性能刻画为一体的并发系统模型,模型检验是一种自动功能验证与性能评价技术。文中提出的模型检验算法结合了传统的功能验证与性能评价的功能,并且与现有的算法相一致。实验分析表明,该算法具有较高的性能,适用于大型复杂系统的验证和评价。
-
关键词
交互式马尔可夫链
模型检验
性能评价
-
Keywords
interactive markov chains（IMC）
model checking
performance evaluation
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-
