【摘 要】
：
为提供更优质的使用Event-B形式化方法建模混合系统的工具,根据混合系统的时序约束建模方法,其能够很好刻画混合系统建模中的时间相关性质并且支持精化和组合,提出基于它的自动筛选、精化和组合的方法。开发对应的自动精化和组合的工具链,工具链包含模型检测、自动精化和组合、模型证明等一系列功能并拥有用户友好的界面。给出一个使用工具的案例介绍和应用此工具。
【基金项目】
：
国家自然科学基金项目(61602293)。
论文部分内容阅读
为提供更优质的使用Event-B形式化方法建模混合系统的工具,根据混合系统的时序约束建模方法,其能够很好刻画混合系统建模中的时间相关性质并且支持精化和组合,提出基于它的自动筛选、精化和组合的方法。开发对应的自动精化和组合的工具链,工具链包含模型检测、自动精化和组合、模型证明等一系列功能并拥有用户友好的界面。给出一个使用工具的案例介绍和应用此工具。
其他文献
以周负荷数据为用户用电行为分析的视角较通常使用日负荷数据更符合用户客观用电周期规律,提出一种面向用户周负荷数据聚类方法,通过改进的近邻相似度图聚类避免计算过程中维度增高导致的相似一致化,优化计算的时间与空间复杂度,实现用户用电特征准确快速提取,相较常见的K-means和DBSCAN等方法聚类效果更佳,使用逐段聚集平均降维表示,便于后续分析。以某省大工业用户用电数据作为仿真算例进行验证。
为解决传统图像拼接方法对含噪无人机(UAV)图像的拼接存在严重图像畸变的问题,提出一种基于欧拉弹性模型与加速稳健特征(SURF)算法的含噪无人机图像拼接方法。将欧拉弹性能量模型应用在无人机图像拼接的去噪预处理环节,通过SURF算法进行特征点的提取、描述与匹配,通过随机抽样一致性(RANSAC)算法进一步去除错误的特征匹配点,运用加权平均融合算法实现对含噪无人机图像的无缝拼接。实验结果表明,相比传统
需求侧管理的主要目的是允许对消费者能源需求进行控制和调度,主要是利用云进行操作,但由于物理距离和数据量大,会造成延迟问题,雾计算的出现缓解了这些问题,因此提出一种可用于能源需求调度的云-雾计算架构,实现降低智能建筑的总能源成本。主要工作包括两部分:基于分布式和博弈的需求调度方法,以及用于选择将执行此分布式方法的雾节点的模型。仿真结果表明,雾化体系结构的集成有助于在确定最佳需求计划的同时减少延迟。
为提高对发酵过程中质量变量的预测精度,解决发酵数据非线性的问题,提出一种基于核二次互信息回归的质量预测模型。将非线性过程数据核映射至高维特征空间,使其线性可分;基于高维特征空间,使用Renyi二次熵与二次互信息定义目标函数提取过程特征,建立过程特征与质量变量间的回归模型;二次互信息可衡量变量间的非线性关系。仿真实验及大肠杆菌发酵生产数据的实验结果表明,该方法具有较高质量预测精度,对非线性数据有较强处理能力。
针对由于风速变化因素复杂导致的风速预测模型准确率低的问题,提出一种多特征嵌入的Seq2Seq(序列到序列)风速预测模型。以Seq2Seq为基础,将影响风速的多种因素数据进行多特征嵌入编码,实现对未来若干个小时风速的预测。通过准确率、预测评分和平均绝对误差等指标的实验评价,验证Seq2Seq模型相比当前最优模型达到了更好的预测稳定性,风速多特征嵌入编码方法的加入显著提高了Seq2Seq模型的预测准确性。实验结果验证了该模型的有效性。
针对采用松弛-量化策略的深度哈希方法面临的二值码离散优化的难题,提出一种端到端的基于成对标签的哈希方法来学习更具有判别力的哈希码,通过优化损失函数来解决离散优化丢失信息的问题。引入锚点哈希码概念,以汉明空间中的锚点作为监督信息训练AlexNet网络,将表示图片的二值码拟合至各锚点附近,使用优化后的损失函数计算分类误差和锚点误差,使哈希函数生成具有强判别力的哈希码。在CIFOR-10数据集和Imag
为获得国家间双边关系预测的因果关系模型,提出一种融合事件抽取(event extraction,EE)、时序贡献度(time contributions,TCs)与动态贝叶斯网络(dynamic Bayesian networks,DBN)的国家双边关系预测方法。基于事件抽取技术对爬取的新闻数据抽取事件句、事件类型等要素。按月划分新闻数据,提取特征词,根据频次等计算每月的时序贡献度。基于专家制定的事件分值表与事件抽取结果构建国家双边关系数据集,将其输入融合时序贡献度的DBN模型训练结构和参数。以南海争端为
针对工业应用中的指针式仪表自动检测识别任务,为解决指针式仪表检测过程中所涉及到的小目标检测性能不足与检测速度慢的问题,提出一种改进版本的YOLOv3检测算法。使用网络爬虫及数据增强扩充数据集,通过Kmeans++初始化的Mini Batch Kmeans方法对数据集聚类得到先验框;使用轻量级网络MobileNet框架与设计的适应样本的损失函数,得到改进模型。理论分析和实验结果表明,在指针式仪表检测
针对目前基于聚类方法的交通流预测模型,在聚类时,未考虑到不同因素对交通流影响程度不同的问题,引入因果分析方法来量化各因素的重要程度,同时提出一种预测框架,基于因果分析的套索回归(LASSO)和极限学习机(ELM)组合预测模型。采用占用率和车速两种因素,引入符号转移熵分别对各因素与交通流进行因果分析;根据分析结果为每种因素加权,利用K-Means算法对数据进行聚类;通过LASSO捕捉线性关系,ELM学习非线性关系,为每一类交通流建立特有的预测模型。通过对洛杉矶地区的实验,验证了组合模型对预测精度的提升具有很
飞机油耗区间估计是航空公司系统规划和运行决策的重要依据,针对传统油耗估计中对实际业载和航程差异分散特征以及运行环境和驾驶员操作习惯等因素变化的不确定性未能充分考虑而影响整体区间估计结果的问题,提出一种基于数据偏离性和密度分布欠采样US-D-DD(under-sampling based on data deviation and density distribution)的飞机油耗区间估计方法。对于同一机型的全部航程,在考虑数据的偏离性和密度分布的同时,运用相关向量机(RVM)建立飞机油耗区间估计模型,获