个人简介

   陈祖希，CCF会员、IEEE会员，硕士生导师，同济大学计算机软件与理论专业博士。厦门市数据安全与区块链技术重点实验室核心成员【https://dsbt.hqu.edu.cn/sysgk/zzjg.htm】。主要研究应用于高可信轨道交通等工业领域的“信息-物理融合系统（Cyber-Physics System, CPS）”可信保障技术和多机器人路径规划（Multi-Agent Path Finding, MAPF）算法。曾于2012年至2013年，公派美国University of Colorado at Boulder，在Sriram Sankaranarayanan教授团队从事 “信息-物理融合系统”的形式化验证相关的学习和科研工作。2016年9月入职华侨大学，目前已经同卡斯柯信号有限公司【https://www.casco.com.cn  中国通号集团与法国阿尔斯通合资、国内最大的轨道交通控制系统开发商】、上海电气泰雷兹交通自动化系统有限公司【https://www.thalessec.com.cn 上海电气集团与法国泰雷兹合资】等轨道交通控制系统龙头企业和同济大学-泰雷兹“智慧轨道交通联合工程中心”等研发机构在内的多家机构建立项目合作关系，共同研究轨道交通控制系统的危害识别、安全分析和面向安全的形式化开发、验证和确认等相关技术。

本课题组经费充足，欢迎有兴趣攻读研究生的同学积极联系交流（zuxichen@hotmail.com）。课题组为参与项目研究生提供生活补贴，研究生发表的高水平论文将根据SCI分区（3区及以上）或CCF级别（期刊和A、B类会议）获得3000至10000不等的科研奖励!

2022届拟招硕士生研究方向如下（各方向均有实际项目可以参与）：

（1） 全新一代自主列车运行控制系统高可信性建模与分析；

（2） 基于多智能路径规划理论的自主列车运行路径规划算法研究；

       （3）物联网板卡（嵌入式硬件）及其云平台研发（软件）；

       （4）金融大数据或区块链的应用平台研发。

科研项目列表

[1] 基于形式化方法的高可信轨道交通控制系统验证和确认技术研究.同济-泰雷兹【智慧轨道交通联合工程中心】(泰雷兹项目联系人：设计总监-高翔).2021.12-2023.12，华侨大学课题负责人

[2] TACS系统联锁需求研究.卡斯柯信号有限公司（卡斯柯项目联系人：城轨事业部-潘亮）.2020.12-2021.12，负责形式化建模、验证工作

[3] 面向轨道交通领域的可信工业控制软件核心保障技术研究.福建省自然科学基金面上项目.2021.8-2024.8，主持

[4] 基于“故障-安全”模型的联锁安全需求形式化建模与验证技术研究.卡斯柯信号有限公司（卡斯柯项目联系人：联锁事业部经理-张程）.2020.10-2021.7.主持

[5] 基于有限状态演化模型的机电设备故障诊断系统.厦门光系智能信息科技有限公司.2020.12-2021.12,主持

[6] 基于区块链的分布式存储证明系统开发. 深圳市星际大陆科技有限公司.2021.1-2021.9,主持

[7] 基于区块链集成电路集团保税业务信息化平台开发.厦门市科技计划课题.2020.5-2021.6,主持

[8] 网络舆论智能引导仿真推演与系统建模研究.国家社会科学基金项目-一般项目.2019.7-2021.6,参与

[8] 自主可控的区块链联盟系统研发.福建省中盈数金科技有限公司. 2020.5-2021.2，参与

[9] 基于区块链集成电路集团保税业务信息化平台开发.厦门市关务通科技有限公司.2019.7-2020.7,主持

[10] 基于可判定形式理论的高铁列控软件安全性验证技术研究. 福建省教育厅中青年教师教育科研项. JAT170041.2018.6-2020.6，主持

[11] 炒菜机控制系统设计及软件研发. 厦门饭易科技有限公司.2018.8-2019.8，主持

[12] 基于认知机理的网络舆情引导智能代理研究.福建省社会科学规划项目-一般项目.2017.9-2019.9,参与

