基本信息来源于合作网站,原文需代理用户跳转至来源网站获取       
摘要:
Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型.提出了如何将Event-B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤.首先从环境、功能、性质三个主要方面重写需求,明确精化策略;然后利用形式化方法建立抽象模型并验证该模型;最后,在正确的抽象模型上按照精化策略添加需求、逐层精化,并对每层模型进行验证,基于满足需求的最后一层模型,可进一步利用工具完成代码自动生成.该方法学采用精化理论,以逐层递增的方式明确被开发系统的需求及性质,并进行形式化建模与验证,确保了模型的正确性.为了说明该方法学的可行性,以真正工业界的多应用智能卡为实例,基于Event B方法及其工具平台Rodin给出了该方法在实际建模及验证过程中的应用.
推荐文章
基于智能卡的多银行离线电子现金方案
电子现金
多银行
椭圆曲线密码体制
智能卡
应对智能卡硬件攻击的软件方法
硬件攻击
软件防御
智能卡
基于FPGA的身份认证智能卡设计
身份认证
FPGA
智能卡
信息安全
一种基于多应用智能卡的MMB-CAS支付模型
多应用
智能卡
条件接收
支付
模型
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 基于Event-B方法的多应用智能卡的建模与开发
来源期刊 计算机工程与科学 学科 工学
关键词 智能卡 Event-B 精化 定理证明
年,卷(期) 2014,(10) 所属期刊栏目
研究方向 页码范围 1943-1951
页数 9页 分类号 TP301.1
字数 6418字 语种 中文
DOI 10.3969/j.issn.1007-130X.2014.10.017
五维指标
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (3)
共引文献  (2)
参考文献  (2)
节点文献
引证文献  (4)
同被引文献  (10)
二级引证文献  (3)
1997(1)
  • 参考文献(0)
  • 二级参考文献(1)
2007(1)
  • 参考文献(0)
  • 二级参考文献(1)
2010(1)
  • 参考文献(0)
  • 二级参考文献(1)
2012(2)
  • 参考文献(2)
  • 二级参考文献(0)
2014(0)
  • 参考文献(0)
  • 二级参考文献(0)
  • 引证文献(0)
  • 二级引证文献(0)
2016(3)
  • 引证文献(2)
  • 二级引证文献(1)
2018(1)
  • 引证文献(1)
  • 二级引证文献(0)
2019(2)
  • 引证文献(1)
  • 二级引证文献(1)
2020(1)
  • 引证文献(0)
  • 二级引证文献(1)
研究主题发展历程
节点文献
智能卡
Event-B
精化
定理证明
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
计算机工程与科学
月刊
1007-130X
43-1258/TP
大16开
湖南省长沙市开福区德雅路109号国防科技大学计算机学院
42-153
1973
chi
出版文献量(篇)
8622
总下载数(次)
11
总被引数(次)
59030
  • 期刊分类
  • 期刊(年)
  • 期刊(期)
  • 期刊推荐
论文1v1指导