基于关键状态的虚拟人组合任务分层规划方法

运动规划是虚拟人运动合成中的热点和难点.虚拟人通过推理决策,选定最优运动序列完成给定目标.然而现有的运动规划方法由于维数爆炸问题难以规划具有多个子任务的组合任务.为此提出一种基于关键状态的虚拟人组合任务分层规划方法.该方法分为两层:上层的层次增强学习模型在状态空间中稀疏采样并搜索某些局部任务的成功路径,将被访问频次最大的状态作为关键状态从而将组合任务分解为若干子任务;底层的增强学习模型将运动片段抽象为行为,将环境信息抽象为状态,采用试错搜索策略分而治之地规划子任务.合成运动时虚拟人只需遵循各子任务的控制策略,依次选择运动片段并顺序拼接即可.实验结果表明该算法能够生成逼真的虚拟人运动以完成组合任务,并且大大减少规划所需的计算时间和存储空间.     

语义Web服务自动组合的有色网验证模型

Web服务组合是面向服务的计算模式下应用构造的主要方式,而现有的组合方法与实施框架缺乏有效的验证机制,从而产生大量无效的组合结果.针对这一问题,提出一种具有正确性分析与验证功能的Web服务自动组合系统框架.其核心是利用有色Petri网对基于OWL-S的服务组合系统进行形式化建模,通过对组合模型的模拟执行及对其动态性能的全面分析,预测组合服务的执行结果,从而提高组合的可靠性.另外,该框架采用智能Agent技术,可有效实现组合过程的自动化.     

基于同步网的BPEL建模和验证

Web服务组合是面向服务架构的一个应用,是指将已有的Web服务组合成为新的服务。业务流程执行语言BPEL（Business Process Execution Language）是一种描述Web服务组合的语言。为了保证BPEL描述的Web服务组合的正确性,提出了分层建模和验证的思想,将BPEL流程分为逻辑层和语义层,并分别建立形式化模型和验证方法。这样不仅能保证对流程正确地建模,而且能降低建模和验证的复杂度。在逻辑层,BPEL元素映射为基于同步网的WSL_net模型。畅通性和无冗余变迁性质保证了BPEL流程基本控制流的正确性并避免了资源的浪费。语义层的建模和验证将另文给出。     

多任务执行中无人机行动联盟形成模型及算法

针对多无人机(unmanned aerial vehicle, UAV)多任务执行问题,开展基于行动联盟的任务执行策略研究。分析了无人机行动联盟形成 (UAV action coalition formation, UACF) 策略的约束条件,建立了以最小化任务完成时间为目标函数的数学模型;设计了求解该模型的分阶段贪心规划算法 (phased greedy planning algorithm, PGPA),在进行算法状态空间描述的基础上,给出了包括任务选取、无人机〖CD*2〗任务匹配和资源分发策略等在内的算法流程;最后,通过多组仿真实验,验证了算法的有效性和优越性。     

C4ISR仿真系统动态演化机制

以基于代理技术的C4ISR仿真系统为研究对象,重点研究通过基于事务的动态依赖关系确保仿真系统的一致性.首先,为保障演化系统的事务一致性,通过静态分析方法获得基于事务的动态依赖关系;然后,针对动态演化的执行,设计了一个动态配置平台来管理动态演化操作并恢复演化系统状态,在此基础上,提出了一个基于代理的C4ISR仿真系统模型,基于该模型设计的C4ISR仿真系统具备动态演化的能力;并通过项目的实施验证了所提方法的可行性和有效性.     

基于知识的仿真模型的验证方法

仿真模型的验证研究的是模型的可信度问题。由于模型验证需要关于真实系统,建模理论以及数据分析等多方面的知识,基于知识的智能化方法适合于仿真模型的自动验证。这类方法是建立在三个知识库的基础上的:存储验证相关知识的验证知识库(VKB),用于智能推理和决策的决策知识库(DKB),以及由各类验证算法所构成的验证技术库(VTB)。通过分析验证知识库的验证域,系统选择合理的验证技术和相关的验证过程。在此基础上,系统自动设计仿真实验,获得运行结果,并自动分析数据,执行验证过程,生成验证报告。此外,我们也讨论了验证相关知识的获取过程和细节。     

小样本情况下仿真模型的验证方法

根据系统的真实输出与仿真的输出结果，研究了仿真模型的验证方法，本文主要介绍小样本情况下静态数据的验证方法，动态数据的验证方法见文献[1]。当仿真试验结果为静态数据，它与真实系统的试验结果是否相匹配的验证，从数理统计的角度来讲，其实质是检验这两种试验数据是否属于同一概率分布，本文主要研究了小样本情况下指数分布和均匀分布仿真模型的验证方法。     

考虑不完美维修的定期检测与备件策略联合优化

