基于B方法的磁盘调度软件开发  

Disk Scheduling Software Development Based On B Method

作　　者：李启南[1] 

机构地区：[1]兰州交通大学电子与信息工程学院,甘肃兰州730070

出　　处：《甘肃科学学报》2008年第2期120-123,共4页Journal of Gansu Sciences

摘　　要：使用B方法对磁盘调度建立了B模型,对所建模型进行了活性证明,然后遵循B模型逐步精化的开发规则,利用B方法的精化正确性验证功能,得到系统的可靠实现模型,最后借助B工具自动生成C代码.研究表明使用B方法能够开发出高可靠性的可复用高效磁盘调度软件.The B model of disk scheduling is built by using B method and its liveness is proved. Then in the environment of B method, the verified B model is refined step by step into an implementation model and finally translated into the source C code with the aid of 13 toolkit. The correctness of the B model and of the refinement process is guararnteed by the B method. Our study shows using B method can develop the highly reliable and reusable disk scheduling software.

关 键 词：形式化方法 B方法 磁盘调度 抽象机 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]