Using Model Checking to Verify the Logic Module of Flight Control Software

Abstract. Model checking is an important method to verify state machine based system. In this paper, we using PAT, a novel and powerful model checking tool, to verify the logic module of flight control software, which is public available. Conclusions are drawn from the verification and these are valuable for similar researches