5G网络认证与密钥协商协议的形式化验证与分析

网络攻击的手段层出不穷,如中间人攻击,重放攻击, DoS攻击等,以此获取不当利益.密钥协商协议的设立是为合法用户提供正确认证入口,并拒绝攻击者的非法接入和攻击.密钥协商协议是保护移动通信提高服务质量的第一道安全防线, 5G网络密钥协商协议在实际环境中仍然存在安全隐患,其协议本身的安全特性能否满足要求仍未可知,本文提出使用基于概率模型检测的方法,通过对5G网络密钥协商协议的各协议方实体进行建模,建立离散时间马尔科夫链模型,在建模过程中考虑外界的攻击影响,引入攻击率来描述外界的影响程度,通过攻击率对5G网络密钥协商协议的研究进行定量分析,使用概率计算树逻辑对待验属性规约进行编码描述,利用概率模型检测工具PRISM进行实验.实验结果表明:在引入攻击率的5G网络密钥协商协议模型中, 5G网络密钥协商协议各协议方实体所受攻击的影响对该协议的时延性,有效性,保密性等属性规约的性能有不同程度的影响,因此,研究外界网络攻击对协议的安全性能的影响,对加强协议安全性能及其改进具有一定借鉴意义,并对5G网络密钥协商协议的安全特性的提升和保护用户的经济与信息安全具有很大的意义.     

从单视点DVC到多视点DVC的研究进展

多视点视频编码对编码器的功耗、复杂度、存储能力和传输能力有较高的要求,而分布式信源编码理论恰恰适应了这一需求.为了使人们对这一技术现状有一概略了解,首先总结了分布式视频编码的基本理论和关键技术,然后介绍了分布式信源编码理论从单视点到多视点的拓展,接着论述了分布式多视点视频编码的研究现状,最后分析了分布式信源编码理论在多视点视频编码领域的发展前景.     

基于VIC-3L模型的黑河上游流域径流模拟研究

为解决我国西部地区气象水文站点稀少、分布不均匀的问题,并充分表达气象要素的空间差异性,利用VIC-3L模型对黑河上游山区流域进行了模拟研究,以检验该模型在干旱区较细网格尺度上的适用性和模型参数移植以及改造的可能性。模型所需要的土壤参数和植被参数主要通过野外实测、土壤普查数据或根据有关参考文献获得。模拟结果显示,在日、月尺度上的径流模拟变化趋势与实测径流除了在时间上有大约2~3 d的滞后外,其他方面较为吻合,在丰水年日、月尺度上的径流模拟远好于同尺度上枯水年的模拟精度,说明模型在研究区具有一定的适用性,但有待于进一步改进。     

面向复杂随机系统的启发式统计模型检测方法 *

统计模型检测是一种高效的验证技术,常用于复杂的随机系统验证,如分布式算法等。而在超长路径上对性质进行验证时,其验证效率会急剧降低。为解决这个问题,这里提出一种启发式的统计模型检测算法。在对路径进行验证时,我们会查找帮助剪枝的最短前缀。并在后续抽样时,利用前缀信息直接判定路径是否满足给定性质,避免进入费时的路径验证阶段。在与PRISM的比较中,它的路径验证次数相对更少且平均抽样路径长度更短。因此使统计模型检测技术可应用于超长路径上的性质验证。     

The structure of poly(ethylene oxide) liquids: comparison of integral equation theory with molecular dynamics simulations and neutron scattering

Polymer reference interaction site model (PRISM) calculations and molecular dynamics (MD) simulations were carried out on poly(ethylene oxide) liquids using a force field of Smith, Jaffe, and Yoon. The intermolecular pair correlation functions and radius of gyration from theory were in very good agreement with MD simulations when the partial charges were turned off. When the charges were turned on, considerably more structure was seen in the intermolecular correlations obtained from MD simulation. Moreover, the radius of gyration increased by 38% due to electrostatic repulsions along the chain backbone. Because the partial charges greatly affect the structure, significant differences were seen between the PRISM calculations (without charges) and the wide angle neutron scattering measurements of Annis and coworkers for the total structure factor, and the hydrogen/hydrogen intermolecular correlation function. This is in contrast to previous PRISM calculations on poly (dimethyl siloxane).     

基于模型检测的微服务组合平台QoS验证

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

基于概率模型检验的云渲染任务调度定量验证

云渲染技术已被广泛应用于影视和动漫等行业.与传统的渲染农场和租赁市场模式不同,云渲染系统依托云计算基础设施提供多种软件服务进行渲染作业的方式,正逐渐成为新兴的计算模式.由于任务执行和资源操作等作业调度对于用户而言是透明的,这要求云渲染系统应具备智能化以实现计算资源优化调度和多端任务管理,并对系统可靠性提出了更高要求.针对这一问题,提出了采用概率模型检验对云渲染系统任务调度进行定量评估.首先,考虑渲染服务失效等因素引发的随机系统异常和指令错误,如文件损坏和渲染任务超时等,提出了基于离散马尔可夫链(DTMC)的概率模型对云渲染系统的文件准备模块、资源请求模块、渲染任务执行模块进行形式化建模;其次,从服务质量属性角度提出了9类验证性质用于定义云渲染系统的可靠性,采用概率计算树逻辑(PCTL)描述检验性质公式并执行工具PRISM计算和验证渲染系统可靠性;最后,结合案例和实验证明了该方法的可行性和有效性,尤其是对改进前后云渲染系统进行定量检验,可用于指导如何进行失效恢复和任务切换.因此,该方法在一定程度上可提高云渲染系统的可靠性.     

Fast fabrication of silicon based microstructures using 355 nm UV laser

Abstract

In this study, a 355 nm UV Nd:YAG laser is used to process silicon wafers. In order to obtain microstructures with high aspect ratio, a dual prism optical system is set up to control the cutting linewidth of the UV laser beam. During the laser beam propagation through the prisms, the two prisms are rotated with the same angular velocity, which results in the focal spot of the laser beam moving in a circular path on the silicon substrates. When the laser beam moves relative to the holder (workstation), a laser cutting process can be carried out. With this laser system, the cutting linewidth is controllable ranging from 10 μm to 1 mm by adjusting the initial phase difference in the two prisms. The experimental results show that arbitrary shaped silicon based microstructures with high aspect ratio can be fabricated by this 355 nm UV laser system, and the aspect ratio over 10 can be obtained.     

Modeling and Analysis of Data Flow-Oriented ROS2 Data Distribution Service

Robot Operating System (ROS) is an open-source, meta-operating system, which can provide a structured communication layer based on the message mechanism on heterogeneous computing clusters. To improve the unsatisfactory real-time performance and reliability of data distribution in ROS1, ROS2 is proposed with a data flow-oriented data distribution service mechanism. This study validates the real-time performance and reliability of the ROS2 data distribution mechanism by means of probabilistic model checking. Firstly, a formal validation framework is put forward for the data flow-oriented ROS2 data distribution service system, and the probabilistic timed automata model is set up for the communication system module. Secondly, the probabilistic model checker PRISM is used to verify the real-time performance and reliability of data flow-oriented ROS2 data distribution service through the analysis of data loss rate and system response time. Finally, depending on the retransmission mechanism and Quality of Service (QoS) policy analysis, different data requirements and quantitative performance analysis of the transmission mode are achieved through the setting and adjustment of QoS parameters. This study can provide references for ROS2 application designers and the formal modeling, validation, and quantitative performance analysis of the distributed data distribution service based on the data flow.     

基于模型检测的系统生存性分析

提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型。通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例,利用PRISM对系统进行建模及验证,结果表明,该形式化方法可以规范并简化生存性分析过程。