公开(公告)号：CN118444667A

公开(公告)日：2024-08-06

申请号：CN202410905362.9

申请日：2024-07-08

Applicant: 华侨大学 ,  同济大学

Inventor： 张世旭 ,  陈祖希 ,  梅萌 ,  周长利 ,  缑锦 ,  潘亮 ,  汪小勇 ,  翁建辉

IPC: G05B23/02

Abstract: 本发明一种轨道交通联锁系统故障注入测试方法，涉及测试技术领域，包括：使用STPA方法对轨道交通联锁系统进行分析，识别潜在的故障场景和影响因素；使用CoFI方法将故障场景注入到轨道交通联锁系统的控制流图中，并观察轨道交通联锁系统的响应，生成有限状态机模型FSM；利用W方法从轨道交通联锁系统的有限状态机模型FSM中生成测试用例；使用测试用例测试轨道交通联锁系统在面对不同故障情况时的行为是否符合设计要求。本发明将STPA方法、CoFI方法和W方法相结合，为轨道交通联锁系统的故障注入测试提供了一种全面而有效的方法。

公开(公告)号：CN118426449A

公开(公告)日：2024-08-02

申请号：CN202410885607.6

申请日：2024-07-03

Applicant: 华侨大学

Inventor： 牛传军 ,  陈祖希 ,  梅萌 ,  徐中伟 ,  汪小勇 ,  周长利 ,  翁建辉

IPC: G05B23/02

Abstract: 本发明公开了一种安全目标导向的CBTC系统精化开发和确认方法及装置，涉及系统安全评估领域，包括：对CBTC系统进行分析，确定CBTC系统的控制结构；对控制结构进行精化分层，建模得到CBTC系统的形式化模型；采用Event‑B形式化方法对CBTC系统的形式化模型进行精化，得到Event‑B模型，通过Rodin平台中的定理证明器完成Event‑B模型进行证明，得到证明后的Event‑B模型；使用ProB工具对证明后的Event‑B模型进行动态仿真、死锁以及不变式违背检测，得到CBTC系统开发结果。本发明解决了采用基于模型检测的形式化方法进行开发会导致状态空间爆炸和无法保证构建模型正确性的问题。

公开(公告)号：CN118746976A

公开(公告)日：2024-10-08

申请号：CN202411111928.7

申请日：2024-08-14

Applicant: 华侨大学

Inventor： 张世旭 ,  陈祖希 ,  梅萌 ,  汪小勇 ,  张宏扬 ,  周长利 ,  缑锦

IPC: G05B23/02 ,  B61L19/00

Abstract: 一种轨道交通联锁系统完备性测试用例生成方法和系统，包括：应用STPA方法分析轨道交通联锁系统的安全需求，并将安全需求转换为线性时态逻辑属性；利用符号化有限状态机对轨道交通联锁系统进行建模得到参考模型，计算轨道交通联锁系统中的所有估值函数，根据估值函数生成得到参考模型中的符号迹；改良参考模型，并结合线性时态逻辑属性对参考模型的输入输出事件进行等价类划分；基于改良后的参考模型的符号迹生成测试用例，在被测系统上执行测试用例，检测被测系统是否满足轨道交通联锁系统的安全需求。本发明通过合理地划分等价类，可以有效减少测试用例的生成数量，从而缩减测试时长，提高测试效率。

公开(公告)号：CN118363368B

公开(公告)日：2024-10-01

申请号：CN202410796198.2

申请日：2024-06-20

Applicant: 华侨大学

Inventor： 陈圣彬 ,  陈祖希 ,  梅萌 ,  徐中伟 ,  缑锦 ,  汪小勇 ,  周长利 ,  翁建辉

IPC: G05B23/02 ,  B61L19/00 ,  G06F8/20

Abstract: 一种面向安全的铁路联锁系统的建模方法和系统，包括构建铁路联锁系统的初始系统理论的事故模型和过程，其包括控制结构和过程模型以及安全约束；构建铁路联锁系统的第一次增量系统理论的事故模型和过程，引入轨道区段并对控制结构和过程模型以及安全约束进行更新；构建铁联锁系统的第二次增量系统理论的事故模型和过程，将轨道区段分解为不同类型的实体并对控制结构和过程模型以及安全约束进行更新；构建铁联锁系统的第三次增量系统理论的事故模型和过程，引入信号机并对控制结构和过程模型以及安全约束进行更新得到最终的铁路联锁系统。本发明利用增量开发技术逐步构建STAMP，有效地降低了对软件密集系统分析的难度。

公开(公告)号：CN118627717A

公开(公告)日：2024-09-10

申请号：CN202411107282.5

申请日：2024-08-13

Applicant: 华侨大学

Inventor： 孙伟杰 ,  陈祖希 ,  梅萌 ,  徐中伟 ,  汪小勇 ,  潘亮 ,  张宏扬

IPC: G06Q10/047 ,  G06N3/006 ,  G06Q50/43 ,  G06F16/29 ,  B61L27/10

Abstract: 本发明公开了一种基于MDD‑SAT的轨道交通列车智能体路径规划方法，涉及路径规划技术领域，包括以下步骤：S1，对轨道交通系统进行地图建模和智能体建模；S2，分别对所有智能体进行单独的路径规划，将所有路径规划方案中最大的时间成本设置为#imgabs0#；将所有智能体的成本总和设置为#imgabs1#；初始化#imgabs2#；S3，运行#imgabs3#算法求解路径规划方案，无解则进入S4，有解则进入S5；S4，令#imgabs4#，返回S3；S5，输出路径规划方案；所述S3采用的#imgabs5#算法基于多值决策图构建命题公式，基于布尔可满足性求解命题公式，获得路径规划方案。本发明通过建模将地铁系统抽象为MAPF问题，并利用MDD‑SAT算法解决路径规划中的冲突，以找到高速铁路系统的最优路径规划解决方案。