深度学习模型中的公平性研究

近几年深度神经网络正被广泛应用于现实决策系统,决策系统中的不公平现象会加剧社会不平等,造成社会危害.因此研究者们开始对深度学习系统的公平性展开大量研究,但大部分研究都从群体公平的角度切入,且这些缓解群体偏见的方法无法保证群体内部的公平.针对以上问题,本文定义了两种个体公平率计算方法,分别为基于输出标签的个体公平率（IFR_b）,即相似样本对在模型预测中标签相同的概率和基于输出分布的个体公平率（IFR_p）,即相似样本对的预测分布差异在阈值范围内的概率,后者是更严格的个体公平.更进一步,本文提出一种提高模型个体公平性的算法IIFR,该算法通过余弦相似度计算样本之间的差异程度,利用相似临界值筛选出满足条件的相似训练样本对,最后在训练过程中将相似训练样本对的输出差异作为个体公平损失项添加到目标函数中,惩罚模型输出差异过大的相似训练样本对,以达到提高模型个体公平性的目的.实验结果表明,IIFR算法在个体公平的提升上优于最先进的个体公平提升方法.此外IIFR算法能够在提高模型个体公平性的同时,较好地维持模型的群体公平性.     

航空机载嵌入式控制软件需求建模的形式化工程方法

嵌入式控制软件是现代航空飞行器的核心部件之一。构建软件需求的形式化规约精确地刻画人们对软件期望的功能和运行场景,是确保此类安全攸关软件质量的根本途径。在工业界,形式化需求建模的大规模应用尽管有成功的案例,但仍面临众多的困难。其根本性难点在于缺少一种系统化的工程方法来引导工业界软件实践者,从原始需求开始最终完成形式化需求规约,并能确认该规约真实、充分地反映了人们对软件期望的功能。针对上述挑战,提出了一种面向机载控制软件需求建模的形式化工程方法ACSDL-MV,以形式化方法为理论基础,结合软件需求工程的基本原理,引导工程人员从原始需求出发以演化式的过程逐步完成需求规约的构建;定制了航空控制软件的形式化描述语言ACSDL,用以构建形式化规约;为了确认软件需求规约准确、充分地描述了人们对软件期望的功能,该方法给出了基于图形的静态审查和基于模型的动态模拟技术。在航空发动机公司中的实验结果表明,该方法相比传统方法探测到了更多的潜在错误。     

一种面向CPS的自适应统计模型检测方法

随着计算机与物理环境的交互日益密切,信息物理融合系统（cyber physical systems,CPSs）在健康医疗、航空电子、智能建筑等领域有着广泛的应用前景,CPSs的正确性、可靠性分析已引起人们的广泛关注.统计模型检测（statistical model checking,SMC）技术能够对CPSs进行有效验证,并为系统的性能提供定量评估.然而,随着系统规模的日益扩大,如何提高统计模型检测技术验证CPSs的效率,是目前所面临的主要困难之一.针对此问题,本文首先对现有SMC技术进行实验分析,总结各种SMC技术的受限适用范围和性能缺陷,并针对贝叶斯区间估计算法（Bayesian Interval Estimate,BIE）在实际概率接近0.5时需要大量路径才能完成验证的缺陷,提出一种基于抽象和学习的统计模型检测方法AL-SMC.该方法采用了主成分分析、前缀树约减等技术,对仿真路径进行学习和抽象,以减少样本空间.接着,提出了一个面向CPS的自适应SMC算法框架,可根据不同的概率区间自动选择AL-SMC算法或者BIE算法,有效应对不同情况下的验证问题.最后,结合经典案例进行实验分析,实验结果表明自适应SMC算法框架能够在一定误差范围内有效提高CPSs统计模型检测的效率,为CPSs的分析验证提供了一种有效的途径.     

不确定环境下智能大厦空调系统调度策略评估

