基于Event-B方法的多应用智能卡的建模与开发

• 作者: 朱晓冉 朱晶洋 汤家华 王文君 章玥 郭建 陈峻念
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 智能卡 Event-B 精化 定理证明
• 年，卷（期）: 2014,（10）
• 页码范围: 1943-1951
• 页数: 9页
• 分类号: TP301.1
• 字数: 6418字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2014.10.017

摘要

Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型.提出了如何将Event-B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤.首先从环境、功能、性质三个主要方面重写需求,明确精化策略;然后利用形式化方法建立抽象模型并验证该模型;最后,在正确的抽象模型上按照精化策略添加需求、逐层精化,并对每层模型进行验证,基于满足需求的最后一层模型,可进一步利用工具完成代码自动生成.该方法学采用精化理论,以逐层递增的方式明确被开发系统的需求及性质,并进行形式化建模与验证,确保了模型的正确性.为了说明该方法学的可行性,以真正工业界的多应用智能卡为实例,基于Event B方法及其工具平台Rodin给出了该方法在实际建模及验证过程中的应用.