位置：艺考-上海本科院校-上海科技大学-微高校-院校号-上海科技大学-上科大江智浩团队研究成果让智能辅助软件更“懂”你

上科大江智浩团队研究成果让智能辅助软件更“懂”你

上海科技大学

2022/1/31

上海科技大学

随着计算机科学的进步，智能软件拥有了在复杂环境中自主做出决策的能力，可在减轻人类专家负担的同时提升工作效率。但在医疗、交通等领域，由于问题的复杂性以及对安全的重视，智能软件还无法完全取代人类专家。在上述领域中的智能软件应保证人-机-物的三元融合，即领域专家（人）在智能软件（机）的辅助下解决复杂问题（物）。智能软件如何利用其严谨性以及高算力承担人类专家不擅长的工作，并为领域专家提供具有可解释性的辅助是人-机-物三元融合系统的核心问题。上科大信息学院江智浩团队利用形式化方法保证智能软件的正确性，并使用数字孪生技术集成领域知识，保证辅助的可解释性，在智慧医疗、软件工程等应用领域取得多项成果。

形式化工具降低交叉领域软件验证门槛

嵌入式软件的开发属于计算机领域与应用领域的交叉领域，如何让应用领域专家在缺乏计算机专业知识的情况下参与嵌入式软件开发是一项重大的难题。模型验证方法可在软件开发早期对系统在不同环境状况下的正确性进行形式化验证，并通过提供反例的方式为软件改进提供依据。在模型验证中，系统所处的环境状况由环境模型表示，该模型需要覆盖所有可能的环境状况，并在存在反例时保证反例的可解释性。开发满足以上条件的环境模型需要同时具备应用领域以及形式化方法两个领域的知识，极大地限制了模型验证方法在软件开发中的应用。

江智浩团队提出了一种领域无关的环境建模范式，并基于此范式开发抽象树工具，将环境模型的形式化抽象与细化过程对用户隐藏，使得应用领域专家（人）可在缺乏计算机专业知识的情况下利用抽象树工具（机）进行软件验证（物），在保证环境模型覆盖度的同时得到具有可解释性的反例。该成果极大地降低了模型验证方法在嵌入式软件开发过程中的应用门槛，可尽早为嵌入式软件提供正确性保障。该成果以“Environment Modeling During Model Checking of Cyber-Physical Systems”为题在IEEE Computer作为封面文章发表。

上海科技大学

上海科技大学是论文唯一完成单位，信息学院2020级硕士研究生陈光耀为第一作者，信息学院助理教授江智浩为通讯作者。

上海科技大学

图 |（1）应用领域的专家提供常见环境状况模型；（2）利用领域无关的抽象规则提升环境模型覆盖度，建立抽象树；（3）如有反例产生，则沿抽象树对环境模型进行细化，为反例提供可解释性；（4）领域专家可根据反例补充环境模型。

数字孪生技术提升诊断效率

在医疗领域，对病人状况的诊断与评估主要依赖医生的经验，在面对不确定性很高的复杂状况时无法保证诊断的严谨性与准确性。如何开发智能辅助系统，在保证诊断过程严谨性的同时为医生提供具有可解释的诊断辅助成为一大难题。在传统心脏射频消融手术中，医生通过放置于心脏内的导管电极观测心脏内电信号的产生与传导，并对病人的心脏状况进行诊断。由于观测有限，在诊断过程中可能存在多种可解释历史观测的疑似心脏状况。医生需要“脑补”所有疑似心脏状况，并通过对病人心脏进行电刺激来排除部分疑似心脏状况，最终得到准确的诊断。诊断过程的准确性与耗时取决于医生的经验，不利于射频消融手术的普及。

江智浩团队开发出基于模型的心脏射频消融手术辅助系统，使用心脏电生理模型建立病人数字孪生，枚举诊断过程中的疑似心脏状况，为诊断结果提供可解释性，并利用形式化方法保证诊断过程的严谨性。该辅助系统在手术过程中承担计算机更擅长的枚举与推理任务，并将推理结果以符合医生专业知识的形式进行呈现，使医生（人）在该辅助系统（机）的帮助下对病人的心脏状况进行准确诊断（物），可有效地减轻医生的推理负担，推动射频消融手术的普及。该成果以“Model-based Clinical Assist System for Cardiac Ablation”为题发表于Proceedings of the ACM/IEEE 12th International Conference on Cyber-Physical Systems (ICCPS '21)并获最佳论文提名；同时以“基于模型的射频消融手术辅助系统”为题获得中国发明专利。

此项论文由上海科技大学与美国卡内基梅隆大学合作完成，上海科技大学作为第一完成单位，信息学院2018级硕士研究生吴雨桐为第一作者，信息学院助理教授江智浩为通讯作者。

上海科技大学