国家自然科学基金面上项目（主持）
项目名称：基于标号Petri网的行为安全互模拟研究（No. 61572360, 2016.1-2019.12）
项目简介：安全性是网络环境下的系统（如网上银行交易系统）所关注的重要问题之一，行为安全性策略为预防网络环境下的欺诈等不法行为提供保障。不同的行为安全性策略可致使具有相同功能的两个系统具有不同的安全性，从而导致它们的行为并不等价，这也是行为安全性策略能够预防不法行为的原因所在。如何形式化刻画具有不同行为安全性策略但完成相同功能的两个系统的（不）等价性以及如何形式化比较两个不等价系统的安全性强弱是支撑这些系统开发的理论所关心的两个核心问题。我们发现经典的互模拟理论与语言等价理论不适用于所有的面向安全的系统的需要，不能回答上述问题。本项目发展经典的互模拟理论，提出基于标号Petri网的行为安全互模拟，研究面向安全的行为等价理论以及行为安全性层级体系。据我们所知，目前还没有相关工作从形式化角度去研究这些问题。因此，本项目的研究成果是对形式化方法与互模拟理论的一个有益扩充，为面向安全的系统的设计提供理论支撑。
国家自然科学基金重点项目-子课题（主持）
项目名称：人机物融合场景计算的建模理论与软件定义方法（No. 62032019, 2021.1-2025.12）
项目简介：人机物融合场景计算是人在计算系统协同下通过网络对物理环境实施监测、协调、控制和集成的新型计算模式；人机物融合场景计算系统（HCPS）是深度融合大数据、物联网、泛在计算和云计算等现代计算通信与控制技术构建的工程系统，且充分考虑人在场景中的角色、行为和作用。设计、开发、部署和运维这样的工程系统需新的科学理论和工程方法。本项目将研究建立人机物融合场景的计算模型和计算理论，并在此基础上，研究建立HCPS设计、开发、部署和运维的系统架构建模理论和方法，提出软件定义的程序设计模型和规约语言，研究HCPS系统特征和应用需求的规约、分析、验证和软件生成技术。通过研究这些理论、方法和技术，提供人机物融合场景计算各层次的抽象，为人机物融合场景泛在计算系统软件的设计提供模型基础。项目在理论、方法和技术方面的发现和成果将在灾后联合搜索救援和跨域健康紧急救护两个典型的人机物融合场景案例中应用验证。
国家自然科学基金面上项目（主持）
项目名称：基于Petri网的实时并发系统三位一体化建模与分析（No. 62172299, 2022.1-2025.12）
项目简介：实时并发系统，如实时嵌入式系统和物理信息融合系统，其正确性与可靠性至关重要，因为一旦出现错误，就可能机毁人亡。目前，对系统形式化建模与分析越来越受到学术界与工业界的重视，因为这些数学方法能够发现其他方法（如测试）难以发现的错误。但是，有些错误隐蔽性强，不仅与系统自身有关，而且与其运行支撑环境（如任务/进程调度策略）以及外部不确定环境（如环境致传感器故障及其中断服务例程）有关，仅靠系统自身模型难以发现它们。然而，目前缺少将三者综合建模分析的研究。为此，本项目将实时并发系统的运行支撑环境与外部环境中的要素综合到系统模型之中，开展基于Petri网的三位一体的行为建模研究，并基于模型，研究系统行为正确性与可靠性的时序逻辑表达与模型检测方法，开发一套建模分析的工具软件。成果将为安全攸关的实时并发系统的开发设计及其正确可靠性分析提供模型理论与方法基础。
国家自然科学基金青年基金项目（主持）
项目名称：交互式Petri网及其兼容性研究（No. 61202016, 2013.1-2015.12）
项目简介：Web服务组合与跨组织工作流在学术界与工业界得到广泛研究与应用，它们在逻辑层可以抽象为一组子系统通过消息的发送与接收进行交互协同。提出交互式Petri网（IPN）以模拟这些系统。基于IPN可达性，定义0、1、2、3级兼容性以刻画子系统间不同的协同能力。给出IPN的平凡拓展网，证明IPN的3级兼容性等价于其平凡拓展网的活和有界性,但其判定是co-NP-难的。从子系统执行逻辑、消息库所的输出以及事件的外部使能条件等三个维度，将IPN分为16个具有不同结构特征的子类，其目的是针对不同类别研究其基于网结构的兼容性判定与控制。对其中一些子类已给出判定其兼容性、活性的充要条件。在已有工作基础上继续研究：IPN的0、1、2级兼容性问题的复杂度，以及与平凡拓展网的性质（如活性、可重复性等）之间的关系；基于网结构判定其他子类兼容性的充要条件；兼容性的控制问题；基于理论成果开发IPN分析软件。
上海市曙光人才计划项目（主持）
项目名称：面向安全的交互式系统建模与分析（No. 15SG18, 2016.1-2018.12）
项目简介：图领奖获得者Robin Milner发现经典的刻画计算式行为的语言等价理论不适合刻画交互式行为，因为系统内部事件的确定性与非确定性影响系统与用户的交互、而语言等价理论不区分内部事件的确定性与非确定性，从而开创了互模拟理论。我们发现互模拟理论不适用于刻画面向安全的交互式系统的行为，因为外部不可观测的事件（如木马程序篡改数据）以及系统的安全策略影响系统与用户的交互，但互模拟理论不考虑这些影响。本项目拟利用Petri网，考虑外部事件与安全策略对系统行为的影响，开展面向安全的交互式系统的行为建模与分析方法，为面向安全的交互式系统的设计与验证提供新的理论与方法支持。
上海市“科技创新行动计划”项目－人工智能科技支撑专项（主持）
项目名称：鲁棒抗噪的多智能体强化学习理论模型与缺陷诊断方法（No. 22511105500, 2022.9-2024.8）
项目简介：深度强化学习方法在机器人控制、自动驾驶、物流调度等领域都有着广泛的应用。与深度神经网络相似，深度强化学习的决策网络也具有近似能力强、但抗噪能力弱的特点。事实上，由于传感器误差或恶意攻击的存在，带扰动的状态对诸如自动驾驶、无人机作战之类的安全敏感的应用中会造成严重的后果。本项目拟围绕多智能体强化学习算法，从鲁棒训练框架展开研究，提出一套抗噪的多智能体鲁棒训练框架与带有缺陷的随机博弈与分布式部分可观测的马尔科夫模型，在此基础上，设计具有可靠性保证的缺陷诊断方法，并且针对缺陷提出基于因果关系模型修复方法。
中央高校学科交叉预研类重大项目（主持）
项目名称：基于机器学习的网络支付行为建模与欺诈辨识方法（No. 22120190198, 2019.8-2021.7）
项目简介：我国已成为世界上最大的网络支付国家，网络支付为国家经济的发展与人民生活水平的提高提供了新的动力。然而，支付欺诈事件频发，现有的身份认证的方法与技术难以防范这些欺诈事件，因为犯罪分子已经利用木马、伪基站、撞库等技术手段获取了合法用户的身份信息，从而进行非法的购物、转账等支付交易；目前，利用机器学习与数据挖掘的方法辨识支付欺诈行为已成为研究与应用的热点。但是，现有的基于机器学习的检测模型与方法仍然面临着支付行为不确定性与机器学习算法不精准性这两大挑战。本项目在前期研究的基础上，拟从支付行为的时序特征与概念飘逸、支付行为模型的稳定性与可解释性、以及训练数据类别不均衡性等方面开展支付行为的建模与欺诈辨识方法的研究；建立一套基于循环神经网络与attention机制的特征表达与挖掘新方法，从而更加全面有效地刻画不确定性的支付行为；利用再生核希尔伯特空间等泛函理论改进卷积神经网络与迁移学习方法，以提高算法的精准性；构造一个可成长的综合系统模型，更加有效辨识支付欺诈行为。
上海工业控制系统安全创新功能型平台开放课题（主持）
项目名称：图神经网络的可解释性及其在交易欺诈辨识上的应用研究（No.TICPSH202103001-ZC, 2021.3-2022.2）
项目简介：从交易行为图的构造、交易行为模型的精准性与可解释性等方面开展交易行为的建模、辨识与解释方法的研究。基于已有的专家库知识构建交易行为异质图，从而利用行为的节点特征和结构信息刻画不确定的支付行为；结合节点级别和边级别的attention，以分层的形式得到邻居节点和边信息的最佳组合，从而提高图神经网络算法的精准性；研究与分类结果最相关的子图结构和节点特征来实现对结果的解释，为金融机构的决策提供直观的解释，提升深度学习在金融欺诈检测中的应用效果。
同济大学学科交叉联合攻关示范项目（人工智能方向重大专项，主持）
项目名称：基于强化学习和Petri网理论的多智能体软件系统设计研究（2021.8-2022.7）
项目简介：多智能体强化学习目前在游戏、推荐系统、网络优化等领域取得了大量成果，但在医疗、交通、救援等关乎国计民生的无人自主协同系统等真实场景中，还难以瞥见可以落地的相关技术。前期的研究中，本课题组完成了单智能体（单无人机目标跟踪）的虚拟环境往真实环境的迁移，但多智能体协同（多无人机协同）迁移到真实场景时，还存在两大挑战：1.多智能体强化学习算法本身的泛化性和鲁棒性较差，难以适应复杂多变的场景；2.虚拟环境中学习的协同决策模型迁移至真实的的分布式交互场景时，系统的实时性、交互协同性难以保证。针对以上两点挑战，本项目拟研究适应真实环境的多智能体强化学习算法、以及基于Petri网模型的分布式自适应软件系统的设计方法，从而提高智能软件的泛化性、鲁棒性与自主性，并构建典型应用案例，验证上述理论和方法的有效性。
航天五〇二所“高可信嵌入式软件工程技术重点实验室”开放课题（主持）
项目名称：面向C语言的嵌入式多核软件系统WCET和可调度性评估与死锁检测（No. LHCESET202201, 2023.3-2025.2）
项目简介：随着我国航天事业的快速发展，航天器软件系统的功能和复杂性日益增加，对实时嵌入式系统的性能和集成度等方面提出了更高的要求。多核嵌入式系统能够满足高性能与高集成度的需求，但同时也增加软件分析验证的难度，对软件的可信性提出了更高的挑战。在基于程序源代码的系统性能与功能分析验证时，存在三个主要的挑战：1. 如何在多核平台上保证系统行为的可预测性；2. 如何在保证多核系统调度算法正确性的基础上，保证应用的实时性；3. 源代码模型语义复杂，如何准确完成从源码到形式化模型的转换。针对以上三点挑战，本项目拟研究：从嵌入式软件系统的C程序源代码到形式化模型的转换规则、基于Petri网的实时多核嵌入式软件系统的WCET（最坏执行时间）和可调度性评估以及死锁检测方法，从而提高多核软件系统的安全性与可靠性，并通过典型案例，验证上述理论和方法的有效性。
CCF-华为胡杨林基金（主持）
项目名称：基于Petri网的RUST语程序并发安全漏洞检测（2024.1-2024.12）
