关键词: 智能卡, Event-B, 精化, 定理证明

Abstract:

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.

Key words: smart card;EventB;refinement;theory proof