Web应用中UML到Event-B的系统性转换方法

1

作者 智玉华 邹盛荣 +1 位作者 刘晓莹 耿雪 《软件导刊》 2025年第8期112-120,共9页

在面向对象的软件开发过程中,UML被广泛应用于建模,但因其语义的不精确性使得模型难以进行形式化验证。同时,Event-B作为一种基于数学逻辑的形式化方法,尽管精确但难以理解。为了充分发挥两种方法的优势,提出一种将UML与Event-B形式化... 在面向对象的软件开发过程中,UML被广泛应用于建模,但因其语义的不精确性使得模型难以进行形式化验证。同时,Event-B作为一种基于数学逻辑的形式化方法,尽管精确但难以理解。为了充分发挥两种方法的优势,提出一种将UML与Event-B形式化方法相结合的解决方案,针对中型Web应用系统,提出了用例图、类图、顺序图、组件图和部署图5种UML图到Event-B的转换方法。通过将其应用于实际Web应用系统,并利用Rodin平台的证明器解除模型中的证明义务,验证了这一转换方法的可行性和有效性。该方法的应用,不仅提高了UML的精确性和系统的可靠性,减少了故障风险,还增强了形式化方法的可理解性,有助于其推广和应用。 展开更多

关键词 统一建模语言 形式化方法 event-b WEb应用

在线阅读 下载PDF 职称材料

基于Event-B的区块链Raft共识形式化建模方法

2

作者 陈中绪 任睿 崔慧敏 《山西电子技术》 2025年第2期97-99,共3页

Raft共识机制是一个关键的分布式系统组件,用于确保数据一致性和容错性。在工业互联网等领域,数据的准确性和系统的可用性至关重要。通过Event-B方法,可以精确地规约Raft共识机制的行为和性质,确保其在各种情况下能够正确运行。基于此,... Raft共识机制是一个关键的分布式系统组件,用于确保数据一致性和容错性。在工业互联网等领域,数据的准确性和系统的可用性至关重要。通过Event-B方法,可以精确地规约Raft共识机制的行为和性质,确保其在各种情况下能够正确运行。基于此,提出一种基于Event-B方法的区块链Raft共识机制的形式化建模方法,以期为Raft共识机制的设计、开发和维护提供更高的可信度。 展开更多

关键词 Raft共识算法 event-b方法 形式化建模

在线阅读 下载PDF 职称材料

基于改进Event-B建模的高速列车追踪运行仿真研究 被引量：3

3

作者 陈永 张薇 胡晓辉 《计算机工程》 CAS CSCD 北大核心 2015年第8期256-261,共6页

针对铁路移动闭塞系统中高速列车间隔动态实时变化的特征,结合Agent理论对Event-B方法中Machine动态属性进行改进,提出一种基于Event-B建模方法的高速列车追踪运行模型。给出高速列车追踪运行形式化控制策略,研究运行过程中速度变化关... 针对铁路移动闭塞系统中高速列车间隔动态实时变化的特征,结合Agent理论对Event-B方法中Machine动态属性进行改进,提出一种基于Event-B建模方法的高速列车追踪运行模型。给出高速列车追踪运行形式化控制策略,研究运行过程中速度变化关系、不同发车间隔时间对高速铁路运营的影响,得到相应的定量与定性分析。仿真结果表明,该模型能够准确描述高速列车追踪运行机理,有助于列车间隔动态控制,具有较强的适用性。 展开更多

关键词 高速列车 列车追踪 event-b方法 形式化方法 交通仿真 建模

在线阅读 下载PDF 职称材料

基于Event-B方法的安全协议设计、建模与验证 被引量：3

4

作者 李梦君 潘国腾 欧国东 《软件学报》 EI CSCD 北大核心 2018年第11期3400-3411,共12页

