Paper Info
Title
A livelock freedom analysis for infinite state asynchronous reactive systems
Abstract
We describe an incomplete but sound and efficient livelock freedom test for infinite state asynchronous reactive systems. The method abstracts 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 spuriousness and to refine the abstraction. We illustrate the application of the method to Promela models using our prototype implementation named aLive.
Year
DOI
Venue
2006
10.1007/11817949_6
CONCUR
Keywords
Field
DocType
automated cycle dependency analysis,promela model,homogeneous ip,reactive system,infinite state,homogeneous integer programming problem,method abstract,livelock freedom analysis,necessary condition,efficient livelock freedom test,livelock run,livelock freedom,message passing,polynomial time,dependence analysis,control flow
Asynchronous communication,Computer science,Concurrency,Deadlock,Control flow,Algorithm,Theoretical computer science,Promela,Counterexample,Reactive system,Message passing
Conference
Volume
ISSN
ISBN
4137
0302-9743
3-540-37376-4
Citations 
PageRank 
References 
5
0.43
15
Authors
3
Name
Order
Citations
PageRank
Stefan Leue11199108.55
Alin Stefanescu220917.79
Wei Wei348069.55