基于B方法的内存管理模型的设计-论文.pdf

《基于B方法的内存管理模型的设计-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第45卷第4期河南大学学报(自然科学版)Vo1．45No．42O15年7月JournalofHenanUniversity(NaturalScience)Ju1．2015基于B方法的内存管理模型的设计陈丹敏，孙越，陈志国。(1．河南大学软件学院，河南开封475004；2．开封大学信息工程学院，河南开封4750043．河南大学数据与知识5-程研究所，河南开封475004)摘要：内存管理是操作系统的重要组成部分，一个安全可靠的内存管理程序，对于操作系统的运行十分关键．采用传统软件开发方法开发的内存管理系统，安全性和

2、可靠性得不到很好的保证．为此提出用形式化的B方法开发内存管理系统．首先使用B方法建立了内存管理的形式化模型，利用B工具对该阶段生成的证明义务进行证明，保证系统在初始规范说明层次上的内在一致性和设计的正确性．然后根据B方法分层构造的思想对上一阶段得到的抽象规范模型进行精化．最终得到一个可实现的内存管理模型，该模型更好地保证了系统的一致性和可靠性．关键词：B方法；内存管理；规范；精化；实现中图分类号：TP311．11文献标志码：A文章编号：1003—4978(2015)04—0477—05DesignofMemor

3、yManagementModelBasedonBMethodCHENDanmin，SUNYue，CHENZhiguo。(1．SchoolofSoftware，HenanUniversity，Kang475004，China；2．SchoolofInformationEngineering，KaifengUniversity，Kaifeng475004，China；3．InstituteofDataandKnowledgeEngineering，HenanUniversity，Kaifeng475004，Chin

4、a)Abstract：Memorymanagementisasignificantcomponentofoperatingsystem．Itiscrucialforoperatingsystemtorunwhetheramemorymanagementprogramissafeandreliable．However，memorymanagementsystembasedontraditionalsoftwaredevelopmentmethodscannotlendsupportstohighsecuritya

5、ndreliabilityverywel1．Thepaper，therefore，introducesBmethodtodevelopmemorymanagementsystemsoastoenhanceitssecurityandreliability．Firstofall，thepaperemploysBmethodtodesignaformalmodelofmemorymanagementandthenappliesBtoolstoproveproofobligationsinthisstage，whic

6、hensurescoherenceandcorrectnessintheinitialspecifications．Secondly，theabstractspecificationdesignedinthepreviousstageisfurtherrefinedonbasisofthestep—wisedideaofBmethod．Thepaper，finally，achievesarealizablememorymanagementsystemmodelwhichguaranteescoherencean

7、dreliabilityofthesystembetter．Keywords：Bmethod；memorymanagement；specification；refinement；implementation0引言一个安全可靠的内存管理程序对于操作系统的运行是十分关键的．国内外学者做了大量有关内存管理方面的研究工作，其内容大多是为了提高内存分配效率，减少内存碎片，很少关注内存管理程序本身的安全性和可靠性．内存管理程序采用传统的软件开发方法，无论使用哪种内存管理算法，它的安全性和正确性都得不到很好的保证．因为采用传

8、统软件开发方法开发的内存管理系统，安全性和可靠性只能通过在长期使用中发现和更正错误的方式逐渐“改善”，这使现存的内存管理系统本质上是脆弱的．B方法是一种描收稿日期：2014—07—18基金项目：河南省基础与前沿技术研究计划项目(1223O。41。062)；河南省教育厅自然科学研究项目(12A52O()07)作者简介：陈丹敏(1983一)，女，回族，河南开封人，讲师，硕士．研究方向：形式