PRISM

摘要： 机器人操作系统(robot operating system,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题,ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法,分析、验证ROS2系统数据分发机制的实时性和可靠性.首先,提出一种面向数据流的ROS2数据分发服务的形式化验证框架,并对通信系统模块建立概率时间自动机模型;其次,运用概率模型检测器,通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性;最后,基于重传机制、服务质量(quality of service,简称QoS)策略分析,通过设置和调整服务质量参数,实现不同的数据需求和传输方式的量化性能分析,为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考.

摘要： 数字化仪控系统(DCS)是核电厂的神经中枢,是一种以微处理器为基础,采用控制功能分散显示、操作集中、兼顾分而自治和综合协调的设计原则的仪表控制系统,它对机组的安全、经济运行起着至关重要的作用。I/O卡件是DCS与现场仪表交互的关键部件,当I/O卡件出现故障时,需要及时更换,所以I/O卡件需要一定数量的备件。如果备件过少,系统可用率达不到要求,反之会导致总费用过高。基于马尔可夫模型,提出了一种可用率约束条件下,考虑共因失效的I/O卡件备件数量优化方法。并采用概率检测器PRSIM实现了对马尔可夫模型的定量分析,得出了满足可用率的约束条件的最少备件数,达到降低核电厂DCS运行维护费用的同时,保证其安全可靠运行的优化效果。

摘要： 文中基于数字高程模型,建立了多元线性回归插值模型(MLR)和PRISM空间插值方法,并与传统的反距离权重法(IDW)和普通克里金插值法(OK)进行比较。结果表明:1)江西省5月、7-10月降水量与海拔高度存在显著的相关性,与坡度、坡向无明显相关。2)从插值精度来看,3-9月PRISM和MLR空间插值精度明显优于IDW和OK,冬半年IDW和OK插值精度略高于MLR和PRISM;4种插值方法的年降水量插值精度排序为PRISM>MLR>OK>IDW;PRISM和MLR在高海拔地区的插值精度远高于IDW和OK。3)从插值效果来看,4种插值方法的降水空间分布具有一致性,MLR和PRISM优于IDW和OK。

摘要： 针对当前缺少对微服务组合平台的服务质量(QoS)指标进行分析验证的问题,提出一种基于模型检测的形式化验证方法,对影响微服务平台性能的因素进行分析评估.首先,将微服务组合的服务资源配置过程划分为服务请求、资源配置和服务执行3个阶段,并分别由服务请求队列、服务请求配置器和提供服务资源的虚拟机等模块实现;其次,将各个模块的实现过程建模为带标记Markov回报模型(LMRM),借助类似于进程代数的同步概念获得微服务组合过程的全局模型;接着,用连续随机回报逻辑公式刻画期望的QoS指标;最后,将形式模型与逻辑公式作为模型检测工具PRISM的输入以获得验证结果.实验结果表明,LMRM可较好地用于微服务组合平台的建模和QoS验证分析.

摘要： 随着航空发动机技术的不断发展,对其性能要求不断提高,使得航空发动机的安全性和可靠性变得愈发重要.然而,当前针对航空发动机的可靠性分析方法较少考虑系统失效时的动态特性,面向《航空发动机适航规定》(CCAR33-R2),考虑航空发动机危害性发动机后果发生时系统的动态特性,提出了一种将动态故障树和概率模型检测相结合的可靠性分析方法,对航空发动机的可靠性进行分析.首先,通过动态故障树对航空发动机的动态行为进行建模,并将其转换到离散时间马尔科夫链模型;然后基于概率模型检测语言PRISM对离散时间马尔科夫链模型进行描述,并利用相应工具进行定量分析,将顶事件发生概率和《CCAR33-R2.75》条款规定的故障发生概率比较,验证航空发动机是否符合《CCAR33-R2.75》条款安全性要求;最后对某型航空涡轮发动机进行实例建模分析,验证所提方法的正确性与可行性.

摘要： 匿名WBANs通信技术是保护互联网用户和服务器间隐私的最有力手段之一,但匿名WBANs无证书认证协议的形式化验证仍是亟待解决的难题.采用概率模型检测的方法对一种基于云辅助的匿名WBANs的轻量级无证书认证协议建立离散时间马尔科夫链模型,在协议建模的状态迁移中加入了攻击率,重点对攻击率进行定量分析,用概率计算树逻辑对协议属性进行描述,利用PRISM概率模型检验工具对协议进行定量分析和验证,并且与SIP协议进行性能方面的对比.验证结果表明:在匿名WBANs通信环境下,云辅助的轻量级无证书认证协议各实体间所受攻击率对协议的不可否认性、时延性和有效性有不同程度的影响,控制好攻击率可以提高协议安全性,这对医疗服务质量和实时监测效率的提高以及远程医学的基本需求有着极大的意义.

摘要： 为了让玩家们能够拥有一个更加靓丽的游戏环境,背光同步技术除了在PC硬件中大放异彩之外,还被外设厂商所广泛采用,比如赛睿推出了Prism、Razer推出了Chroma。而冰豹也整合了自家旗下外设产品的背光系统,推出了Aimo智能灯效系统,前不久我们才介绍了拥有该功能的Vulcan 120 Aimo机械键盘。那么作为一个背光同步技术标配的游戏鼠标和游戏耳机又在哪儿呢?今天我们为大家带来的便是拥有Aimo智能灯效系统的冰豹Kone Aimo游戏鼠标、Khan Aimo游戏耳机。

摘要： 最近在“吃鸡”游戏中跟玩家们老聊一个话题,如果你预算有限,帮你尽快吃鸡的方法是什么。答案是多種多样的:有的建议加一根内存;有的建议买一块小容量的SSD来作为系统盘;更有甚者建议淘一款10系旧显卡。在我看来,最简单的方式莫过于给你的鼠标找一个好的“着陆点”。

摘要： 本公开涉及用于获取PET图像的设备和正电子发射断层摄影（PET）扫描仪以及用于生成PET图像的系统。本公开描述了一种可以具有一个或多个可移动部分的设备。该设备可以包括上部和下部。上部和下部限定用于患者的体腔。上部或下部中的至少一个可以是可移动的。上部和下部可以分别包括盖和翼，盖和/或翼中的至少一个可以包括一个或多个检测模块。翼也可以相对于对应的盖移动。

摘要： 本发明公开了一种基于PRISM的抗SEU的可靠性验证方法。本发明是一种将形式化验证技术应用于系统早期设计阶段，分析不同加固技术和参数下的系统可靠性、可用性和安全性，帮助设计人员开发出更可靠和更有效的解决方案的一种方法，使用PRISM概率模型检验器考虑内存刷新、冗余等加固技术对系统设计进行建模，采用CDFG调度(用于故障恢复)，故障检测覆盖率(安全性相关)和特征库(用于提供各组件的单粒子翻转发生概率)，建立好的模型能够描述系统能够到达的所有状态。