基于模型的开发方法在多应用智能卡中的应用

• 作者: 朱晓冉 章玥 郭建
• 来源期刊: 信息网络安全
• 学科: 工学
• 关键词: 智能卡 Event-B 形式化方法 定理证明
• 年，卷（期）: 2013,（12）
• 所属期刊栏目: 理论研究
• 页码范围: 75-79
• 页数: 5页
• 分类号: TP309
• 字数: 5117字
• 语种: 中文
• DOI: 10.3969/j.issn.1671-1122.2013.12.019

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭建	华东师范大学教育部软硬件协同设计技术与应用工程研究中心	5	11	2.0	3.0
3	章玥	华东师范大学教育部软硬件协同设计技术与应用工程研究中心	8	54	2.0	7.0
9	朱晓冉	华东师范大学教育部软硬件协同设计技术与应用工程研究中心	2	4	2.0	2.0