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 controller 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. © 2014 Springer-Verlag.
CITATION STYLE
Aiswarya, C., Gastin, P., & Narayan Kumar, K. (2014). Controllers for the verification of communicating multi-pushdown systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704 LNCS, pp. 297–311). Springer Verlag. https://doi.org/10.1007/978-3-662-44584-6_21
Mendeley helps you to discover research relevant for your work.