[3] 基于形式化方法的高可信轨道交通控制系统验证和确认技术研究.同济-泰雷兹【智慧轨道交通联合工程中心】(泰雷兹项目联系人:设计总监-高翔).2021.12-2023.12,华侨大学课题负责人
[4] TACS系统联锁需求研究.卡斯柯信号有限公司(卡斯柯项目联系人:城轨事业部-潘亮).2020.12-2021.12,负责形式化建模、验证工作
[5] 面向轨道交通领域的可信工业控制软件核心保障技术研究.福建省自然科学基金面上项目.2021.8-2024.8,主持
[6] 基于“故障-安全”模型的联锁安全需求形式化建模与验证技术研究.卡斯柯信号有限公司(卡斯柯项目联系人:联锁事业部经理-张程).2020.10-2021.7.主持
[7] 基于有限状态演化模型的机电设备故障诊断系统.厦门光系智能信息科技有限公司.2020.12-2021.12,主持
[8] 基于区块链的分布式存储证明系统开发. 深圳市星际大陆科技有限公司.2021.1-2021.9,主持
[9] 基于区块链集成电路集团保税业务信息化平台开发.厦门市科技计划课题.2020.5-2021.6,主持
[10] 网络舆论智能引导仿真推演与系统建模研究.国家社会科学基金项目-一般项目.2019.7-2021.6,参与
[11] 自主可控的区块链联盟系统研发.福建省中盈数金科技有限公司. 2020.5-2021.2,参与
[12] 基于区块链集成电路集团保税业务信息化平台开发.厦门市关务通科技有限公司.2019.7-2020.7,主持
[13] 基于可判定形式理论的高铁列控软件安全性验证技术研究. 福建省教育厅中青年教师教育科研项. JAT170041.2018.6-2020.6,主持
[14] 炒菜机控制系统设计及软件研发. 厦门饭易科技有限公司.2018.8-2019.8,主持
[15] 基于认知机理的网络舆情引导智能代理研究.福建省社会科学规划项目-一般项目.2017.9-2019.9,参与
[16] 基于一阶逻辑的实时轨道交通运行控制系统安全性验证技术研究.华侨大学高层次人才科研启动项目.No:16BS708.2016.9-2020.6,主持
[17] 面向无可信实体架构的LBS隐私保护协议及其评价方案研究. 国家自然科学基金项目-青年科学基金项目. 61802134,2018.8-2021.8 参与
[18] 基于微分逻辑的轨道交通运营实时场景全符号化模型检测技术研究. 国家自然科学基金面上项目. No:61273180.2012.9-2016.9, 参与 排名第5
[19] 高速铁路信号系统安全认证和评估技术研究. 国家高技术研究发展计划(863 计划)课题. No:2012AA112801.2012.6-2016.6, 参与 同济课题排名第6
[20] 新一代城轨交通列车运行控制系统研制. 国家“十二五”科技支撑计划项目. No:2011BAG01B03.2011-2015,参与 同济课题排名6
[21] 高速铁路列控系统安全性验证的一阶可判定形式理论研究. 国家自然科学基金面上项目. No:61075002. 2010.9-2014.9参与 排名6
[22] 生命周期过程驱动的铁路信号系统可信性综合评价体系的研究. 铁道部科技研究开发计划重点课题. No:J2011X003.2011.9-2013.9,参与 排名第5
[23] 铁路信号系统功能需求形式化说明技术的研究. 铁道部科技研究开发计划重点课题. 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] 一种蒸汽锅炉系统的安全分析方法及系统. 陈祖希,谭兴,骆翔宇,梅萌,郑黎晓,徐中伟(ZL202011639828.3,授权);
[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年大学生创新创业训练省级立项;
课程教学
本科生课程:《软件安全》、《程序设计基础》;
研究生课程:《高可信软件技术》;