Formal Verification of a Railway Interlocking System Using Model Checking