The application and verification of Banker´s algorithm for deadlock avoidance in Flexible Manufacturing System with SPIN

Author

GANG, XU ; WU, ZHIMlNG

Author_Institution

Shanghai Jiaotong Univ., China

Volume

2

fYear

2003

fDate

14-19 Sept. 2003

Firstpage

2165

Abstract

This paper presents a method for deadlock avoidance algorithm used in Flexible Manufacturing System(FMS). This method is an improvement of the Banker algorithm. The Banker algorithm is commonly used in the operating system (OS), but some improvement will have to be made on the algorithm if this algorithm is used in FMS. The difference between the process in operating system and the job in the FMS is fully discussed. Based on this difference, the improvement is made. In order to improve the algorithm, formal methods are adopted to the manufacturing systems. The simulation model is translated into a format suitable for model checking. That is, the model is written into PROMELA, the input language of the popular model checker SPIN. After that, SPIN is used to verify that the model does not have deadlock.

Keywords

computer aided production planning; flexible manufacturing systems; operating systems (computers); resource allocation; scheduling; Banker algorithm verification; FMS; PROMELA; communicating sequential processes; deadlock avoidance policy; flexible manufacturing system; operating system; popular model checker; production planning; resource allocation; resource allocation algorithm; Flexible manufacturing systems; Job shop scheduling; Manufacturing automation; Manufacturing processes; Manufacturing systems; Operating systems; Production; Pulp manufacturing; Resource management; System recovery;

fLanguage

English

Publisher

ieee

Conference_Titel

Robotics and Automation, 2003. Proceedings. ICRA '03. IEEE International Conference on

ISSN

1050-4729

Print_ISBN

0-7803-7736-2

Type

conf

DOI

10.1109/ROBOT.2003.1241914

Filename

1241914