[13] 基于一阶逻辑的实时轨道交通运行控制系统安全性验证技术研究.华侨大学高层次人才科研启动项目.No:16BS708.2016.9-2020.6，主持

[14] 面向无可信实体架构的LBS隐私保护协议及其评价方案研究. 国家自然科学基金项目-青年科学基金项目. 61802134,2018.8-2021.8 参与

[15] 基于微分逻辑的轨道交通运营实时场景全符号化模型检测技术研究. 国家自然科学基金面上项目. No:61273180.2012.9-2016.9, 参与 排名第5

[16] 高速铁路信号系统安全认证和评估技术研究. 国家高技术研究发展计划(863 计划)课题.  No:2012AA112801.2012.6-2016.6, 参与 同济课题排名第6

[17] 新一代城轨交通列车运行控制系统研制. 国家“十二五”科技支撑计划项目. No:2011BAG01B03.2011-2015,参与 同济课题排名6

[18] 高速铁路列控系统安全性验证的一阶可判定形式理论研究. 国家自然科学基金面上项目. No:61075002. 2010.9-2014.9参与 排名6

[19] 生命周期过程驱动的铁路信号系统可信性综合评价体系的研究. 铁道部科技研究开发计划重点课题.  No:J2011X003.2011.9-2013.9,参与 排名第5

[20] 铁路信号系统功能需求形式化说明技术的研究. 铁道部科技研究开发计划重点课题. No:J2011X004.2011.9-2013.9,参与 排名第5

论文列表

[1] Xiangyu Luo, Sen Liang, Lixiao Zheng, Zuxi Chen(通讯作者), and Fan Yang. Incremental Witness Generation for Branching-Time Logic CTL. IEEE Transactions on Reliability,2022（SCI检索，已录用）

[2] 骆翔宇, 黄欣玥, 古天龙, 苏开乐, 陈祖希, 郑黎晓.基于正时态测试器的实时分支时态逻辑符号化模型检测.软件学报.2022.08（EI检索，已录用）

[3] Lixiao Zheng, Shuai Ma, Zuxi Chen, Xiangyu Luo. Ensuring the Correctness of Regular Expressions: A Review. International Journal of Automation and Computing. 2021.（SCI检索）

[4] Xiangyu Luo, Liang Sen, and Zuxi Chen(通讯作者). Counterexample Generation for Real-Time Branching Temporal Logic. Formal Methods and Applications FMAC 2019，(CCF形式化专委会会议)

[5] zuxi chen, etc. Optimized Step Semantics Encoding for Bounded Model Checking of Timed Automata. 2019 International Symposium on Theoretical Aspects of Software Engineering (TASE).July 2019(EI检索，CCF C类会议)

[6] 骆翔宇,许杭娜,曾昊晟,陈祖希(通讯作者),杨 帆.离散实时线性动态逻辑的符号化模型检测. 计算机科学,2019-12-24

[7] Xiangyu Luo, Lijun Wu, Qingliang Chen, Haibo Li, Lixiao Zheng, Zuxi Chen. Symbolic model checking for discrete real-time systems. SCIENCE CHINA-INFORMATION SCIENCES(中国科学), 2018.春季, 61(5) （SCI检索）

[8] Zuxi Chen, etc. Efficient encoding for bounded model checking of timed automata. IEEJ Transactions on Electrical and Electronic Engineering. Volume 10, Issue 10,  pages 83-90, May 2017 (SCI检索).

[9] Zuxi Chen, and Zhongwei Xu. Lazy abstraction for timed automaton with interpolation. IEEJ Transactions on Electrical and Electronic Engineering. Volume 10, Issue S1,  pages 102-113, October 2015 (SCI检索)

[10] 陈祖希，徐中伟，霍伟伟，俞钢. 基于craig插值的混成系统符号化模型检测.电子学报. 2014, Vol. 42 Issue (7):1338-1346(EI检索)

[11] 于丽珍, 徐中伟,陈祖希, 张舒青. 基于梯形逻辑的联锁系统形式化验证方法. 计算机应用. 2013/33:12 PP.3419-3422

[12] 张舒青, 徐中伟, 陈祖希. 基于项重写系统的联锁系统模型检测方法研究. 计算机工程与应用. 2013/33:12 PP.3419-3422

