安全目标导向的CBTC系统精化开发和确认方法及装置

    公开(公告)号:CN118426449B

    公开(公告)日:2024-09-06

    申请号:CN202410885607.6

    申请日:2024-07-03

    Applicant: 华侨大学

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

    一种面向安全的铁路联锁系统的建模方法和系统

    公开(公告)号:CN118363368A

    公开(公告)日:2024-07-19

    申请号:CN202410796198.2

    申请日:2024-06-20

    Applicant: 华侨大学

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

    基于增量MAPF的轨道交通路径规划方法及相关装置

    公开(公告)号:CN118387169A

    公开(公告)日:2024-07-26

    申请号:CN202410813361.1

    申请日:2024-06-24

    Abstract: 本发明公开一种基于增量MAPF的轨道交通路径规划方法及相关装置,涉及轨道交通路径规划领域,方法包括:先根据各轨道交通列车的当前路径方案构造冲突树,在根节点中各轨道交通列车的当前路径方案之间存在冲突时,更新冲突树并确定出一当前最佳节点;在交通环境发生变化时,根据当前交通环境和当前最佳节点,判断当前交通环境是否导致当前最佳节点中的路径方案存在冲突,在确定产生冲突时,根据当前交通环境和当前最佳节点,再次更新冲突树并确定出一当前最佳节点,当前最佳节点中各轨道交通列车的当前路径方案适用于变化后的交通环境中,可用于控制各轨道交通列车的运行。本发明方案适用于复杂且动态多变的轨道交通场景。

    一种面向安全的铁路联锁系统的建模方法和系统

    公开(公告)号:CN118363368B

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

    申请号:CN202410796198.2

    申请日:2024-06-20

    Applicant: 华侨大学

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

    基于增量MAPF的轨道交通路径规划方法及相关装置

    公开(公告)号:CN118387169B

    公开(公告)日:2024-09-24

    申请号:CN202410813361.1

    申请日:2024-06-24

    Abstract: 本发明公开一种基于增量MAPF的轨道交通路径规划方法及相关装置,涉及轨道交通路径规划领域,方法包括:先根据各轨道交通列车的当前路径方案构造冲突树,在根节点中各轨道交通列车的当前路径方案之间存在冲突时,更新冲突树并确定出一当前最佳节点;在交通环境发生变化时,根据当前交通环境和当前最佳节点,判断当前交通环境是否导致当前最佳节点中的路径方案存在冲突,在确定产生冲突时,根据当前交通环境和当前最佳节点,再次更新冲突树并确定出一当前最佳节点,当前最佳节点中各轨道交通列车的当前路径方案适用于变化后的交通环境中,可用于控制各轨道交通列车的运行。本发明方案适用于复杂且动态多变的轨道交通场景。

    面向安全关键系统的可信开发与验证方法及装置

    公开(公告)号:CN118445816B

    公开(公告)日:2024-09-13

    申请号:CN202410902984.6

    申请日:2024-07-08

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

    一种轨道交通联锁系统故障注入测试方法

    公开(公告)号:CN118444667B

    公开(公告)日:2024-10-22

    申请号:CN202410905362.9

    申请日:2024-07-08

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

    面向安全需求的轨道交通联锁系统一致性测试方法及装置

    公开(公告)号:CN118427841B

    公开(公告)日:2024-10-22

    申请号:CN202410886462.1

    申请日:2024-07-03

    Applicant: 华侨大学

    Abstract: 本发明公开了一种面向安全需求的轨道交通联锁系统一致性测试方法及装置,涉及软件测试领域,包括:采用STPA技术对轨道交通联锁系统进行分析,得到精炼的软件安全要求并转换为线性时态逻辑属性,并得到原子命题集;采用符号化有限状态机对轨道交通联锁系统进行建模,得到参考模型;计算轨道交通联锁系统中的所有估值函数,根据估值函数生成得到符号迹及其对应的具体迹;对参考模型进行改良,得到改良后的参考模型,将估值函数映射到原子命题集中,得到命题抽象;基于参考模型的符号迹和命题抽象生成测试用例,在改良后的参考模型上执行测试用例,直至测试用例满足精炼的软件安全要求,解决了轨道联通联锁系统的一致性测试无法面向其安全需求的问题。

    面向安全需求的轨道交通联锁系统一致性测试方法及装置

    公开(公告)号:CN118427841A

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

    申请号:CN202410886462.1

    申请日:2024-07-03

    Applicant: 华侨大学

    Abstract: 本发明公开了一种面向安全需求的轨道交通联锁系统一致性测试方法及装置,涉及软件测试领域,包括:采用STPA技术对轨道交通联锁系统进行分析,得到精炼的软件安全要求并转换为线性时态逻辑属性,并得到原子命题集;采用符号化有限状态机对轨道交通联锁系统进行建模,得到参考模型;计算轨道交通联锁系统中的所有估值函数,根据估值函数生成得到符号迹及其对应的具体迹;对参考模型进行改良,得到改良后的参考模型,将估值函数映射到原子命题集中,得到命题抽象;基于参考模型的符号迹和命题抽象生成测试用例,在改良后的参考模型上执行测试用例,直至测试用例满足精炼的软件安全要求,解决了轨道联通联锁系统的一致性测试无法面向其安全需求的问题。

Patent Agency Ranking