Incomplete Property Checking for Asynchronous Reactive Systems

摘要: Asynchronous reactive systems find applications in a wide range of software such as communication protocols, embedded systems, etc. It is highly desirable to rigorously show that these are correctly designed, because correct design vital providing services high quality. However, formal approaches the verification model checking, often difficult usually possess extremely large or even infinite state spaces. In fact, case many interesting problems become undecidable and traditional finite checking techniques cannot be applied those systems. We propose an Integer Linear Program (ILP) solving based framework concentrates on local analysis cyclic behavior each individual component system. This way we avoid exploration huge space More precisely, use automated abstraction transform original system into set control flow cycles over-approximate message passing effects cycles. Then, derive necessary condition for violation considered property further encode ILP problem whose solution represents violating behavior. The infeasibility then establishes satisfaction by Moreover, resulting can checked polynomial time. have our buffer boundedness livelock freedom properties, both which asynchronous with space. On one hand, efficient since it needs not consider exponential number all possible interleavings executions components. Instead, maintains locality reduces polynomial-time solvable problem. other incomplete: either proves property, returns inconclusive verdict “UNKNOWN”. latter case, may satisfied under scrutiny. imprecision comes from potential coarseness abstractions employs. After all, incompleteness inevitable properties check undecidable. While precision remains issue, counterexample guided refinement procedure discovery dependencies among discovered cycle efficiently encoded linear inequalities used augment constraint determination newly added constraints rule out certain spurious violates thus refine abstraction. dependency methods devise also incomplete. means some never eliminated any discover. make applicable two widely modeling languages, namely Promela UML RT, devising tailored code techniques. These address issues concerning specific fea-