[13] Rui Ma, Zhongwei Xu, Zuxi Chen, and Shuqing Zhang. Initial State Modeling of Interlocking System Using Maude. Computer engineering and networking: Proceedings of the 2013 international conference on computer engineering and network. Heidelberg : Springer, 2013(EI 检索)

[14] 唐晨, 陈邦兴, 陈祖希, 沈啸. 基于Event-B的控制系统形式化建模方法研究. 计算机工程与应用. 2013/33:12 PP.3419-3422

[15] 夏志翔, 徐中伟, 陈祖希. UML模型形式化B方法转换的实现. 计算机应用与软件. 2011/28:11 PP. 15-20

发明专利列表

[1] 一种自动驾驶人机界面安全性验证方法及系统. 陈祖希,谭兴,骆翔宇,梅萌,徐中伟,郑黎晓,李卫娟,张程,刘晓(专利号: ZL202011640279.1,授权)；

[2] 一种蒸汽锅炉系统的安全分析方法及系统. 陈祖希,谭兴,骆翔宇,梅萌,郑黎晓,徐中伟(申请号: 2021101489814,实质审查)；

[3] 基于区块链的权限可控的物联网云平台及数据交互方法. 陈祖希,曹子昱,杜振博,缑锦; 刘杰,骆翔宇(申请号: 2020109271451,实质审查)；

[4] 一种轨道交通联锁系统的安全分析方法及系统. 骆翔宇,陈祖希,黄欣玥,梅萌,徐中伟,郑黎晓,李卫娟,张程,刘晓(专利号: ZL202011639828.3,授权)；

[5] CPU和IO设备低能耗调度方法. 张忆文,谢维波,张惠臻,刘进,陈祖希(ZL201710165505.7,授权)；

[6] 一种人脸相似性比较方法. 郭婧,刘尉,陈祖希(ZL201710165505.7,授权)；

[7] 一种智能用电权限的管理装置及方法. 郭婧,刘尉,陈祖希(ZL201710165505.7,授权)；

[8] 一种机械手臂的行为识别的数据生成以及存储系统. 郭婧,刘尉,陈祖希(申请号:201811294469.5,实质审查)；

[9] 一种铁路继电器底座锁住方法. 郭婧,刘尉,陈祖希(ZL201710165505.7,授权)；

[10] 固定优先级资源受限系统层次能耗优化方法.张忆文,王成,陈祖希,刘进(申请号:201710165339.0,公开)；

社会服务

[1]厦门长江电子科技有限公司 专业委员；

[2]厦门中软海晟信息技术有限公司 专业委员；

[3]软质通（厦门）评测技术有限公司 专业委员；

[4]福建省四川商会 顾问；

导师制毕业学生

杜振博 字节跳动科技有限公司深圳分公司；

曹子昱 IGG成都分公司;

陈  亮 杭州达西信息技术有限公司；

指导科创

杜振博、曹子昱、李永振；《智能家居服务机器人》；2020年第13届中国大学生计算机设计大赛国赛三等奖，福建赛区二等奖；

曹子昱、杜振博、李佳煜；《SupriotClou物联网平台》；2020年第13届中国大学生计算机设计大赛国赛三等奖，福建赛区二等奖；

曹子昱、杜振博、李佳煜；《基于区块链的集成电路保税业务信息化平台》；2020年第13届中国大学生计算机设计大赛福建赛区一等奖；

杜振博、靳蒙柯、阳德行；《基于ROS的全覆盖路径规划与视觉信息融合的智能移动机器人》；2019年第12届中国大学生计算机设计大赛国赛三等奖，福建赛区二等奖；

杜振博、靳蒙柯、阳德行；《基于ROS的全覆盖路径规划与视觉信息融合的智能移动机器人》；2019年大学生创新创业训练国家级立项；

陈亮、尹硕、肖妮妮、梁晓威；《基于计算机视觉的无人搬运避障小车》；2018年大学生创新创业训练省级立项；

课程教学

本科生课程：《软件安全》、《程序设计基础》；

研究生课程：《高可信软件技术》；