河南大学学报（自然科学版）
河南大學學報（自然科學版）
하남대학학보（자연과학판）
JOURNAL OF HENAN UNIVERSITY(NATURAL SCIENCE)
2015年
4期
477-481
,共5页
B方法%内存管理%规范%精化%实现
B方法%內存管理%規範%精化%實現
B방법%내존관리%규범%정화%실현
B method%memory management%specification%refinement%implementation
内存管理是操作系统的重要组成部分,一个安全可靠的内存管理程序,对于操作系统的运行十分关键.采用传统软件开发方法开发的内存管理系统,安全性和可靠性得不到很好的保证.为此提出用形式化的B方法开发内存管理系统.首先使用B方法建立了内存管理的形式化模型,利用B工具对该阶段生成的证明义务进行证明,保证系统在初始规范说明层次上的内在一致性和设计的正确性.然后根据B方法分层构造的思想对上一阶段得到的抽象规范模型进行精化.最终得到一个可实现的内存管理模型,该模型更好地保证了系统的一致性和可靠性.
內存管理是操作繫統的重要組成部分,一箇安全可靠的內存管理程序,對于操作繫統的運行十分關鍵.採用傳統軟件開髮方法開髮的內存管理繫統,安全性和可靠性得不到很好的保證.為此提齣用形式化的B方法開髮內存管理繫統.首先使用B方法建立瞭內存管理的形式化模型,利用B工具對該階段生成的證明義務進行證明,保證繫統在初始規範說明層次上的內在一緻性和設計的正確性.然後根據B方法分層構造的思想對上一階段得到的抽象規範模型進行精化.最終得到一箇可實現的內存管理模型,該模型更好地保證瞭繫統的一緻性和可靠性.
내존관리시조작계통적중요조성부분,일개안전가고적내존관리정서,대우조작계통적운행십분관건.채용전통연건개발방법개발적내존관리계통,안전성화가고성득불도흔호적보증.위차제출용형식화적B방법개발내존관리계통.수선사용B방법건립료내존관리적형식화모형,이용B공구대해계단생성적증명의무진행증명,보증계통재초시규범설명층차상적내재일치성화설계적정학성.연후근거B방법분층구조적사상대상일계단득도적추상규범모형진행정화.최종득도일개가실현적내존관리모형,해모형경호지보증료계통적일치성화가고성.
