-
公开(公告)号:CN112947370A
公开(公告)日:2021-06-11
申请号:CN202110148981.4
申请日:2021-02-03
Applicant: 华侨大学 , 舒柏睿(厦门)信息科技有限公司
IPC: G05B23/02
Abstract: 本发明公开了一种蒸汽锅炉系统的安全分析方法及系统,本发明通过对蒸汽锅炉系统的控制结构和控制流程分析,获得控制结构的分析结果到控制流程的映射关系和蒸汽锅炉系统到Event‑B模型的建模元素的映射关系,进而建立了用于蒸汽锅炉系统的安全预防的初始的Event‑B模型,并进一步对初始的Event‑B模型进行了修正,利用修正后的Event‑B模型进行蒸汽锅炉系统的安全性的预防,实现了蒸汽锅炉系统的安全预防。
-
公开(公告)号:CN116187104A
公开(公告)日:2023-05-30
申请号:CN202310464545.7
申请日:2023-04-27
Applicant: 华侨大学
IPC: G06F30/20 , G06F111/04 , G06F119/02
Abstract: 本发明公开一种轨道交通联锁系统安全分析开发方法及装置,涉及系统安全评估技术领域,方法包括:基于系统级安全约束表,采用STPA分析方法,确定所述初始控制反馈模型的安全分析结果;若初始控制反馈模型不满足预设安全条件,则对初始控制反馈模型进行精化处理,以得到精化后控制反馈模型;精化处理包括引入轨道区段、引入道岔和道岔位置状态、引入轨道区段状态以及引入信号机中的一项或多项;基于系统级安全约束表,采用STPA分析方法确定精化后控制反馈模型的安全分析结果,并基于精化后控制反馈模型的安全分析结果进行轨道交通联锁系统的设计开发。本发明实现基于STPA设计的抽象精化的安全分析,提高安全分析的精细程度。
-
公开(公告)号:CN115982207A
公开(公告)日:2023-04-18
申请号:CN202310264829.1
申请日:2023-03-20
Applicant: 华侨大学
IPC: G06F16/2453 , G06F16/2458 , G06F16/901 , G06F9/54
Abstract: 本发明涉及一种银行交易资金回流多线程并行检测方法及系统,属于大数据分析处理领域。方法包括:根据银行交易记录构建有向图及其邻接表存储结构,并增加一个虚拟顶点来指向有向图中每一个顶点;基于有向图创建线程间共享内存数据结构,定义并初始化线程内局部数据结构;调用多个线程同时从虚拟顶点出发进行深度优先搜索遍历执行有向环路求解算法;所有线程运行结束之后,利用线程间共享内存数据结构中的环路集合输出检测到的资金回流环路。本发明方法通过将计算任务分解到多个线程上并行执行,充分利用了底层多核处理器的高并发性缩短了算法执行时间,提高了存在回流预警的交易环路的挖掘效率。
-
公开(公告)号:CN115494829B
公开(公告)日:2023-03-14
申请号:CN202211432332.8
申请日:2022-11-16
Applicant: 华侨大学
Abstract: 本发明公开了一种自主列车运行控制系统建模及验证方法,属于轨道交通系统建模领域。该方法包括:对自主列车运行控制系统进行分析,得到自主列车运行控制系统分析图;基于所述自主列车运行控制系统分析图对所述自主列车运行控制系统进行非形式化描述;基于所述非形式化描述对所述自主列车运行控制系统进行建模;采用Event‑B形式化方法对所述自主列车运行控制系统的模型进行优化;通过Rodin平台中的定理证明器对优化后的自主列车运行控制系统的模型进行证明。本发明基于抽象数据类型(ADT)与Event‑B方法的精化策略对自主列车运行控制系统进行建模,利用ADT的抽象概念,能够有效弥补单一使用精化策略的不足之处。
-
公开(公告)号:CN115494829A
公开(公告)日:2022-12-20
申请号:CN202211432332.8
申请日:2022-11-16
Applicant: 华侨大学
Abstract: 本发明公开了一种自主列车运行控制系统建模及验证方法,属于轨道交通系统建模领域。该方法包括:对自主列车运行控制系统进行分析,得到自主列车运行控制系统分析图;基于所述自主列车运行控制系统分析图对所述自主列车运行控制系统进行非形式化描述;基于所述非形式化描述对所述自主列车运行控制系统进行建模;采用Event‑B形式化方法对所述自主列车运行控制系统的模型进行优化;通过Rodin平台中的定理证明器对优化后的自主列车运行控制系统的模型进行证明。本发明基于抽象数据类型(ADT)与Event‑B方法的精化策略对自主列车运行控制系统进行建模,利用ADT的抽象概念,能够有效弥补单一使用精化策略的不足之处。
-
公开(公告)号:CN118427841B
公开(公告)日:2024-10-22
申请号:CN202410886462.1
申请日:2024-07-03
Applicant: 华侨大学
Abstract: 本发明公开了一种面向安全需求的轨道交通联锁系统一致性测试方法及装置,涉及软件测试领域,包括:采用STPA技术对轨道交通联锁系统进行分析,得到精炼的软件安全要求并转换为线性时态逻辑属性,并得到原子命题集;采用符号化有限状态机对轨道交通联锁系统进行建模,得到参考模型;计算轨道交通联锁系统中的所有估值函数,根据估值函数生成得到符号迹及其对应的具体迹;对参考模型进行改良,得到改良后的参考模型,将估值函数映射到原子命题集中,得到命题抽象;基于参考模型的符号迹和命题抽象生成测试用例,在改良后的参考模型上执行测试用例,直至测试用例满足精炼的软件安全要求,解决了轨道联通联锁系统的一致性测试无法面向其安全需求的问题。
-
公开(公告)号:CN118427841A
公开(公告)日:2024-08-02
申请号:CN202410886462.1
申请日:2024-07-03
Applicant: 华侨大学
Abstract: 本发明公开了一种面向安全需求的轨道交通联锁系统一致性测试方法及装置,涉及软件测试领域,包括:采用STPA技术对轨道交通联锁系统进行分析,得到精炼的软件安全要求并转换为线性时态逻辑属性,并得到原子命题集;采用符号化有限状态机对轨道交通联锁系统进行建模,得到参考模型;计算轨道交通联锁系统中的所有估值函数,根据估值函数生成得到符号迹及其对应的具体迹;对参考模型进行改良,得到改良后的参考模型,将估值函数映射到原子命题集中,得到命题抽象;基于参考模型的符号迹和命题抽象生成测试用例,在改良后的参考模型上执行测试用例,直至测试用例满足精炼的软件安全要求,解决了轨道联通联锁系统的一致性测试无法面向其安全需求的问题。
-
公开(公告)号:CN116187104B
公开(公告)日:2023-08-01
申请号:CN202310464545.7
申请日:2023-04-27
Applicant: 华侨大学
IPC: G06F30/20 , G06F111/04 , G06F119/02
Abstract: 本发明公开一种轨道交通联锁系统安全分析开发方法及装置,涉及系统安全评估技术领域,方法包括:基于系统级安全约束表,采用STPA分析方法,确定所述初始控制反馈模型的安全分析结果;若初始控制反馈模型不满足预设安全条件,则对初始控制反馈模型进行精化处理,以得到精化后控制反馈模型;精化处理包括引入轨道区段、引入道岔和道岔位置状态、引入轨道区段状态以及引入信号机中的一项或多项;基于系统级安全约束表,采用STPA分析方法确定精化后控制反馈模型的安全分析结果,并基于精化后控制反馈模型的安全分析结果进行轨道交通联锁系统的设计开发。本发明实现基于STPA设计的抽象精化的安全分析,提高安全分析的精细程度。
-
公开(公告)号:CN119225336A
公开(公告)日:2024-12-31
申请号:CN202411339029.2
申请日:2024-09-25
Applicant: 华侨大学
IPC: G05B23/02
Abstract: 本发明公开了一种基于STPA的高速铁路ATP系统故障注入测试方法,包括以下步骤:应用STPA方法对高速铁路ATP系统进行分析,识别故障场景与安全要求;基于故障场景与安全要求,运用CoFI方法生成高速铁路ATP系统的有限状态机模型FSM;在有限状态机模型FSM上运用Wp方法生成测试用例;使用测试用例对高速铁路ATP系统进行测试。本发明将STPA方法、CoFI方法和Wp方法相结合,为ATP系统的故障注入测试提供一种全面而有效的方法,确保ATP系统的安全性和可靠性。
-
公开(公告)号:CN118426449B
公开(公告)日:2024-09-06
申请号:CN202410885607.6
申请日:2024-07-03
Applicant: 华侨大学
IPC: G05B23/02
Abstract: 本发明公开了一种安全目标导向的CBTC系统精化开发和确认方法及装置,涉及系统安全评估领域,包括:对CBTC系统进行分析,确定CBTC系统的控制结构;对控制结构进行精化分层,建模得到CBTC系统的形式化模型;采用Event‑B形式化方法对CBTC系统的形式化模型进行精化,得到Event‑B模型,通过Rodin平台中的定理证明器完成Event‑B模型进行证明,得到证明后的Event‑B模型;使用ProB工具对证明后的Event‑B模型进行动态仿真、死锁以及不变式违背检测,得到CBTC系统开发结果。本发明解决了采用基于模型检测的形式化方法进行开发会导致状态空间爆炸和无法保证构建模型正确性的问题。
-
-
-
-
-
-
-
-
-