摘要
使用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.
出处
《甘肃科学学报》
2008年第2期120-123,共4页
Journal of Gansu Sciences
关键词
形式化方法
B方法
磁盘调度
抽象机
formal method
B method
disk scheduling
abstract machine
