不确定环境下hCPS系统的形式化建模与动态验证

随着科技的进步,新型复杂系统例如人机物融合系统（Human Cyber-Physical Systems,HCPS）已经与人类社会生活越来越密不可分.软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全.由于系统安全需求的增长,系统的规模和复杂度随之增加所带来的一系列问题亟待解决.因此,在不确定性环境下,构造智能、安全的人机物融合系统已经成为软件行业不可回避的挑战.环境不确定性使得人机物融合系统软件无法准确感知其所处的运行环境.感知的不确定性将导致系统的误判,从而影响系统的安全性.环境不确定性使得系统设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约.而对于安全要求较高的系统,准确的形式化规约是保证系统安全的首要条件.为了应对规约的不确定性,本文提出时空数据驱动与模型驱动相结合的建模方式,即通过使用机器学习算法,基于环境中时空数据对环境进行建模.根据安全软件的典型特征,采用动态验证的方式保证系统的安全,从而构建统一安全的理论框架.为了展示方案的可行性,本文以自动驾驶车辆与人驾驶的摩托车的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用.     

基于强化学习的温度感知多核任务调度

随着计算机中内核数量的增多,温度感知的多核任务调度算法成为计算机系统中的一个研究热点.近年来,机器学习在各个领域展现出巨大的潜力,彳艮多基于机器学习的系统温度管理研究工作应运而生.其中,强化学习因其较强的自适应性,被广泛地运用于温度感知的任务调度算法中.然而,目前基于强化学习的温度感知任务调度算法系统建模不够准确,很难...     

温度感知的Linux多核调度算法研究

多核处理器温度升高会影响芯片的稳定性和性能的发挥,硬件层面的DTM(Dynamic Thermal Management)方法以牺牲处理器性能为代价来降低功耗,提出了在一种软件层面的温度感知调度算法,它可以在线实时获取处理器性能计数器的值并计算各个执行核温度,根据各执行核的温度状况在各个核上合理分配进程,给出了温度感知的启发式方法。基于ATMI温度仿真器的仿真表明,温度感知调度算法较无温度感知的算法可以创建更均匀的功率密度图,且带MST启发式方法的温度感知调度算法能明显减少进程的迁移次数。     

基于梯形逻辑的联锁系统形式化验证方法

铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证。     

多核平台下应用程序的动态优化

动态优化是计算系统虚拟化的重要支撑技术之一。与虚拟化技术一样,多核时代的到来同样给动态优化机制的发展带来了新的机遇。通过对Dynamo、Pin、Jrpm等典型动态优化和插桩系统的分析总结出传统动态优化机制在多核平台下面临的问题与挑战,探讨了多核平台下可能的动态优化系统框架以及必须解决的关键问题。     

混成系统形式化验证

混成系统是实时嵌入式系统的一种重要子类,其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况,因此行为复杂,难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域,因此,如何对相关系统进行有效的分析与理解,从而保障系统安全运营,是一项具有重要意义的工作.常规的系统安全性分析手段,如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为,无法穷尽地检测复杂混成系统在所有可能输入下的行为,因此并不足以保证系统的安全性.区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此,其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上,针对现阶段实时嵌入式系统复杂化、网络化的特性,对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.     

一种多核系统任务调度算法动态度量方法

任务调度算法的优劣直接影响系统的功能和性能,对其进行功能验证和性能评价具有很强的现实意义。本文改进IMC构建多核系统任务调度算法的功能模型,扩展aCSL从逻辑层次上刻画任务调度算法的性能指标,并基于改进的IMC和扩展的aCSL提出了一种多核系统任务调度算法动态度量方法实现对任务调度算法的功能验证和性能评价。用例分析表明本文提出的动态度量方法能有效对任务调度算法进行功能和性能的描述和度量,为多核系统任务调度算法的正确执行提供了有力支撑。     

基于多核平台的多线程动态优化框架

动态优化是计算系统虚拟化的重要支撑技术之一.本文通过对DynamoRIO、Jrpm等单核平台上典型动态优化系统的分析,总结出传统动态优化机制在多核平台下面临的问题与挑战,据此提出一种面向多核平台的多线程动态优化框架,分析其组织结构和工作原理,并通过实验验证了该框架的可行性.     

温度系统的智能动态矩阵控制

本文对动态矩阵控制算法进行了研究，对于存在较大模型失与或干扰的系统给出了智能动态矩阵算法，即在线识别动态控制曲线，根据上升时间和超调量自动调节矩阵的预测时域长度和反馈校正系数，该算法成功地应用于具有慢时变，弱非线性的ＷＫ－Ｉ温度控制实验系统，证明其易于工业控制并行有效。     

多核系统中基于动态电压频率调节的实时节能调度研究

