Sciweavers

Share
CONCUR
2006
Springer

A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems

9 years 2 months ago
A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems
We describe an incomplete but sound and efficient livelock freedom test for infinite state asynchronous reactive systems. The method s a system into a set of simple control flow cycles labeled with their message passing effects. From these cycles, it constructs a homogeneous integer programming problem (IP) encoding a necessary condition for the existence of livelock runs. Livelock freedom is assured by the infeasibility of the generated homogeneous IP, which can be checked in polynomial time. In the case that livelock freedom cannot be proved, the method proposes a counterexample given as a set of cycles. We apply an automated cycle dependency analysis to counterexamples to check their ness and to refine the abstraction. We illustrate the application of the method to Promela models using our prototype implementation named aLive.
Stefan Leue, Alin Stefanescu, Wei Wei
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CONCUR
Authors Stefan Leue, Alin Stefanescu, Wei Wei
Comments (0)
books