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

发布时间：2018-07-23 08:10

【摘要】：Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型。提出了如何将Event-B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面重写需求,明确精化策略;然后利用形式化方法建立抽象模型并验证该模型;最后,在正确的抽象模型上按照精化策略添加需求、逐层精化,并对每层模型进行验证,基于满足需求的最后一层模型,可进一步利用工具完成代码自动生成。该方法学采用精化理论,以逐层递增的方式明确被开发系统的需求及性质,并进行形式化建模与验证,确保了模型的正确性。为了说明该方法学的可行性,以真正工业界的多应用智能卡为实例,基于Event-B方法及其工具平台Rodin给出了该方法在实际建模及验证过程中的应用。
[Abstract]:Event-B is a formal system language based on set theory and predicate logic. This paper presents a method of applying Event-B to the practical industrial field, which includes three steps: rewriting requirements, building abstract model and refining layer by layer. Firstly, the requirements are rewritten from three main aspects: environment, function and nature. Then the abstract model is established by formal method and the model is verified. Finally, the requirements are added to the correct abstract model according to the refined strategy. Layer by layer refinement and verification of each layer model, based on the last layer model to meet the requirements, we can further use tools to complete the automatic generation of code. The methodology uses the refined theory to clarify the requirements and properties of the developed system in a hierarchical incremental manner, and formalizes and verifies the model to ensure the correctness of the model. In order to illustrate the feasibility of the methodology, the application of this method in the process of modeling and verification is given based on the Event-B method and its tool platform Rodin, taking the real industrial multi-application smart card as an example.
【作者单位】：华东师范大学教育部软硬件协同设计技术与应用工程研究中心;信息网络安全公安部重点实验室;上海市社会保障卡服务中心;
【基金】：国家自然科学基金资助项目(91118008) 国家973计划资助项目(2011CB302904) 上海市科委资助项目(12511504205) 信息网络安全公安部重点实验室开放课题资助项目(C12604) 上海高校知识服务平台-可信物联网产学研联合研发中心(筹)资助项目
【分类号】：TP368.1

【参考文献】