| Autor: |
Antonino, Pedro, Sampaio, Augusto, Woodcock, Jim |
| Rok vydání: |
2022 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
Local analysis has long been recognised as an effective tool to combat the state-space explosion problem. In this work, we propose a method that systematises the use of local analysis in the verification of deadlock freedom for concurrent and distributed systems. It combines a strategy for system decomposition with the verification of the decomposed subsystems via adherence to behavioural patterns. At the core of our work, we have a number of CSP refinement expressions that allows the user of our method to automatically verify all the behavioural restrictions that we impose. We also propose a prototype tool to support our method. Finally, we demonstrate the practical impact our method can have by analysing how it fares when applied to some examples. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