近年来,智能大厦的概念在国内外受到了高度的关注.相比于传统的建筑,智能大厦更加节能、舒适、易维护,已成为未来建筑的发展趋势.作为智能大厦空调通风系统的关键部分,空调系统及其调度策略决定了大厦整体的节能效果以及大厦中用户的舒适度.然而由于智能大厦所处的环境具有许多不确定因素,这极大增加了空调系统调度策略设计与评估的复杂程度.因此如何设计与评估不确定环境下空调系统的调度策略成为了智能大厦设计者面临的一大挑战.已有的方法主要针对智能大厦空调系统进行能耗与性能等方面的分析,但尚未有方法针对调度策略本身进行分析与评估.提出了一种基于价格时间自动机的调度策略评估框架,支持对不确定环境下的智能大厦进行精确建模与定量评估.该框架使用UPPAAL-SMC作为属性查询引擎对模型进行随机模拟运行,根据模拟结果对不同调度策略下大厦的能耗及用户的舒适度进行定量分析.实验结果表明,该方法能有效地帮助设计者进行策略的制定和选取.     

基于环境建模的物联网系统TAP规则生成方法

用户需求是物联网智能服务的根本驱动力，如IFTTT等很多物联网框架允许用户使用简单的触发-命令编程（TAP）规则进行编程，但它们描述的是设备调度程序，并不是用户服务需求.一些物联网系统提出采用面向目标的需求方法，支持服务目标的分解，但很难保证物联网不同服务间的一致性和服务部署的完整性.为了支持正确的“用户编程”并保证用户服务需求的一致性与完整性，本文提出了基于环境建模的TAP规则自动生成方法，在用户提供的服务需求基础上，根据环境模型自动推导出所需的系统行为，检测系统行为的一致性和完整性，并最终自动生成TAP规则，实现从用户服务需求到物联网设备调度的自动生成.本文构建了物联网应用场景的环境本体以建模环境，并定义了基于环境本体的服务需求的描述方法.另外，论文针对方法的准确性、效率、性能以及构建环境本体的时间开销在智能家居场景上进行了评估.结果表明，本文方法准确性、效率和性能超过可用阈值，且在需求达到一定数量后，构建环境本体花费的时间可忽略不计.     

基于通信的列车控制系统可信构造：形式化方法综述

基于通信的列车控制系统（communication based train control system,简称CBTC）已经成为世界范围内建造轨道交通信号系统的标准制式.CBTC采用更加灵活和精确的列车控制,并提供连续的安全列车间隔保证和超速防护,在很大程度上提高了轨道交通运输的效率和安全性.尽管CBTC能够精确地实施实时控制,但由于CBTC涉及计算、通信与控制这3个方面的实时协同,系统设计与实现异常复杂.由设计缺陷而导致严重的灾难、事故和损失屡见不鲜.作为一个典型的安全攸关系统,如何保证CBTC的可信构造已成为领域研发人员关注的焦点与面临的最大挑战.鉴于在软硬件领域的成功经验,形式化方法目前已被公认为是保障CBTC可信性的一种有效方案.围绕CBTC的可信构造,从其生命周期的3个重要阶段,即系统需求分析、设计建模与底层实现入手,针对CBTC在可信方面的典型特征,梳理分析了CBTC系统在可信构造方面面临的挑战、国内外研究现状和发展趋势,全面介绍了形式化方法在CBTC可信构造中扮演的角色.     

基于SHML的CPS行为建模及仿真

信息物理融合系统（cyber-physical systems，简称CPS）是深度融合了计算进程和物理进程的统一体，是集计算、通信与控制于一体的下一代智能系统，具有广阔的应用前景.CPS的行为具有混成性、随机性等特征，建模及仿真CPS的动态行为对于开发高质量的CPS系统至关重要.但是目前缺乏面向CPS的领域建模方法及建模CPS的领域建模语言，也迫切需要支持仿真CPS领域模型的仿真工具.针对以上问题，提出一种面向CPS领域的随机混成建模语言（stochastic hybrid modeling language，简称SHML）以支持建模CPS系统的行为.首先，根据CPS的领域特征定义了SHML的元模型作为其抽象语法，并定义了SHML的具体语法和操作语义；其次，基于GEMOC框架实现了SHML的可视化建模工具.此外，集成GEMOC的序列化执行引擎和Scilab的连续行为仿真引擎，实现仿真CPS的混成行为.提出了一种面向CPS领域的建模及仿真方法，设计并实现了一个集成的面向CPS行为的建模与仿真平台，为CPS的建模及仿真提供了一种有效的方法及工具支撑.     