随着软件精化验证方法以及Isabella/HOL、VCC等验证工具不断取得进展,研究者们开始采用精化方法和验证工具设计、建模安全协议和验证安全协议源程序的正确性.在介绍Event-B方法和验证工具Isabella/HOL、VCC的基础上,综述了基于Event-B... 随着软件精化验证方法以及Isabella/HOL、VCC等验证工具不断取得进展,研究者们开始采用精化方法和验证工具设计、建模安全协议和验证安全协议源程序的正确性.在介绍Event-B方法和验证工具Isabella/HOL、VCC的基础上,综述了基于Event-B方法的安全协议形式化设计、建模与源程序验证的典型研究工作,主要包括从需求规范到消息传递形式协议的安全协议精化设计、基于TPM(trusted platform module)的安全协议应用的精化建模以及从消息传递形式协议到代码的源程序精化验证. 展开更多

关键词 安全协议设计 安全协议建模与验证 精化 event-b方法

在线阅读 下载PDF 职称材料

基于Event-B的形式化建模关键技术研究 被引量：4

5

作者 吴劲 陈志慧 《电子科技大学学报》 EI CAS CSCD 北大核心 2014年第3期405-408,共4页

软件系统的规模和复杂程度不断提高而传统的需求分析方法难以确保软件的正确性和一致性,为软件系统的质量埋下了隐患。软件工程的实践表明,在开发过程中,错误发现得越早,修复得越早,付出的代价越小。为了确保软件的质量,可在软件开发的... 软件系统的规模和复杂程度不断提高而传统的需求分析方法难以确保软件的正确性和一致性,为软件系统的质量埋下了隐患。软件工程的实践表明,在开发过程中,错误发现得越早,修复得越早,付出的代价越小。为了确保软件的质量,可在软件开发的早期需求分析阶段,采用Event-B形式化方法描述软件的需求,并验证模型的正确性。以文件系统建模为例,该文讨论了如何利用Event-B方法,采用逐步精化的方式建立并验证模型,确保软件的正确性。 展开更多

关键词 event-b形式化方法 形式化建模 精化 需求分析

在线阅读 下载PDF 职称材料

基于Event-B和Rodin开展形式化软件工程教学 被引量：1

6

作者 李梦君 《计算机工程与科学》 CSCD 北大核心 2016年第A01期143-145,共3页

形式化软件工程是软件工程的重要组成部分。Event-B方法是一种软件形式化开发方法,Rodin是支持Event-B方法的开放工具集。基于Event-B方法和Rodin开展形式化软件工程教学,有益于学生正确理解精化等重要的软件工程概念,理解并掌握开发可... 形式化软件工程是软件工程的重要组成部分。Event-B方法是一种软件形式化开发方法,Rodin是支持Event-B方法的开放工具集。基于Event-B方法和Rodin开展形式化软件工程教学,有益于学生正确理解精化等重要的软件工程概念,理解并掌握开发可信软件的方法,是软件工程教学的重要补充。 展开更多

关键词 形式化软件工程 event—b方法 Rodin

在线阅读 下载PDF 职称材料

基于Event-B的联锁进路控制建模验证方法研究 被引量：2

7

作者 童湖东 宁滨 王海峰 《铁路计算机应用》 2013年第6期57-61,共5页

计算机联锁系统具有典型的安全苛求特性。传统的联锁软件开发方法难以完整准确地定义需求,单纯依靠测试也无法发现软件中的所有错误,使软件在功能完整性和安全性方面难以得到保证。本文利用形式化Event-B方法和相关工具对联锁系统的核... 计算机联锁系统具有典型的安全苛求特性。传统的联锁软件开发方法难以完整准确地定义需求,单纯依靠测试也无法发现软件中的所有错误,使软件在功能完整性和安全性方面难以得到保证。本文利用形式化Event-B方法和相关工具对联锁系统的核心功能—进路控制的相关功能需求和安全需求进行了建模、精化和验证,对开发高安全苛求和高可靠性的联锁软件提供了新的方法借鉴。 展开更多

关键词 联锁 进路控制 event-b建模 形式化方法

在线阅读 下载PDF 职称材料

矿井机车运输信号系统的Event-B建模与验证研究

8

作者 荚文祥 陆阳 +1 位作者 许崇 魏振春 《合肥工业大学学报（自然科学版）》 CAS 北大核心 2018年第6期787-794,共8页

