CAJ | 학술논문

安全性、可靠性是嵌入式软件的重要性质。为了更好地保证开发的嵌入式软件是可靠和安全的，提出了一种基于模型的开发方法学，包括提炼需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面提取需求，同时明确层次化的精化策略；然后利用形式化方法建立抽象模型并对该模型进行形式化验证，在正确的抽象模型上逐层精化，并对每层模型进行验证；最后，基于满足需求的模型，进一步利用工具完成代码自动生成。该方法从抽象到具体，以逐层递增的方式明确被开发系统的需求及性质，进行形式化建模，通过反馈机制确保模型的正确性及可用性。为了证明该方法学的可行性，文章以多应用智能卡为开发实例，基于Event-B方法及Rodin平台给出了实际建模及证明的过程和结果。
안전성、가고성시감입식연건적중요성질。위료경호지보증개발적감입식연건시가고화안전적，제출료일충기우모형적개발방법학，포괄제련수구、건립추상모형급축층정화삼개보취。수선종배경、공능、성질삼개주요방면제취수구，동시명학층차화적정화책략；연후이용형식화방법건립추상모형병대해모형진행형식화험증，재정학적추상모형상축층정화，병대매층모형진행험증；최후，기우만족수구적모형，진일보이용공구완성대마자동생성。해방법종추상도구체，이축층체증적방식명학피개발계통적수구급성질，진행형식화건모，통과반궤궤제학보모형적정학성급가용성。위료증명해방법학적가행성，문장이다응용지능잡위개발실례，기우Event-B방법급Rodin평태급출료실제건모급증명적과정화결과。
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 reifning. Firstly, requirements are extracted from three different views:environmental view, functional view, and property view. During this phase, reifnement 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 reifnement 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 identiifed from abstract to speciifc 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.