在项目资助期间，本人最有感触且深感自豪的一项成就是成功将本人在信息物理融合系统（Cyber-Physical System, CPS）领域的一项研究成果，成功应用于列控这一安全攸关领域的实际系统上。

与简单嵌入式系统的运行不同，CPS系统的运行是一个开放、不确定的过程。系统的运行过程中需要时刻监测外界环境的变化，接收外界信号的激励，并适应性地根据外界的变化来动态调整系统的策略与控制逻辑。在此动态、开放、不确定的环境下，现有建模与验证工作难以胜任。

针对此问题，本人提出了一种基于带参混成系统的CPS动态建模与在线验证框架。通过实时捕获系统运行时参数，对带参模型进行实例化来构建在此运行参数取值指导下的系统短期内可预测行为模型。通过对此短期行为模型进行实时、在线验证来判断系统短期内可靠性，将不可验证长期不确定行为转为多阶段可验证短期行为。

在提出该方法框架之后，本人所在研究组在实际案例研究上进行了努力的探索与尝试。列车控制是该领域最典型的应用场景之一。现代化列控系统是一种典型的CPS系统，其运行已经是一个全面信息化、自动化的过程。列车在运行中高频获取当前环境参数，并基于相关参数，快速计算并设定短期内的控制参数。而在此过程中，一旦计算所得参数有误，后果不堪设想。而在列控系统国产化的大趋势下，如何保证我国自产的系统正确性尤为重要。

幸运的是，由于本人所在研究组长期以来在形式化验证方向的积累与声誉，列控系统的专家主动找到了我们进行合作。借此机会，我们开始了将在线验证这一思路在列控系统上进行实例研究的努力。

研究成果从论文到落地永远不是一个轻松的过程。在项目开展过程中，我们逐步发现研究成果中过于简化的假设，缺乏考虑的环节等细节问题，并一步步进行思考、完善，提出了流水线式在线验证、提前预警式控制、增量式计算、面向场景验证等系列学术成果，使得我们的在线验证技术愈发成熟。

同时，我们也深入第一线与工程师交流，一轮接一轮地修改系统模型，以期与实际系统相符。在近一年时间，十多轮迭代之后，我们终于得到了工程师的首肯，认为我们的模型与其实际控制代码逻辑已经完全一致。而为了处理如此细节且复杂的模型，又进一步促进我们在混成系统模型检验算法与工具上进一步研究以支持相关模型。最终我们的最新系统成功与列控国家工程中心的半实物仿真平台对接，快速发现对方工程师植入的危险场景，并控制列车安全停车，而我们在那一霎那也感到了一切付出的意义。

这一工作让我们深刻理解了理论研究与实际应用的距离，也更让我们意识到了从应用中发现问题，在应用中解决问题的意义所在。我们将进一步在相关方向上努力，在理论算法和系统应用上做出实际、具体且有意义的工作！

卜磊，南京大学副教授，主要研究领域软件工程与形式化方法, 侧重于基于模型检验的形式化验证技术, 涉及实时、混成和信息物理融合等复杂系统。CCF系统软件专委委员、CCF形式化方法专业组委员、CCF青工委预备委员。入选2015-2017CCF青年人才发展计划。