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

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