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

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

Application of Model-based Development Method in Multi- Application Smart Cards

Reliability and security are two important aspects for embedded software. A model-based development method was proposed for better development of reliable and secure embedded software. It consists of extracting requirement, establishing abstract model, and step by step refining. Firstly, requirements are extracted from three different views： environmental view, functional view, and property view. During this phase, refinement strategy reflecting model hierarchy is also identified. Then formal methods are adopted in establishing abstract model and proving the established model. Using this well-proved abstract model, model refinement and proof are carried out at following levels of the model hierarchy. Finally, based on the whole established models corresponding to requirements, implementation codes can be automatically generated by related tools. With this model-based development method, requirements and properties of system under development can be identified from abstract to specific and incrementally. Modeling using formal methods can also be carried out in the above way and correctness and availability of models can be guaranteed by feedback mechanism of this method. To illustrate the feasibility of this method, the development of multi-application smart cards is shown as case study. Relevant processes and results are given based on Event-B and Rodin platform.