面向安全攸关系统中小概率事件的统计模型检测

在开放运行环境中,安全攸关系统的不确定性行为有可能导致小概率事件的发生,而此类事件的可靠性指标往往很高,小概率事件一旦发生就会产生灾难性的后果,严重威胁到人们的生命、财产安全.因此,评估、预测小概率事件发生的概率,对于提高系统的可靠性具有重要意义.统计模型检测是一种基于模拟的模型验证技术,结合了系统的快速模拟及统计分析技术,能够有效提高模型检测的效率,适用于验证、评估安全攸关系统的可靠性,但其面临的挑战性问题之一是在可接受的样本数量下,使用统计模型检测技术难以预测、评估小概率事件发生的概率.因此,提出一种改进的统计模型检测框架,设计和开发基于机器学习的统计模型检测器,实现在相对较少的样本数量下预测和评估小概率事件发生的概率.结合轨道交通控制系统中避碰控制案例分析,进一步证明改进后的统计模型检测器能够有效预测和评估安全攸关系统中小概率事件发生的概率.     

基于贝叶斯网络构建RoboSim模型的自动驾驶行为决策

为汽车自动驾驶提供安全高效的自动驾驶行为决策,是汽车自动驾驶领域面临的挑战性问题之一.目前,随着自动驾驶行业的蓬勃发展,工业界与学术界提出了诸多自动驾驶行为决策方法,但由于汽车自动驾驶行为决策受环境不确定因素的影响,决策本身也要求实效性及高安全性,现有的行为决策方法难以完全支撑这些要素.针对以上问题,提出了一种基于贝叶斯网络构建RoboSim模型的自动驾驶行为决策方法.首先,基于领域本体分析自动驾驶场景元素之间的语义关系,并结合LSTM模型预测场景中动态实体的意图,进而为构建贝叶斯网络提供驾驶场景理解信息;然后,通过贝叶斯网络推理特定场景的自动驾驶行为决策,并使用RoboSim模型的状态迁移承载行为决策的动态执行过程,以减少贝叶斯网络推理的冗余操作,提高了决策生成的效率. RoboSim模型具有平台无关、能模拟仿真执行周期的特点,并支持多种形式化的验证技术.为确保行为决策的安全性,使用模型检测工具UPPAAL对RoboSim模型进行验证分析.最后,结合变道超车场景案例,进一步证实所提方法的可行性,为设计安全、高效的自动驾驶行为决策提供了一种可行的途径.     

时空轨迹数据驱动的自动驾驶场景元建模方法

时空轨迹数据驱动的汽车自动驾驶场景建模,是当前汽车自动驾驶领域中驾驶场景建模、仿真所面临的关键问题,对于提高系统的安全性具有重要研究意义.近年来,随着时空轨迹数据建模及应用研究的快速发展,时空轨迹数据应用于特定领域建模的研究引起人们的广泛关注.但由于时空轨迹数据所反映现实世界的多元性和复杂性以及时空轨迹数据的海量、异构、动态等特点,基于时空轨迹数据驱动的安全攸关场景建模的研究仍面临着挑战,包括：统一的时空轨迹数据元模型、基于时空轨迹数据的元建模方法、基于数据分析技术的时空轨迹数据处理、数据质量评价等.针对汽车自动驾驶领域的场景建模需求,我们提出一种基于MOF元建模体系构建时空轨迹数据的元建模方法,根据时空轨迹数据的特征及自动驾驶的领域知识,构建了面向汽车自动驾驶的时空轨迹数据元模型;并基于此,提出基于时空轨迹数据元建模技术体系的自动驾驶安全场景建模方法,并使用场景建模语言ADSML实例化安全场景,构建安全场景库,旨在为此类系统的安全关键场景建模提供一种可行的方案.结合变道超车场景的案例,展示了时空轨迹数据驱动的自动驾驶安全场景元建模方法的可用性,为场景模型的构建、仿真、分析奠定了基础.