A static analysis framework for livelock freedom in CSP

DOI10.2168/LMCS-9(3:24)2013MaRDI QIDQ2848369zbMATH OpenOpenAlexFDO

Authors Joël Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell

Publication date 26 September 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1304.7394

zbMATH Keywords

communicating sequential processesdivergencefairnesssymbolic static analysis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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.

Recommendations

• Static Livelock Analysis in CSP
• Compositional and local livelock analysis for CSP
• A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems
• scientific article; zbMATH DE number 3890704
• scientific article; zbMATH DE number 1863165

Cited in

(6)

• Compositional and local livelock analysis for CSP
• Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
• Static Livelock Analysis in CSP
• Rigorous development of component-based systems using component metadata and patterns
• scientific article; zbMATH DE number 3890704 (Why is no real title available?)
• A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems

Describes a project that uses

Uses Software

• PRISM

This page was built for publication: A static analysis framework for livelock freedom in CSP

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848369)