人工编制联锁表难以保证联锁表的准确性,而且单纯依靠人工检查联锁表中每个表项的正确性也是一项非常繁琐的工作。文章针对目前存在的问题,利用形式化Event-B方法对机车运输信号平面布置图、进路联锁表和机车车辆运输信号设计规范进行建... 人工编制联锁表难以保证联锁表的准确性,而且单纯依靠人工检查联锁表中每个表项的正确性也是一项非常繁琐的工作。文章针对目前存在的问题,利用形式化Event-B方法对机车运输信号平面布置图、进路联锁表和机车车辆运输信号设计规范进行建模,模型生成的证明义务通过与否验证了进路联锁表建立过程是否符合平面布置图和设计规范的要求,利用该种思路解决了人工检查联锁表存在的效率低和不确定性等问题。 展开更多

关键词 联锁表 event-b方法 形式化方法 机车 证明义务

在线阅读 下载PDF 职称材料

基于Event-B的可靠智能合约自动生成方法

9

作者 朱健 胡凯 +3 位作者 王军 李洁 叶亚飞 时希言 《计算机科学》 CSCD 北大核心 2023年第10期343-349,共7页

智能合约是一种以代码的方式执行合同条款的可计算交易协议,其应用场景与规模日益增长,承载着多达数十亿美元的各类资产。由于其代码缺陷可能会造成严重的经济损失,因此智能合约的可信开发成为技术关键。为此,提出了一种基于集合论语言E... 智能合约是一种以代码的方式执行合同条款的可计算交易协议,其应用场景与规模日益增长,承载着多达数十亿美元的各类资产。由于其代码缺陷可能会造成严重的经济损失,因此智能合约的可信开发成为技术关键。为此,提出了一种基于集合论语言Event-B的智能合约可信验证与自动生成方法。Event-B方法是一种基于精化的形式化方法,可用于规约、设计和验证软件系统。通过对智能合约的模型验证和可执行代码的自动生成技术,研发了自动转换工具EB2S,打通了形式化模型和智能合约编程语言的语义鸿沟和技术壁垒。最后,选取典型的在线支付智能合约场景,应用基于Event-B的智能合约模型自动生成合约代码,验证了EB2S转换工具的有效性。 展开更多

关键词 智能合约 event-b方法 自动代码生成 Solidity合约 定理证明

在线阅读 下载PDF 职称材料

UML到Event-B的系统化转换方法 被引量：1

10

作者 耿雪 邹盛荣 +1 位作者 刘晓莹 姚聚义 《计算机技术与发展》 2023年第12期113-120,共8页

在面向对象的软件开发中,UML已经成为事实上的建模标准。然而,UML虽然直观容易理解和应用,却存在着不精确的语义,而且UML是一种半形式化的建模语言,无法进行形式化的验证。Event-B是一种基于大量数学谓词逻辑的形式化方法,虽然精确却难... 在面向对象的软件开发中,UML已经成为事实上的建模标准。然而,UML虽然直观容易理解和应用,却存在着不精确的语义,而且UML是一种半形式化的建模语言,无法进行形式化的验证。Event-B是一种基于大量数学谓词逻辑的形式化方法,虽然精确却难以理解和应用。因此,如何结合UML图和Event-B方法的优点是研究的重点,以往的方法都是基于UML零散图到Event-B的转换,缺乏系统的转换方法。系统性的转换方法可以实现UML中的元素与Event-B中的元素相对应统一。一般的软件系统是中型系统,中型系统采用用例图、类图、状态图和顺序图这四种图就可以很好地表达清楚,有了上述的四种图,软件生命周期的需求获取、分析、设计、详细设计就可以完全表达清楚。文章中分别给出了这四种图到Event-B的转换方法,并将该系统的转换方法应用到对安全性和可靠性要求较高的电梯控制系统中。基于该实例的研究,验证了UML到Event-B系统性转换方法的可行性和有效性。UML到Event-B的系统转换方法不仅有利于UML的精确化和软件从业人员的使用,而且增强了形式化方法的可理解性,有利于形式化方法的推广和应用。 展开更多

关键词 统一建模语言 形式化方法 event-b 抽象转换 模型

在线阅读 下载PDF 职称材料

基于Event-B的自动化模块组合方法研究 被引量：1

11

作者 陈金鑫 苏雯 《计算机工程》 CAS CSCD 北大核心 2019年第5期298-307,314,共11页

