Survey: Linear Temporal Logic Symbolic Model Checking

摘要: We are seeing an increased push in the use of formal verification techniques safety-critical software and hardware practice. Formal has been successfully used to verify systems such as air traffic control, airplane separation assurance, autopilot, CPU designs, life-support systems, medical equipment (such devices which administer radiation), many other ensure human safety. This survey provides a perspective on technique linear temporal logic (LTL) symbolic model checking, from its history evolution leading up state-of-the-art. unify research 1977 2009, providing complete end-to-end analysis embracing users' by applying each step real-life aerospace example. include in-depth examination algorithms underlying model-checking procedure, show proofs important theorems, point directions ongoing research. The primary focus is checking using LTL specifications, though approaches briefly discussed compared LTL.