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

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

信息物理系统软件设计自动化专题前言

为了更精确地认识与改造世界，新一代的嵌入式系统必须将计算世界与物理世界作为紧密交互的整体进行认知，实现集计算、通信与控制于一体的深度融合的理论体系与技术框架，即信息物理系统（cyber-physical systems，简称CPS）.与传统嵌入式系统不同，CPS充分考虑了计算部件与物理环境的深度融合，通过将设备智能化连接，实现物理环境系统与计算系统之间精确感知与高效协同.基于CPS理念设计出来的计算设备可以根据具体任务需求自适应地调整与配置计算逻辑，精确智能地获取外部物理环境信息并做出针对性的实时反应，完成安全可靠的控制服务，从而实现物理世界与信息世界的有机统一.
随着人们对信息技术质量要求的不断提高，CPS迅速在众多安全攸关领域得以部署承担关键任务.从远程精准医疗到智能轨道交通，从无人驾驶到航空航天，从智慧城市到智能制造，无处不见CPS的身影.虽然CPS在众多领域获得成功，然而由于其涉及多维时空约束、异构物理/计算进程交互、运行环境不确定等因素，CPS设计复杂度极高.在缺乏设计自动化方法与技术的情况下，CPS开发周期长且质量难于保证.日益复杂的CPS设计与实现在给产业界与学术界带来巨大挑战的同时，也创造了大量新的机遇，CPS设计自动化目前已成为国际相关研究领域的关注与研究热点.
本专题采取自由投稿的方式，共收到14篇投稿.特约编辑邀请了30余位领域专家参与审稿，每篇稿件至少邀请3位专家进行评审，每篇录用稿件都经过至少3轮审稿.14篇稿件中共计10篇稿件通过第1轮评审，8篇稿件通过第2轮评审，并在CCF软件工程专业委员会、系统软件专业委员会年会全国软件与应用学术会议NASAC2019会议上进行了报告.经过第3轮终审及少数稿件的第4轮复审后，最终有6篇论文入选本专题.
《基于SHML的CPS行为建模及仿真》提出了一种面向CPS领域的建模及仿真方法，设计并实现了一个集成的面向CPS行为的建模与仿真平台，为CPS的建模及仿真提供了一种有效的方法及工具支撑.
《垂悬指针检测与防御方法》针对复杂系统软件中广泛出现的悬垂指针问题进行研究，提出了一种名为DangDone的垂悬指针防御方法，通过在编译时的程序转换来定位潜在的垂悬指针并防御use-after-free或double-free漏洞.
《自主机器人多智能体软件架构及伴随行为机制》提出了基于多智能体的自主机器人控制软件软件架构，以及基于相应架构的伴随行为机制.该工作基于分步规划和动态决策的思想设计并实现了相应自主决策算法DAAB，并在相应仿真环境和实际机器人环境上进行了案例分析.
《轨道交通联锁领域特定语言的形式化》基于轨道交通联锁系统中故障的随机性和行为实时性的特点，提出了基于建立随机混成系统模型来仿真、预测轨道交通连锁系统的方法.该方法在实际联锁系统进行实例研究，并在UPPAAL-SMC平台上进行了事故模型的预测分析.
《基于AADL的失效概率分配及安全性评估方法》综合考虑AADL架构的层次化设计、模型复杂度和构件失效造成影响的严重程度，针对安全关键系统提出基于AADL的失效概率分配方法，以应对安全性评估过程中如何分配失效概率的问题.相关技术在飞控CPS系统上进行了实例研究.
《马尔可夫信息物理系统拒绝服务攻击安全控制》研究了马尔可夫跳变信息物理系统在模态依赖拒绝服务（DoS）攻击下的安全控制问题.提出了一种新颖的模态依赖事件触发策略来减少网络资源消耗.
本专题面向信息物理系统的研究人员和工程人员，内容涵盖系统建模、系统架构、可信保障等领域，反映了我国学者在相关领域的高水平研究成果.感谢《软件学报》编委会、CCF软件工程专委会、系统软件专委会对专题工作的指导和帮助，感谢专题全体评审专家及时、耐心、细致的评审工作，感谢踊跃投稿的所有作者.希望本专题能够对形式化方法的科研工作有所促进.
专刊特约编辑、北航计算机学院刘超教授在专刊的筹划阶段分享了大量宝贵的经验，并在征稿、审稿等环节做了大量的工作，使得专刊实施过程得以顺利开展.然而，在本专刊即将完成之际，刘超老师却因病永远离开了我们.刘老师睿智、谦逊、渊博、平和，为推动我国软件工程事业发展做出了重要贡献，我们借此表达深深的怀念和敬意.
     

UML行为图驱动的Java程序运行时验证工具

UML是一种标准的可视化建模工具，广泛应用于软件系统的描述、可视化、构建和建立文档。本文介绍了一种UMI。行为图驱动的Java程序运行时验证工具。该工具以一个随机的测试用例集作为输入，运行经过插装的被测Java程序，得到一组用于验证的程序运行轨迹。通过对程序运行轨迹和UML行为图中合法的事件序列的比较，该工具可以对程序的动态行为规约进行检查。本文描述了该工具的设计思想、算法和实现技术，并通过对实例研究对该工具的可用性和有效性进行了讨论。     

时间自动机可达性分析中的状态空间约减技术综述

时间自动机是检验实时系统建模的有效工具，其可达性分析可以检验系统是否可能达到某些特定的状态，其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量，时间自动机的可达性分析算法会产生大量的中间状态，需要巨大的存储空间，往往超出了计算机能力的极限，导致分析和检验不能完成。这就是所谓的“状态空间爆炸”。研究人员设计了很多种优化技术来约减可迭性分析所需的存储空间，以解决或者缓解这个问题。本文首先介绍了时间自动机及其可达性分析的基本概念，然后分类讨论了现有的空间约减优化技术并对此做出总结，最后提出了一些未来的研究方向。     

二级C语言理论基础讲评

随着计算机技术的发展，程序设计语言更新换代也加快了步伐。c作为一门优秀实用的语言，在计算机潮流中一直非常强劲。     

前言

<正>随着与物联网、人工智能、云计算等新一代信息技术的持续融合，嵌入式系统与物理世界交互日益频繁，其时间敏感特征越发明显，成为了典型的时间敏感系统.由于在此类系统运行过程中些许违反时间约束将会导致系统运行的错误甚至引发灾难性的后果，因此亟需相关的方法与技术保证时间敏感系统在计算、控制与通信等方面的实时性与确定性.我们组织本次“时间敏感嵌入式软件与系统”专题，邀请领域专家对新型体系架构以及边缘协同计算架构下的时间敏感嵌入式软件与系统开展综述与进展报告，旨在增强并推动国内同行在时间敏感嵌入式软件与系统方面的交流.