Controllers for the Verification of Communicating Multi-Pushdown Systems - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2014

Controllers for the Verification of Communicating Multi-Pushdown Systems

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.
Fichier principal
Vignette du fichier
phase-controller-hal.pdf (501.99 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01057525 , version 1 (22-08-2014)

Identifiers

  • HAL Id : hal-01057525 , version 1

Cite

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⟩
153 View
96 Download

Share

Gmail Facebook X LinkedIn More