Controllers for the Verification of Communicating Multi-Pushdown Systems

Cyriac Aiswarya (1) , Paul Gastin (2, 3) , K. Narayan Kumar (4)

1 DIT-UPPSALA - Department of Information Technology
2 LSV - Laboratoire Spécification et Vérification [Cachan]
3 MEXICO - Modeling and Exploitation of Interaction and Concurrency
4 Chennai Mathematical Institute [Inde]

Multi-pushdowns communicating via queues are formal models of multi-threaded programs communicating via channels. They are turing powerful and much of the work on their verification has focussed on under-approximation techniques. Any error detected in the under-approximation implies an error in the system. However the successful verification of the under-approximation is not as useful if the system exhibits unverified behaviours. Our aim is to design controllers that observe/restrict the system so that it stays within the verified under-approximation. We identify some important properties that a good con- troller should satisfy. We consider an extensive under-approximation class, construct a distributed controller with the desired properties and also establish the decidability of verification problems for this class.

Mots clés: Verification; Distributed controller; Message sequence charts Multi-pushdown systems

Domaines: Logique en informatique [cs.LO]

Cyriac Aiswarya, Paul Gastin, K. Narayan Kumar. Controllers for the Verification of Communicating Multi-Pushdown Systems. 25th International Conference on Concurrency Theory (CONCUR'14),, 2014, Rome, Italy. pp.297-311. ⟨hal-01057525⟩