Event-B共享变量和共享事件方法可将大型系统分解成多个子系统,并独立建模开发,但其需要手工干预以实现模型间事件的组合。为提高组合效率,提出一种针对模型的自动化组合理论,并开发自动化组合工具原型。为在精化模型中逐步引入模块调用... Event-B共享变量和共享事件方法可将大型系统分解成多个子系统,并独立建模开发,但其需要手工干预以实现模型间事件的组合。为提高组合效率,提出一种针对模型的自动化组合理论,并开发自动化组合工具原型。为在精化模型中逐步引入模块调用,改进PROG方法,开发自动精化工具原型。通过2个应用案例,验证了自动化组合工具能自动组合事件,自动精化工具能减少调用变量的数量,从而增强系统模型的可读性和可维护性。 展开更多

关键词 形式化方法 event-b方法 模块化建模 自动化模块组合方法 模块调用 精化

在线阅读 下载PDF 职称材料

基于Event-B的控制系统形式化建模方法研究

12

作者 唐晨 陈邦兴 +1 位作者 陈祖希 沈啸 《佳木斯大学学报（自然科学版）》 CAS 2014年第1期33-36,41,共5页

为降低形式化建模的难度,本文深入研究了基于Event-B的开发框架,并结合控制系统中控制器与被控环境之间的交互特征,提出了一套基于Event-B的控制系统有序模块化建模指导原则,能够帮助设计人员在开发的早期更加深入地理解系统需求,获得... 为降低形式化建模的难度,本文深入研究了基于Event-B的开发框架,并结合控制系统中控制器与被控环境之间的交互特征,提出了一套基于Event-B的控制系统有序模块化建模指导原则,能够帮助设计人员在开发的早期更加深入地理解系统需求,获得清晰的建模思路和开发策略,为设计高安全性的软件系统提供保障.最后,应用该方法完成了RBC(区域控制器)系统的形式化建模,说明了该方法的实用性. 展开更多

关键词 控制系统 形式化方法 event—b建模 RbC系统

在线阅读 下载PDF 职称材料

基于Event-B对存在网络攻击的安全协议的改进研究 被引量：1

13

作者 朱俊翔 张翔 《中国电子科学研究院学报》 北大核心 2020年第6期530-538,共9页

设计对指定类型的网络攻击具有防御能力的安全协议,通常是一项重要且具有挑战性的任务。即使知道安全协议容易受到某种攻击,对其进行合理的改进也并不容易。本研究提出了一个基于Event-B方法的通用框架,用来指导安全协议的修改,并验证... 设计对指定类型的网络攻击具有防御能力的安全协议,通常是一项重要且具有挑战性的任务。即使知道安全协议容易受到某种攻击,对其进行合理的改进也并不容易。本研究提出了一个基于Event-B方法的通用框架,用来指导安全协议的修改,并验证改进后的协议可以防御已知的网络攻击。首先用初始模型对攻击场景高度抽象,通过对抽象模型的精化,得到反映真实攻击过程的具体模型。然后将描述协议行为的事件从模型中分离出来,单独对其进行精化改进,如果改进后的协议事件重组的模型与具体模型不存在精化关系,则改进的合理性可以得到验证。最后通过NSPK协议被攻击的案例展示了本研究所提出方法的可用性。该框架可用于开发协议,以避免由逻辑漏洞引起的攻击,并验证协议补丁的正确性。 展开更多

关键词 形式化方法 精化理论 模型检测 event-b方法 安全协议设计 网络攻击

在线阅读 下载PDF 职称材料

基于Event-B方法的需求建模及验证

14

作者 史逸轩 《忻州师范学院学报》 2019年第2期24-31,共8页

Event-B是国外新兴的一种通过形式化方法,主要用于对系统功能性需求建模并验证,在Rodin工具集中,通过给出环境、变量、常量和相关事件,对每一个抽象需求建模。其后,使用Pro-B animator进行验证。它通过逻辑分析产生验证规约并且自动抛... Event-B是国外新兴的一种通过形式化方法,主要用于对系统功能性需求建模并验证,在Rodin工具集中,通过给出环境、变量、常量和相关事件,对每一个抽象需求建模。其后,使用Pro-B animator进行验证。它通过逻辑分析产生验证规约并且自动抛除无关紧要的验证规约来取代传统的编译,解决了传统的软件工程过程中系统分析与设计阶段非形式化方法带来的低效率,错误率高,不易纠错,不灵活,编码复杂以及常常不够符合实际的缺陷。以账单分摊系统为例,详细描述了Event-B方法的需求建模和规范化验证的思路和过程方法。 展开更多

