Controllers for the Verification of Communicating Multi-Pushdown Systems

Cyriac Aiswarya 1, * Paul Gastin 2, 3 K. Narayan Kumar 4
* Corresponding author
3 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : 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.
Document type :
Conference papers
25th International Conference on Concurrency Theory (CONCUR'14),, 2014, Rome, Italy. Springer, LNCS 8704, pp.297-311, 2014
Liste complète des métadonnées

Cited literature [18 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01057525
Contributor : C. Aiswarya <>
Submitted on : Friday, August 22, 2014 - 11:50:02 PM
Last modification on : Thursday, January 11, 2018 - 6:23:37 AM
Document(s) archivé(s) le : Thursday, November 27, 2014 - 1:55:54 PM

File

phase-controller-hal.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01057525, version 1

Collections

Citation

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. Springer, LNCS 8704, pp.297-311, 2014. 〈hal-01057525〉

Share

Metrics

Record views

264

Files downloads

105