在实时嵌入式领域,特别是无线移动和便携式计算领域,能耗是首要考虑的因素,这也是多核处理器尚未在嵌入式领域全面展开应用的首要因素。目前针对多核系统的实时应用,基于动态电压频率调节(DVFS)的实时节能调度技术研究得较少,还有许多问题亟待解决。本文介绍了多核系统中动态电压频率调节技术,分析讨论了当前多核系统中实时调度研究进展,主要针对同构多核、异构多核、并行任务模型和弱硬实时模型等方面,深入探讨了多核系统中基于DVFS的实时节能调度。本文结合多核系统、电压频率动态调节节能和实时调度,探索了多核系统中的实时节能调度,奠定了理论和技术基础,具有重大的理论意义和现实应用价值。     

统计算法选择对统计模型检测效率的影响分析

近年来,统计模型检测技术已经得到了广泛的应用,不同的统计算法对统计模型检测的性能有所影响。主要对比不同统计算法对统计模型检测的时间开销影响,从而分析算法的适用环境。选择的统计算法包括切诺夫算法、序贯算法、智能概率估计算法、智能假设检验算法及蒙特卡罗算法。采用无线局域网协议验证和哲学家就餐问题的状态可达性验证为实例进行分析,使用PLASMA模型检测工具进行验证。实验结果表明,不同的统计算法在不同的环境中对模型检测的效率有不同的影响。序贯算法适用于状态可达性性质的验证,时间性能最优;智能假设检验算法与蒙特卡罗算法适合验证复杂模型。这一结论有助于在模型检测时对统计算法的选择,从而提高模型检测的效率。     

概率模型检测在动态能耗管理中的应用

如何平衡嵌入式设备的能耗和性能表现,成为了一个热门话题。动态能耗管理是一种在保证系统性能的基础上降低其能耗的有效方法,其关键点是如何生成有效的动态能耗管理策略。在概率模型检测技术的基础上,提出了一种生成和验证动态能耗管理策略的方法。首先对目标系统和能耗管理目标建模,然后利用PRISM-games工具进行动态能耗管理策略的合成,同时利用模型检测工具PRISM对合成的动态能耗管理策略进行验证。实验表明,该方法具备可行性和有效性。     

ARINC653实时任务可调度性验证方法

针对综合模块化航空电子系统(Integrated Modular Avionics,IMA)存在周期任务和非周期任务,以及任务间依赖关系,传统方法不能准确验证其实时任务可调度性的问题,本文提出了一种基于Stopwatch时间自动机的ARINC653实时任务可调度性验证方法,利用模型检验工具UPPAAL对IMA系统进行建...     

系统级芯片动态温度响应快速估计方法研究

针对高性能集成芯片的热管理,提出了一种动态温度的快速估计方法。该估计方法利用等价热阻网络建立芯片热电模型,在实时电路中把芯片由于外部激励和自生耗能引起的温度变化反馈到估计过程中,并采用数字滤波原理,将连续时域响应函数转化为离散时域响应函数,通过温度-功耗迭代计算可以准确高效地估计动态电路的温度变化。通过C语言程序实现了该温度估计算法,并通过实验验证了该方法能够有效地提高实时温度响应估计的准确度和实时性,适用于系统级芯片动态温度管理。     

A Stack-Slicing Algorithm for Multi-Core Model Checking

The broad availability of multi-core chips on standard desktop PCs provides strong motivation for the development of new algorithms for logic model checkers that can take advantage of the additional processing power. With a steady increase in the number of available processing cores, we would like the performance of a model checker to increase as well – ideally linearly. The new trend implies a change of focus away from cluster computers towards shared memory systems. In this paper we discuss the multi-core algorithms that are in development for the SPIN model checker.     

概率网络传播的干预策略验证

在现实生活中,疾病,病毒和火情等在人群、计算机、森林等网络中的传播可以对社会造成严重的影响,可能大规模疫情的爆发,计算机的大规模瘫痪,或者火情的急剧蔓延,其带来的损失是无法估量的。因此,设计合理的干预策略,即在网络传播线路中选取适当的个体,通过注射防疫针,安装软件补丁,分配消防人员等各种方式,对各种危害进行有效地控制,具有重要的使用价值。文章以概率网络传播模型为研究对象,然后采用时序逻辑表示出相应的干预策略目标并通过概率模型检测方法找出有效的干预策略。     

基于角色的数据仓库分级安全模型的形式化研究

数据仓库安全模型及访问控制技术随数据仓库应用的推广而变得重要。首先通过对RBAC模型(Role-Based Access Controlmodel)进行分级安全的扩展,并将模型应用到数据仓库的访问控制机制中;通过数据仓库结构模型的形式化描述,建立基于角色的数据仓库分级安全基础模型、分级安全配置模型,以及数据仓库分级安全模型的一致性检测算法。指出下一步的研究工作是分级安全策略与OLAP操作,扩展MDX查询语言,真正实现数据仓库分级安全应用体系。     

多智体系统中约简状态空间的限界模型检测算法

为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题;其次,定义PBTLK的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小.