Static livelock analysis in CSP
In a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are said to diverge or livelock. In this paper we show how it is possible to conservatively classify processes as livelock-free...
| Hlavní autoři: | , , , |
|---|---|
| Médium: | Kniha |
| Vydáno: |
2011
|
| _version_ | 1826258685015359488 |
|---|---|
| author | Ouaknine, J Palikareva, H Roscoe, A Worrell, J |
| author_facet | Ouaknine, J Palikareva, H Roscoe, A Worrell, J |
| author_sort | Ouaknine, J |
| collection | OXFORD |
| description | In a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are said to diverge or livelock. In this paper we show how it is possible to conservatively classify processes as livelock-free through a static analysis of their syntax. In particular, we present a collection of rules, based on the inductive structure of terms, which guarantee livelock-freedom of the denoted process. This gives rise to an algorithm which conservatively flags processes that can potentially livelock. We illustrate our approach by applying both BDD-based and SAT-based implementations of our algorithm to a range of benchmarks, and show that our technique in general substantially outperforms the model checker FDR whilst exhibiting a low rate of inconclusive results. |
| first_indexed | 2024-03-06T18:37:52Z |
| format | Book |
| id | oxford-uuid:0be6a4f4-6756-4d25-bbb6-a2142739cba3 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:37:52Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | oxford-uuid:0be6a4f4-6756-4d25-bbb6-a2142739cba32022-03-26T09:31:51ZStatic livelock analysis in CSPBookhttp://purl.org/coar/resource_type/c_2f33uuid:0be6a4f4-6756-4d25-bbb6-a2142739cba3Department of Computer Science2011Ouaknine, JPalikareva, HRoscoe, AWorrell, JIn a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are said to diverge or livelock. In this paper we show how it is possible to conservatively classify processes as livelock-free through a static analysis of their syntax. In particular, we present a collection of rules, based on the inductive structure of terms, which guarantee livelock-freedom of the denoted process. This gives rise to an algorithm which conservatively flags processes that can potentially livelock. We illustrate our approach by applying both BDD-based and SAT-based implementations of our algorithm to a range of benchmarks, and show that our technique in general substantially outperforms the model checker FDR whilst exhibiting a low rate of inconclusive results. |
| spellingShingle | Ouaknine, J Palikareva, H Roscoe, A Worrell, J Static livelock analysis in CSP |
| title | Static livelock analysis in CSP |
| title_full | Static livelock analysis in CSP |
| title_fullStr | Static livelock analysis in CSP |
| title_full_unstemmed | Static livelock analysis in CSP |
| title_short | Static livelock analysis in CSP |
| title_sort | static livelock analysis in csp |
| work_keys_str_mv | AT ouakninej staticlivelockanalysisincsp AT palikarevah staticlivelockanalysisincsp AT roscoea staticlivelockanalysisincsp AT worrellj staticlivelockanalysisincsp |