Disk Scheduling Software Development Based On B Method
Qinan Li · Journal of Gansu Sciences · 2008
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 B toolkit.The correctness of the B model and of the refinement process is guaranteed by the B method.Our study shows using B method can develop the highly reliable and reusable disk scheduling software.