2022/07/18 by Antonino, Pedro, Sampaio, Augusto, Woodcock, Jim
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Software Engineering (cs.SE)
paper · doi:10.48550/arxiv.2207.08854
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.