区域控制器的安全需求建模与自动验证

轨道交通区域控制器（ZC）是我国轨道交通信号系统选型的主流制式——基于通信的列车控制系统（CBTC）的核心子系统，其突出的安全性使得安全需求的形式化验证成为一个非常重要的问题.但是ZC自身的复杂性以及领域知识的繁杂难以掌握，使得形式化方法很难应用到安全需求的验证中去.针对这些问题，提出一种安全需求的自动验证方法，使用半形式化的问题框架方法（PF）来建模和分解安全需求，根据需求模型自动生成安全需求的验证模型和验证性质，在此基础上自动生成验证模型的Scade语言实现，并通过Design Verifier验证器对需求进行组合验证.最后，使用了某个实际案例ZC的一个子问题CAL_EOA进行了研究，实验结果证明了该方法的可行性与有效性，它能自动地将安全需求模型进行组合验证，改善了验证的效率.     

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

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

基于GPU平台的有效字典压缩与解压缩技术

压缩技术被广泛应用于数据存储和传输中,然而由于其内在的串行特性,大多数已有的基于字典的压缩与解压缩算法被设计在CPU上串行执行。为了探究使用图形处理器（graphic processing unit,GPU）对压缩与解压缩过程潜在性能的提升,结合合并内存访问与并行组装的技术,基于CUDA（compute unified device archi-tecture）平台研究了两种并行压缩与解压缩方法：基于字典的无状态压缩和基于字典的LZW压缩。实验结果表明,与传统的单核实现比较,所提方法能够显著改善已有的基于字典的串行压缩与解压缩算法的性能。     

利用特征融合和整体多样性提升单模型鲁棒性

使用深度神经网络处理物联网设备的急剧增加产生的海量图像数据是大势所趋.但由于深度神经网络对于对抗样本的脆弱性,它容易受到攻击而危及物联网的安全,所以如何提高模型的鲁棒性就成了一个非常重要的课题.通常情况下组合模型的防御表现要优于单模型防御方法,但物联网设备有限的计算能力使得组合模型难以应用.为此本文提出一种在单模型上实现组合模型防御效果的模型改造及训练方法：在基础模型上添加额外的分支;使用特征金字塔对分支进行特征融合;引入整体多样性计算辅助训练.通过在MNIST和CIFAR-10这两个图像分类领域最常用的数据集上的实验表明,本方法能够显著提高模型的鲁棒性,在FGSM等四种基于梯度的攻击下的分类正确率有5倍以上提高,在JSMA、C&W以及EAD攻击下的分类正确率可达到原模型的10倍,同时不干扰模型对干净样本的分类精度,也可与对抗训练方法联合使用获得更好的防御效果.     

一种动态消减时间自动机可达性搜索空间的方法

时间自动机的可达性分析算法通常采用对符号状态的枚举来遍历其状态空间。符号状态由位置与时间区域组成，时间区域用形如x-y≤（〈）n的原子公式的合取式来表示。在对时间自动机进行可达性分析的过程中，分析算法将生成大量的符号状态，往往导致对计算机内存的需求超出了可行的范围。本文给出了一个消减符号状态个数的方法。该方法通过对符号状态间的依赖关系进行分析，在不影响分析结果的前提下消去某些时间区域的原子公式，从而扩展符号状态。扩展后的符号状态包含有更加多的其它的状态，通过删除掉那些被包含的符号状态可以减少算法存储的状态个数，节省存储空间。本文最后给出了相关的案例分析，结果表明这个算法有效地减少了某些时间自动机可达性分析过程中所需的存储空间。     

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

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

面向优先车辆感知的交通灯优化控制方法

智慧交通灯控制能够有效地改善道路交通的秩序和效率.在城市交通网络中,具有紧急任务的特殊车辆对于通行效率的要求更高.目前已有的智慧交通灯控制算法通常对路网中的所有车辆一视同仁,没有考虑到特殊车辆的优先性,而传统的控制特殊车辆优先通行的方法基本上都是采用信号抢占的方式,对普通车辆的通行干扰过大.为此,本文提出了一种面向优先车辆感知的交通灯优化控制方法,通过与道路环境的不断交互来学习交通灯控制策略,在设置状态和奖励函数时增加特殊车辆的权重,并利用Double DQN和Dueling DQN来提升模型表现,最终在城市交通模拟器SUMO中进行仿真实验.在训练趋于稳定之后,与固定时长控制方法的对比实验结果显示,本文方法能够将特殊车辆与普通车辆的平均等待时间分别缩短68%与22%左右,与不考虑优先级的方法相比,特殊车辆的平均等待时间也有35%左右的优化,验证了本文方法能够在提高车辆的通行效率的同时体现出对特殊车辆的优先处理.同时实验也表明本文方法能够扩展应用于多路口场景中.     

泛在嵌入式智能系统专题前言

目前,世界范围的科技革命和产业变革正在孕育兴起,一些重要科学问题和关键核心技术正在呈现革命性的突破先兆.同时,“万物智联”时代正在加速到来,IOT/CPS、AIOT 等蓬勃发展,以泛在感知、泛在互联、泛在智能为特征的各类智慧系统,以嵌入式系统为基础,与大数据、区块链、云计算呈现融合发展趋势.随着人工智能技术和嵌入式AI 芯片技术的发展,人工智能已经开始逐步向嵌入式系统迁移,尤其是伴随着机器人、无人机、无人车等智能设备的技术成熟,越来越多的应用系统需要在以边缘计算为主的嵌入式系统上实现.目前,嵌入式系统应用前景愈发广阔,如5G 通信、智能制造、智能电网、智能交通、国防军事、航空航天、智能网联汽车、数字医疗设备、机器人、智慧家庭、智能建筑等产业的创新发展都与嵌入式系统的技术发展息息相关. 本专题采取定向邀请和自由投稿相结合的方式,共收到 9 篇投稿,其中 8 篇通过了形式审查.特约编辑邀请了13 位领域专家参与审稿,每篇稿件至少邀请2 位专家进行评审,每篇稿件都经过2 轮审稿.共计6 篇稿件通过第1 轮评审,并在CCF 形式化方法专委会年度会议上进行了报告.经过第2 轮终审,最终有6 篇论文入选本专题.