基于Event-B的形式化建模关键技术研究

留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

基于Event-B的形式化建模关键技术研究

吴劲, 陈志慧

文章导航 > 电子科技大学学报 > 2014 > 43(3): 405-408

吴劲, 陈志慧. 基于Event-B的形式化建模关键技术研究[J]. 电子科技大学学报, 2014, 43(3): 405-408. doi: 10.3969/j.issn.1001-0548.2014.03.015

引用本文:

吴劲, 陈志慧. 基于Event-B的形式化建模关键技术研究[J]. 电子科技大学学报, 2014, 43(3): 405-408. doi: 10.3969/j.issn.1001-0548.2014.03.015

WU Jin, CHEN Zhi-hui. Research on Formally Modeling Based Event-B[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(3): 405-408. doi: 10.3969/j.issn.1001-0548.2014.03.015

Citation:

WU Jin, CHEN Zhi-hui. Research on Formally Modeling Based Event-B[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(3): 405-408. doi: 10.3969/j.issn.1001-0548.2014.03.015

基于Event-B的形式化建模关键技术研究

doi: 10.3969/j.issn.1001-0548.2014.03.015

吴劲,
陈志慧

1.
电子科技大学计算机科学与工程学院成都 610054

基金项目:

中央高校基本科研业务费(ZYGX2011J072); 国家科技重大专项(2011ZX03002-002-03); 国家自然科学基金重点项目(61133016); 四川省科技计划项目(2013GZ0022)

作者简介:
吴劲(1972-),女,博士,副教授,主要从事软件技术与理论方面的研究.

中图分类号: TP311

Research on Formally Modeling Based Event-B

1.
School of Computer Science & Engineering,University of Electronic Science and Technology of China Chengdu 610054

摘要: 软件系统的规模和复杂程度不断提高而传统的需求分析方法难以确保软件的正确性和一致性，为软件系统的质量埋下了隐患. 软件工程的实践表明，在开发过程中，错误发现得越早，修复得越早，付出的代价越小. 为了确保软件的质量，可在软件开发的早期需求分析阶段，采用Event-B形式化方法描述软件的需求，并验证模型的正确性. 以文件系统建模为例，该文讨论了如何利用Event-B方法，采用逐步精化的方式建立并验证模型，确保软件的正确性.
- Event-B形式化方法 /
- 形式化建模 /
- 精化 /
- 需求分析
Abstract: The scale and complexity of software systems continue to increase and the traditional requirement analysis method is difficult to ensure the consistency and correctness of software, which is laying the trouble for the quality of a software system. Practice of the software engineering shows that in the software developing process, the earlier the errors are found and repaired, the less the cost is paid. In order to ensure the quality of software, on the early stage of software development, Event-B can be used to formally describe the software requirements and verify the correctness of the model. In the file system modeling as an example, this paper discusses how to use Event-B method and stepwise refinement to establish and validate the model, so as to ensure the correctness of software.
- Event-B formal method /
- formal modling /
- refinement /
- requirement analysis

[1]	叶启彬, 胡泽林, 黄驿轩, 胡苏, 崔国龙, 张振宇. 5G NR通信雷达一体化系统雷达性能分析 . 电子科技大学学报, 2022, 51(6): 847-855. doi: 10.12178/1001-0548.2022299
[2]	黄驿轩, 胡苏, 叶启彬, 胡泽林. 基于连续波的通信雷达一体化距离处理分析 . 电子科技大学学报, 2022, 51(5): 688-693. doi: 10.12178/1001-0548.2021246
[3]	孙海泳, 杨霞, 雷航, 乔磊, 杨拯. 基于TrustZone的TEE设计与信息流形式化验证 . 电子科技大学学报, 2019, 48(2): 259-263. doi: 10.3969/j.issn.1001-0548.2019.02.016
[4]	李凤英, 何志伟, 董荣胜. 多状态不交化路径可靠性分析的符号算法 . 电子科技大学学报, 2018, 47(6): 819-828. doi: 10.3969/j.issn.1001-0548.2018.06.004
[5]	陆金波, 侯晓荣, 罗敏. Hopf分岔系统的参数化镇定方法 . 电子科技大学学报, 2016, 45(6): 944-949. doi: 10.3969/j.issn.1001-0548.2016.06.012
[6]	肖毅, 陈善广, 韩东旭, 王春慧. 脑电信号多重粗粒化复杂度分析方法研究 . 电子科技大学学报, 2013, 42(3): 470-474. doi: 10.3969/j.issn.1001-0548.2013.03.029
[7]	任洪敏, 刘晋. 软件体系结构交互动作精化研究 . 电子科技大学学报, 2013, 42(1): 137-143. doi: 10.3969/j.issn.1001-0548.2013.01.028
[8]	张昌利, 龚建国, 闫茂德. 基于复杂网络的社会化标签语义相似度分析 . 电子科技大学学报, 2012, 41(5): 642-648. doi: 10.3969/j.issn.1001-0548.2012.05.001
[9]	詹鹏, 秦开宇, 蔡顺燕. 新的射频功放预失真线性化方法 . 电子科技大学学报, 2011, 40(5): 676-681. doi: 10.3969/j.issn.1001-0548.2011.05.008
[10]	张靖, 何发镁, 邱云. 个性化推荐系统描述文件攻击检测方法 . 电子科技大学学报, 2011, 40(2): 250-254. doi: 10.3969/j.issn.1001-0548.2011.02.019
[11]	陈文宇, 向涛, 王晓斌, 桑楠, 孙世新. 实时可信服务的构件设计与形式化描述 . 电子科技大学学报, 2011, 40(1): 122-127. doi: 10.3969/j.issn.1001-0548.2011.01.023
[12]	傅强, 刘晓东. 多媒体呈现流程的形式化描述及内容表示 . 电子科技大学学报, 2008, 37(5): 753-756.
[13]	仇傲, 周山宏, 刘春梅. 数字化B超中的频率补偿滤波 . 电子科技大学学报, 2007, 36(4): 798-800.
[14]	瞿成明, 江明, 陈其工. 直接转矩控制转矩脉动最小化方法研究 . 电子科技大学学报, 2006, 35(6): 942-945.
[15]	王聪, 王智学, 江光杰. 基于ECA规则的业务行为描述方法 . 电子科技大学学报, 2006, 35(1): 104-107.
[16]	洪洁, 范修斌, 方刚, 路晓峰. 布尔函数最优连续化 . 电子科技大学学报, 2004, 33(5): 621-622,626.
[17]	袁丁, 范平志. 电子证据与反拒认协议及形式化分析 . 电子科技大学学报, 2004, 33(5): 531-534.
[18]	陶德元, 袁晓, 何小海. 一类复子波的时-频局域化特征分析 . 电子科技大学学报, 2001, 30(1): 21-25.
[19]	李仕明, 唐小我, 曾勇. 产权化激励机制的定量分析 . 电子科技大学学报, 2001, 30(2): 185-191.
[20]	喻胜, 何丕雁, 陈光. 利用最小化代价函数方法实现多窗口谱分析 . 电子科技大学学报, 1999, 28(3): 273-277.

WeChat

点击查看大图

计量

文章访问数: 3327
HTML全文浏览量: 131
PDF下载量: 226
被引次数: 0

基于Event-B的形式化建模关键技术研究

doi: 10.3969/j.issn.1001-0548.2014.03.015

吴劲,
陈志慧

1. 电子科技大学计算机科学与工程学院成都 610054

基金项目:

中央高校基本科研业务费(ZYGX2011J072); 国家科技重大专项(2011ZX03002-002-03); 国家自然科学基金重点项目(61133016); 四川省科技计划项目(2013GZ0022)

作者简介:
吴劲(1972-),女,博士,副教授,主要从事软件技术与理论方面的研究.

收稿日期: 2013-04-08
修回日期: 2014-03-06
刊出日期: 2014-06-15

中图分类号: TP311

关键词:

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

English Abstract

吴劲, 陈志慧. 基于Event-B的形式化建模关键技术研究[J]. 电子科技大学学报, 2014, 43(3): 405-408. doi: 10.3969/j.issn.1001-0548.2014.03.015

引用本文:

吴劲, 陈志慧. 基于Event-B的形式化建模关键技术研究[J]. 电子科技大学学报, 2014, 43(3): 405-408. doi: 10.3969/j.issn.1001-0548.2014.03.015

WU Jin, CHEN Zhi-hui. Research on Formally Modeling Based Event-B[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(3): 405-408. doi: 10.3969/j.issn.1001-0548.2014.03.015

Citation:

WU Jin, CHEN Zhi-hui. Research on Formally Modeling Based Event-B[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(3): 405-408. doi: 10.3969/j.issn.1001-0548.2014.03.015

全文HTML

/

下载: 全尺寸图片幻灯片

分享

用微信扫码二维码

分享至好友和朋友圈

返回

期刊在线

编辑办公

友情链接

电子科技大学

版权所有 © 《电子科技大学学报》编辑部

地址: 成都市建设北路二段四号电子科技大学主楼中350室电话: 028-83202308,83207559 Email: xuebao@uestc.edu.cn

本系统由北京仁和汇智信息技术有限公司开发