针对退化过程服从三阶段故障过程的单部件系统提出了定期检测与备件订购策略联合优化.该策略下,根据检测时系统的状态执行不同的维修活动:当系统处于正常状态,不执行任何维修活动;若识别轻缺陷进行不完美维修并采用比例役龄回退模型描述不完美维修效果;若识别严重缺陷则更换系统.当更换系统时需考虑备件状态:若处于存货状态则立即更换,若正处于途中则到货时更换,若未订货需立即订货并在到货时刻更换.考虑所有更新事件采用更新报酬理论建立以最小化单位时间内期望成本为目标的模型,同时优化检测周期和订货点.最后,设计枚举优化算法和离散仿真算法求解模型,并在算例分析中验证模型的有效性和适用性.     

长期资产投资组合策略的演化稳定性

利用随机动力系统理论研究了金融市场长期资产投资组合策略财富占有比例的动态演化模型.其中资产价格是内生的, 每期末支付的股息或红利收益只用于消费,在财富不断再投资的过程中, 投资组合的表现由财富的市场占有比例决定.将投资策略和红利收益纳入同一自然状态中考虑其相互影响,分析了固定投资组合策略演化稳定性的充分必要条件,在自然状态服从独立同分布和Markov过程时,给出了唯一的演化稳定投资策略, 得到了一些更加直观具体的结果.进一步,利用中国股市数据,通过计算机进行数值模拟验证了演化稳定投资策略的长期效应.研究结果对证券市场投资策略选择 及探讨市场有效性提供了重要的理论依据.     

嵌套的基于时间的软件抗衰策略模型与分析

针对软件在连续运行过程中普遍发生的老化现象,提出了一种嵌套的基于时间的软件抗衰策略,在系统级恢复前先执行多次的应用级恢复。较之周期性系统级恢复,该策略降低了恢复成本;较之周期性应用级恢复,该策略避免了预测失败导致的系统失效。论文采用随机Petri网和有限自动机对策略的实施过程进行建模,计算了策略引发的停机时间和恢复成本,并与传统的软件抗衰策略的结果进行了比较。分析结果表明,嵌套的恢复有利于进一步减少恢复时间,降低恢复成本,提高系统的可靠性。     

基于CPN的智能合约交易顺序依赖漏洞的验证

智能合约的形式化验证工作主要集中在编程语言层面的漏洞研究,而交易顺序依赖作为区块链层面的漏洞更不易被检测。基于着色Petri网对智能合约中潜在的交易顺序依赖漏洞进行形式化验证。以Decode悬赏合约为对象,分析合约中潜在的漏洞,自顶向下地对合约本身及其执行环境建立着色Petri网模型,并引入攻击者模型来考虑合约遭受攻击的情况。通过运行模型以验证合约存在交易顺序依赖漏洞,最后基于Remix平台在以太坊网络中证实结论的正确性。     

基于m-best算法与rollout策略的平台任务关系优化设计方法#br#

在平台任务关系优化设计中,考虑单个任务资源分配过程中平台资源冗余度对后续任务分配的影响,分析优化设计过程的约束条件,构建了以最大任务执行精度与最小资源冗余度为综合目标函数的平台任务关系设计的问题模型,并使用基于m-best算法与rollout策略的方法对问题模型进行求解。m-best算法生成单个任务的m个平台分配方案,rollout策略用于均衡不同优先级任务之间的任务执行精度。最后,分别通过特殊算例和一般算例验证所提优化设计方法的优越性,算例的结果表明,使用该优化设计方法能够使高优先权任务的资源冗余度降低,从而使得整体任务执行精度提高。     

基于滚动优化策略的成像侦察卫星应急调度方法

针对成像侦察卫星应急调度问题进行研究, 在分析主要约束条件的基础上, 构建了多星调度问题的约束满足模型. 根据应急任务具有独立到达时刻与执行截止期需求的特点, 提出了基于滚动优化策略的调度算法. 该策略采用周期驱动与事件驱动相结合的混合驱动模式, 可将调度过程划分为一系列静态的调度区间. 通过优化各区间内任务的规划方案, 实现应急任务的动态调度. 在问题求解过程中, 将滚动优化策略与启发式算法结合, 形成了三种应急调度算法. 最后通过仿真实验, 对不同算法的调度效果进行对比, 验证了滚动优化策略的有效性.     

基于Petri网的Web服务组合模型描述和验证

Web服务及其组合的形式化描述和验证是Web服务中一个重要的研究方向.分析了基于Petri网建模的优势,给出基于Petri网的Web服务的形式化定义和描述,对Web服务组合进行建模及元素映射,给出Petri网模型生成算法并对组合服务模型的可达性、安全性、有界性与活性等特性进行验证分析.最后是对一个具体的业务流程的建模和验证分析.由分析可知,该建模方法具有一定的表达和验证Web服务组合模型的能力.     

虚拟化云中随机任务与资源调度方法

任务和资源调度方法是云系统的关键技术之一。但是,现有的研究往往忽略实时任务的高动态性和任务执行时间的随机性,使得调度方案的实际性能与期望性能相差甚远。针对以上问题,本文设计一个随机性感知的调度框架;提出一个启发式调度算法集成前摄性和反应式策略(proactive and reactive strategy, PRS)来对任务进行调度,以提高云系统保障实时任务时效性的能力;并提出3个计算资源伸缩策略来动态调整计算资源,以减少能量消耗。最后,通过实验将算法PRS的性能与其他4个算法进行比较。实验结果表明,在任务完成率和能耗方面,算法PRS的性能比已有算法提高13.85%和17.23%。     

