面向复杂行为场景的实时和混成系统模型检验技术研究

It is very important and necessary to prove that the real time and hybrid system in the safety critical area is able to meet the requirements and get rid of the defects by model checking technique. However, in practice, the complexity of such systems always go beyond the limitation of the existing techniques and tools, and thus difficult to prove thoroughly. Therefore, it is very important to control the complexity of the verification and conduct the model checking of the typical complex behavioral scenario instead...By investigation of the typical real time and hybrid systems, we can find the increasing of the complexity of their behavioral scenarios mainly comes from the following directions. First, it is quite a common scene to see different components collaborate with each other to achieve certain targets in the-state-of-the-art systems. Therefore, the tangled parallel behavior is widely appeared. Second, with the increasing of the accuracy of the control level, it is a clear trend that the usage of nonlinear control functions is becoming very common and introduces nonlinear state space that is difficult to solve. Last but not least, when the system is open to the environment, the underterminisitc of the system’s behavior is rising up as an important issue. According to the above aspects, this project will conduct the research around the following topics. First, MUSS-guided quick traverse of the tangled parallel scenario; second, quick solving of the nonlinear behavioral scenario under tolerable error; third, full coverage targeted online verification of the dynamic behavior. We will make breakthrough in the above directions. In this case, we can control the complexity of the verification and propose a set of efficient technologies and tool prototypes, which can handle the requirements of the industrial systems.

针对安全攸关应用领域中的实时和混成系统，采用模型检验技术验证其是否满足需求、摆脱缺陷十分重要和必要。然而实际应用中，这类系统的复杂性常常超出现有模型检验技术和工具的能力范围，难以全局验证。因此如何有效控制验证中的复杂性、对系统的重要行为场景进行验证成为亟待解决的重要问题。.通过对典型实时和混成系统的分析可以发现，其行为场景中的复杂性主要体现为：随着系统组件间协同成为常态，组件交互带来的交织与并发行为大量出现；随着系统控制精确程度的不断提升，大量非线性控制方程的引入导致系统行为空间难以求解；随着系统与外界交互愈发密切，动态环境带来的系统行为不确定性也迅速突显。本项目针对上述复杂性导致的问题，采用基于反例子路径定位的组合场景高效遍历、可容忍误差下的非线性场景快速求解、以及全周期覆盖的动态场景在线验证等方法进行研究，力争控制验证过程中的复杂性，设计高效算法，并研制可适应工业界应用需求的工具原型。

面向实施混成系统形式化验证的复杂度挑战，本项目从组合交互，非线性运算，不确定环境等复杂度角度进行研究，提出了基于组合IIS路径定位的混成自动机验证方法，基于带参混成自动机建模语言的面向场景增量式在线验证技术，基于无梯度优化的复杂非线性行为高效符号执行，面向事件驱动IoT的模型、规约、验证与修复一体化验证框架等技术。.项目研究达到了预期的目标，已发表高质量学术论文30 篇，包括期刊论文 8 篇(分别发表在IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems、IEEE Transactions on Computer、ACM Transactions on Cyber-Physical Systems、中国科学、软件学报等国内外重要期刊上)、以及ICSE、DATE、ISSTA、ICRA、SPIN等国际会议论文22篇。.在上述研究结果的基础上，课题组研发了一批工具原型，累计获得授权中国发明专利7件，受理发明专利 6 件，研发了包括混成自动机验证工具BACH、HAT、事件驱动物联网验证工具MenShen、嵌入式代码验证工具BRICK、复杂代码符号执行工具MLB等系列工具。在列控、航天等领域进行应用实践，引起广泛关注。.项目执行期间，培养了博士生 3 人、硕士生 8 人，其中解定宝获得中国计算机学会2017年度优秀博士论文，邢少鹏获得中国计算机学会2018年度优秀大学生奖。项目负责人卜磊于2016年入选中国计算机学会青年人才发展计划，获2016年度Microsoft Research Asia Collaborative Research Award，2019年度NASAC青年软件创新奖。