Abstract: Model checking is a powerful technique to analyse and verify system automatically. Part of the source code of Linux interprocess communication was chosen to be analysed and formalized modeled, then these models were translated into PROMELA, the input lang

Key words: Model checking, Linux, Interprocess communication, Spin, System verification