实时系统概率模型检测问题研究

发布时间：2022-01-04 12:21

　　随着实时系统使用范围的日益扩大,对实时系统的可靠性的要求也越来越高。对实时系统的功能、性能和可靠性进行的评估已成为一个重要的研究课题。作为提高软件可信度的重要手段,概率模型检测可以自动化地对软件及硬件系统完成形式化验证,从定量的角度给出其属性的分析结果。本文的主要工作就是研究对实时系统实施概率模型检测的理论框架,提出对实时系统进行概率模型检测的解决方案,为概率模型检测技术进一步走向应用进行探索。由于实时系统其自身的特殊性,对实时系统进行概率模型检测是十分困难的。归纳起来,实时系统具有以下三个特性:实时性,自稳定性和交互性。第一,由于实时系统具有实时响应的特性,实时系统模型的行为往往是随时间连续变化的。这种模型的根本特征是其状态空间是无限的。但是概率模型检测技术只适用于有限状态空间模型,因此,对实时系统实施概率模型检测几乎是不可能的。第二,实时系统具有自稳定的特性,即在无需外界干预的情况下,实时系统可以自动地从一个不稳定状态到达另一个稳定状态。支配实时系统自稳定过程的自稳定算法的性能成为制约实时系统的性能的关键因素。第三,实时系统要和工作环境或用户进行交互。对实时系统的性能、可靠性的评估... 

【文章来源】：华东师范大学上海市 211工程院校 985工程院校 教育部直属院校

【文章页数】：164 页

【学位级别】：博士

【部分图文】：

模型检测的流程

图 2. 1 一个 DTMC D.1中的 DTMC M，其迁移关系可以用迁移概率矩阵P= 的模型检测属性规约可以用概率计算树逻辑(Probabilistic C)[24]描述，它是时序逻辑 CTL 的概率扩展。CTL 语法). PCTL语法如下： | a | /\ | | P~p[ ]

图 2. 2 确定 Prs( a U b)的概率 DTMC 附加成本/收益MC 也可以增加成本/收益计算。对于 DTMC，成本/收益可以), 其中 ρ,ι 分别代表状态成本（收益）和迁移成本（收益）。ρ(s)指 DTMC 处于状态 s 时所消耗的成本（获得的收益）。可以由成本（收益）函数 ρ：S R+赋值给状态。迁移成本 DTMC 从状态 s 迁移到 积累的成本（收益）。迁移成本（收收益）函数 ι：S S R+赋值给迁移。/收益用来附带资源使用情况信息，如能量消耗或者丢失的分过对 DTMC 加批注的方式来表示。成本/收益可以有两种形的。对于一个 DTMC D =｛S,sinit,P,AP,L｝，成本是两个函数构

【参考文献】：
期刊论文
[1]马尔可夫决策过程的限界模型检测[J]. 周从华,邢支虎,刘志锋,王昌达.  计算机学报. 2013(12)
[2]可信计算的研究与发展[J]. 沈昌祥,张焕国,王怀民,王戟,赵波,严飞,余发江,张立强,徐明迪.  中国科学:信息科学. 2010(02)
[3]高可信软件工程技术[J]. 陈火旺,王戟,董威.  电子学报. 2003(S1)



本文编号：3568329