公开(公告)号：CN118445816A

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

申请号：CN202410902984.6

申请日：2024-07-08

Applicant: 华侨大学 ,  同济大学

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

IPC: G06F21/57 ,  B61L19/00

Abstract: 本发明公开了一种面向安全关键系统的可信开发与验证方法及装置，涉及系统安全分析领域，该方法采用STPA和Event‑B方法协同分析，并结合逐步迭代的过程。首先确立系统任务和安全约束，在初始阶段，根据初始功能需求构建初始的STAMP模型，对初始的STAMP模型中的初始的控制结构进行STPA分析，以识别安全约束，通过Event‑B方法验证以确保安全关键系统符合安全约束。随后的每个迭代阶段的步骤逐渐引入更多的新增功能需求和具体内容，确保和现有安全关键系统的兼容性，并遵循系统级安全约束，解决现有的Event‑B方法因缺乏指导方针而难以有效组织精化步骤。

公开(公告)号：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系统开发结果。本发明解决了采用基于模型检测的形式化方法进行开发会导致状态空间爆炸和无法保证构建模型正确性的问题。