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

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

Modeling and development of multi-application smart cards based on Event-B

Event-B is a formal modeling language based on set theory and predicate logic, within which hierarchical models can be established by refinement strategy. A method for applying Event-B to practical industry is proposed, which consists of rewriting requirement, establishing abstract model, and step-by-step refining. Firstly, requirements are rewritten from three different views: environmental view, functional view, and property view. During this phase, refinement strategy reflecting model hierarchy is identified. Secondly, formal methods are adopted to establish abstract model and validate the established model. Using well-proved abstract model, requirement appending, model refining and model validating are carried out at the following levels of the model hierarchy according to the refinement strategy. Finally, based on the whole established models corresponding to requirements, implementation codes can be automatically generated by the related tools. With refinement theory adopted in this method, requirements and properties of system under development can be identified in a refinement way and incrementally. Modeling and verification using formal methods guarantees the correctness of models. To illustrate the feasibility of the method, the development of multi-application smart cards is shown as a case study. Application example of the proposed method in practical modeling and validation is given based on Event-B and Rodin platform.