关键词 形式化方法 event-b Pro-b Rodin 逻辑分析

在线阅读 下载PDF 职称材料

基于B方法的体系结构描述语言的形式化研究 被引量：2

15

作者 丁湘陵 王志刚 《计算机工程与科学》 CSCD 北大核心 2013年第1期100-106,共7页

通过分析B方法和软件体系结构描述语言ABC/ADL各自的特点,提出了一种两者结合的形式化方法。该方法利用B方法扩充的事件机制,定义软件体系结构描述语言的构件和连接子观察模型、行为规约和约束规约,并给出了规约实例,从而使得基于B方法... 通过分析B方法和软件体系结构描述语言ABC/ADL各自的特点,提出了一种两者结合的形式化方法。该方法利用B方法扩充的事件机制,定义软件体系结构描述语言的构件和连接子观察模型、行为规约和约束规约,并给出了规约实例,从而使得基于B方法的ABC/ADL能够形式化描述软件体系结构的结构和行为。 展开更多

关键词 体系结构描述语言 b方法 事件 形式化

在线阅读 下载PDF 职称材料

优化后触发工具在某院多黏菌素B药品不良事件监测中的应用研究 被引量：2

16

作者 王晔 梁培 +1 位作者 吴晓燕 张海霞 《中国新药与临床杂志》 CAS CSCD 北大核心 2022年第5期307-311,共5页

目的 运用优化后触发工具对本院住院患者发生的多黏菌素B药品不良事件(ADE)进行监测,以期为多黏菌素B不良事件的监测及防治提供依据。方法 依据美国医疗保健改善研究所全球触发工具(GTT)的触发器及文献调研,结合目前国内外关于使用多黏... 目的 运用优化后触发工具对本院住院患者发生的多黏菌素B药品不良事件(ADE)进行监测,以期为多黏菌素B不良事件的监测及防治提供依据。方法 依据美国医疗保健改善研究所全球触发工具(GTT)的触发器及文献调研,结合目前国内外关于使用多黏菌素B报道的相关不良事件,对触发器做适当调整优化。调取本院2019年1月1日至2020年12月31日使用多黏菌素B的病例资料,按照优化后触发工具审查病例,应用Naranjo法评定ADE,对其进行严重程度分级,记录相关累及的器官/系统及临床表现、采取的干预措施及最终转归等信息。比较优化后触发工具检出的ADE与同时段自发呈报系统上报情况,并对相关数据进行统计分析。结果 优化后触发工具包括17项与本研究相关的触发器。209例病例资料中,检出触发器阳性106例次,发生多黏菌素B有关ADE 57例次,涉及52例患者,触发器的阳性预测值为53.8%(57/106),触发器检出的ADE发生率为24.9%(52/209),与医院同期ADE自发上报率6.7%(14/209)相比,有显著差异(P <0.05)。57例次ADE中评定为可能的有36例次(63%),很可能的有21例次(37%);对其严重程度进行分级,E级伤害46例次,F级伤害8例次,G级伤害3例次;共累及器官/系统4类,其中急性肾损害所占比例最多,共35例次(61%)。采取干预措施后,最终痊愈13例次,好转23例次,未好转10例次,不详11例次。结论 相比于自发上报系统,优化后触发工具对ADE的检测效能较高,可用于多黏菌素B ADE的主动监测。 展开更多

关键词 全面触发工具 卫生保健 多黏菌素b 药品不良事件 Naranjo法 药物监测

原文传递

车站联锁进路控制逻辑的形式化方法 被引量：8

17

作者 胡晓辉 韩佳芮 《计算机工程与应用》 CSCD 北大核心 2016年第17期229-234,270,共7页

