Efficient verification of comcurrent systems using local analysis based approximations and SAT solving
This work develops a type of local analysis that can prove concurrent systems deadlock free. As opposed to examining the overall behaviour of a system, local analysis consists of examining the behaviour of small parts of the system to yield a given property. We analyse pairs of interacting component...
| मुख्य लेखकों: | , , |
|---|---|
| स्वरूप: | Journal article |
| प्रकाशित: |
Springer
2019
|
| _version_ | 1826292966850822144 |
|---|---|
| author | Antonino, P Gibson-Robinson, T Roscoe, A |
| author_facet | Antonino, P Gibson-Robinson, T Roscoe, A |
| author_sort | Antonino, P |
| collection | OXFORD |
| description | This work develops a type of local analysis that can prove concurrent systems deadlock free. As opposed to examining the overall behaviour of a system, local analysis consists of examining the behaviour of small parts of the system to yield a given property. We analyse pairs of interacting components to approximate system reachability and propose a new sound but incomplete/approximate framework that checks deadlock and local-deadlock freedom. By replacing exact reachability by this approximation, it looks for deadlock (or local-deadlock) candidates, namely, blocked (locally-blocked) system states that lie within our approximation. This characterisation improves on the precision of current approximate techniques. In particular, it can tackle non-hereditary deadlock-free systems, namely, deadlock-free systems that have a deadlocking subsystem. These are neglected by most approximate techniques. Furthermore, we demonstrate how SAT checkers can be used to efficiently implement our framework, which, typically, scales better than current techniques for deadlock-freedom analysis. This is demonstrated by a series of practical experiments. |
| first_indexed | 2024-03-07T03:22:50Z |
| format | Journal article |
| id | oxford-uuid:b8030af3-8fa5-401e-849a-e63a65b00ddf |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:22:50Z |
| publishDate | 2019 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:b8030af3-8fa5-401e-849a-e63a65b00ddf2022-03-27T04:52:57ZEfficient verification of comcurrent systems using local analysis based approximations and SAT solvingJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:b8030af3-8fa5-401e-849a-e63a65b00ddfSymplectic Elements at OxfordSpringer2019Antonino, PGibson-Robinson, TRoscoe, AThis work develops a type of local analysis that can prove concurrent systems deadlock free. As opposed to examining the overall behaviour of a system, local analysis consists of examining the behaviour of small parts of the system to yield a given property. We analyse pairs of interacting components to approximate system reachability and propose a new sound but incomplete/approximate framework that checks deadlock and local-deadlock freedom. By replacing exact reachability by this approximation, it looks for deadlock (or local-deadlock) candidates, namely, blocked (locally-blocked) system states that lie within our approximation. This characterisation improves on the precision of current approximate techniques. In particular, it can tackle non-hereditary deadlock-free systems, namely, deadlock-free systems that have a deadlocking subsystem. These are neglected by most approximate techniques. Furthermore, we demonstrate how SAT checkers can be used to efficiently implement our framework, which, typically, scales better than current techniques for deadlock-freedom analysis. This is demonstrated by a series of practical experiments. |
| spellingShingle | Antonino, P Gibson-Robinson, T Roscoe, A Efficient verification of comcurrent systems using local analysis based approximations and SAT solving |
| title | Efficient verification of comcurrent systems using local analysis based approximations and SAT solving |
| title_full | Efficient verification of comcurrent systems using local analysis based approximations and SAT solving |
| title_fullStr | Efficient verification of comcurrent systems using local analysis based approximations and SAT solving |
| title_full_unstemmed | Efficient verification of comcurrent systems using local analysis based approximations and SAT solving |
| title_short | Efficient verification of comcurrent systems using local analysis based approximations and SAT solving |
| title_sort | efficient verification of comcurrent systems using local analysis based approximations and sat solving |
| work_keys_str_mv | AT antoninop efficientverificationofcomcurrentsystemsusinglocalanalysisbasedapproximationsandsatsolving AT gibsonrobinsont efficientverificationofcomcurrentsystemsusinglocalanalysisbasedapproximationsandsatsolving AT roscoea efficientverificationofcomcurrentsystemsusinglocalanalysisbasedapproximationsandsatsolving |