Integer Linear Programming-Based Property Checking for Asynchronous Reactive Systems

摘要: Asynchronous reactive systems form the basis of a wide range software systems, for instance in telecommunications domain. It is highly desirable to rigorously show that these are correctly designed. However, traditional formal approaches verification often difficult because asynchronous usually possess extremely large or even infinite state spaces. We propose an integer linear program (ILP) solving-based property checking framework concentrates on local analysis cyclic behavior each individual component system. apply our buffer boundedness and livelock freedom properties, both which undecidable with space. illustrate application proposed methods Promela, input language SPIN model checker. While precision remains issue, we counterexample guided abstraction refinement procedure based discovery dependences among control flow cycles. have implemented prototype tools obtained promising experimental results real-life system models.