基于改进DE算法的敏捷成像卫星前摄式调度

针对卫星资源失效或应急任务加入对敏捷成像卫星前摄式调度的影响,构建了鲁棒模型,提出了一种改进差分进化(differential evolution,DE)算法。首先,考虑卫星资源失效概率、任务执行主从窗口构建了期望收益和松弛时间指标,将这两个指标作为优化目标构建了前摄式调度鲁棒模型;然后,针对该模型的多目标优化特性,在传统DE算法的基础上,重新设计了变异、交叉和选择算子,增加了外部存档更新策略,优化了Pareto解集评价指标,提出一种多目标离散差分进化(multi-objective discrete differential evolution,MDDE)算法,并给出了算法的实现步骤;最后,仿真结果表明,与NSGA-Ⅱ算法相比,MDDE在Pareto解集评价指标上提高了10.42%左右,在求解时间上降低了9.72%左右,为敏捷成像卫星前摄式调度提供了一定的方法支撑。     

可执行能力需求模型的动作语义研究

针对目前基于能力的需求建模方法在形式化以及验证方面的不足,借鉴统一建模语言(unified modeling language, UML)动作语义,提出了可执行能力需求建模方法。该方法在能力需求建模语言的基础上,添加可执行动作语义,提出了动作语义元模型,描述了动作语义的基本内容、执行机制以及表示。最后构建了可执行能力需求模型的仿真平台,并通过案例证明了可执行能力需求建模方法不仅能精确形式化描述能力需求模型的动态行为语义,同时也实现了能力需求模型的仿真和验证。     

A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

A method using quantifier-elimination is proposed for automatically generating programinvariants/inductive assertions.Given a program,inductive assertions,hypothesized as parameterizedformulas in a theory,are associated with program locations.Parameters in inductive assertions arediscovered by generating constraints on parameters by ensuring that an inductive assertion is indeedpreserved by all execution paths leading to the associated location of the program.The method can beused to discover loop invariants-properties of variables that remain invariant at the entry of a loop.Theparameterized formula can be successively refined by considering execution paths one by one;heuristicscan be developed for determining the order in which the paths are considered.Initialization of programvariables as well as the precondition and postcondition,if available,can also be used to further refinethe hypothesized invariant.The method does not depend on the availability of the precondition andpostcondition of a program.Constraints on parameters generated in this way are solved for possiblevalues of parameters.If no solution is possible,this means that an invariant of the hypothesizedform is not likely to exist for the loop under the assumptions/approximations made to generate theassociated verification condition.Otherwise,if the parametric constraints are solvable,then undercertain conditions on methods for generating these constraints,the strongest possible invariant of thehypothesized form can be generated from most general solutions of the parametric constraints.Theapproach is illustrated using the logical languages of conjunction of polynomial equations as well asPresburger arithmetic for expressing assertions.     

任务主体二元约束下作战任务分解EVA方法

针对复杂作战任务分解中存在的随意性、不确定性问题, 综合考虑任务主体能力属性和结构特征等二元约束, 提出了一种由子任务集提取(extraction, E)、约束检验(verification, V)、子任务集调整(adjustment, A)等步骤递进循环形成的任务分解EVA方法。首先, 构建了全局任务空间, 提出基于任务匹配的子任务集提取方法; 其次, 针对任务主体能力属性和结构特征的二元约束, 建立了子任务集调整模型, 通过改进精英保留策略, 引入任务分解粒度和交叉变异概率动态调整策略, 提出了一种引进的非支配排序遗传算法-Ⅱ(improved non-dominated sorting genetic algorithm-Ⅱ, INSGA-Ⅱ)算法; 最后, 进行仿真实验, 验证了算法相较于传统多目标优化算法在解集多样性、收敛性和时间性能上的优势。研究结果表明, 所提方法能够使决策者依据任务主体实际自主调控任务分解结果, 在一定程度上克服了传统方法过度依赖主观经验, 忽略任务主体能力属性、结构特征约束的问题。     

基于Agent的项目交易治理计算模型研究

项目交易治理模式选择是关系到项目成功交付的核心问题,但鲜有研究从可计算角度分析不同项目交易治理模式对项目的微观过程及最终绩效的影响.本研究基于Agent仿真技术和交易治理相关理论,构造了项目交易治理计算模型.模型通过构造集成交易、项目任务与流程、项目组织和Agent的四元子模型,利用Agent技术实现了不同交易治理模式下Agent与任务、Agent之间行为交互的治理计算模型,可以输出项目成本、项目工期、质量风险、工作积压等实施绩效进行预测和评估.研究发现该模型不仅促进了项目交易治理的量化预测分析研究,还为项目交易治理提供了有效的决策支持.