为了更精确地认识与改造世界，新一代的嵌入式系统必须将计算世界与物理世界作为紧密交互的整体进行认知，实现集计算、通信与控制于一体的深度融合的理论体系与技术框架，即信息物理系统（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软件工程专委会、系统软件专委会对专题工作的指导和帮助，感谢专题全体评审专家及时、耐心、细致的评审工作，感谢踊跃投稿的所有作者.希望本专题能够对形式化方法的科研工作有所促进.
专刊特约编辑、北航计算机学院刘超教授在专刊的筹划阶段分享了大量宝贵的经验，并在征稿、审稿等环节做了大量的工作，使得专刊实施过程得以顺利开展.然而，在本专刊即将完成之际，刘超老师却因病永远离开了我们.刘老师睿智、谦逊、渊博、平和，为推动我国软件工程事业发展做出了重要贡献，我们借此表达深深的怀念和敬意.