基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统,车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化方法 Event-B为基础,引入角色Agent对联锁系统进行规范定义,通过智能体与Event-B的建模和验证... 基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统,车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化方法 Event-B为基础,引入角色Agent对联锁系统进行规范定义,通过智能体与Event-B的建模和验证,构造了车站联锁进路控制逻辑形式化验证模型,并进行了形式化规范和推理,该模型在RODIN平台上进行验证,通过实例验证,满足了计算机联锁系统的安全需求。 展开更多

关键词 联锁 进路控制 event-b方法 多智能体系统(MAS)

在线阅读 下载PDF 职称材料

列车安全距离控制形式化建模与验证 被引量：1

18

作者 胡晓辉 肖知屹 +1 位作者 陈永 李欣 《计算机应用》 CSCD 北大核心 2014年第3期851-856,共6页

随着我国铁路的迅速发展,对列车运行安全性的要求越来越高。采用Event-B形式化建模方法研究了高速列车安全距离控制形式化验证问题,以Event-B形式化仿真工具Rodin为基础,通过结合多智能体理论,引入感知决策法则,实现了无线闭塞中心(RBC... 随着我国铁路的迅速发展,对列车运行安全性的要求越来越高。采用Event-B形式化建模方法研究了高速列车安全距离控制形式化验证问题,以Event-B形式化仿真工具Rodin为基础,通过结合多智能体理论,引入感知决策法则,实现了无线闭塞中心(RBC)与列车的车地通信,建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行,对列车安全距离控车行为进行了形式化建模并进行了POs证明义务验证。仿真结果表明,对于CTCS列车控制系统的复杂逻辑关联行为,采用提出的Event-B和多智能体系统(MAS)结合的形式化验证方法,可进行系统规范的模型验证,对于复杂系统的逻辑验证有较强的实际意义。 展开更多

关键词 event-b方法 列车控制 多智能体 形式化建模 分布式系统

在线阅读 下载PDF 职称材料

基于模型的开发方法在多应用智能卡中的应用 被引量：2

19

作者 章玥 郭建 朱晓冉 《信息网络安全》 2013年第12期75-79,共5页

安全性、可靠性是嵌入式软件的重要性质。为了更好地保证开发的嵌入式软件是可靠和安全的,提出了一种基于模型的开发方法学,包括提炼需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面提取需求,同时明确层次... 安全性、可靠性是嵌入式软件的重要性质。为了更好地保证开发的嵌入式软件是可靠和安全的,提出了一种基于模型的开发方法学,包括提炼需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面提取需求,同时明确层次化的精化策略;然后利用形式化方法建立抽象模型并对该模型进行形式化验证,在正确的抽象模型上逐层精化,并对每层模型进行验证;最后,基于满足需求的模型,进一步利用工具完成代码自动生成。该方法从抽象到具体,以逐层递增的方式明确被开发系统的需求及性质,进行形式化建模,通过反馈机制确保模型的正确性及可用性。为了证明该方法学的可行性,文章以多应用智能卡为开发实例,基于Event-B方法及Rodin平台给出了实际建模及证明的过程和结果。 展开更多

关键词 智能卡 event—b 形式化方法 定理证明

在线阅读 下载PDF 职称材料

符合民机适航标准的形式化方法研究 被引量：2

20

作者 王辉 陈蕾 +1 位作者 曹杨华 唐晨 《航空电子技术》 2019年第4期53-59,共7页

描述了形式化方法的定义、目的、作用和软件开发流程。以发动机仪表盘显示布局风格需求为例,通过四变量形式化方法对需求进行形式化建模,通过形式化分析证明模型的完备性和一致性。以发动机油量周期计算需求为例,通过Event-B形式化方法... 描述了形式化方法的定义、目的、作用和软件开发流程。以发动机仪表盘显示布局风格需求为例,通过四变量形式化方法对需求进行形式化建模,通过形式化分析证明模型的完备性和一致性。以发动机油量周期计算需求为例,通过Event-B形式化方法对需求进行形式化建模,通过形式化分析发现需求糢型的缺陷。对民机适航标准形式化方法相关的三份补充文件进行了解读,对采用形式化方法进行民机软件开发具有指导意义。 展开更多

关键词 形式化方法 形式化模型 形式化分析 四变量模型 event-b

在线阅读 下载PDF 职称材料