Automatic Interface Generation for Compositional Verification

Sandro Spina 1 Gordon Pace 1 Frederic Lang 2
2 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Compositional verification, the incremental generation and composition of the state graphs of individual processes to produce the global state graph, tries to address the state explosion problem for systems of communicating processes. The main problem with this approach is that intermediate state graphs are sometimes larger than the overall global system. To overcome this problem, interfaces [JL97], and refined interfaces [Lan06], which take into account a system's environment have been developed. The number of states of these interfaces plays a vital role in their applicability in terms of computational complexity, which is proportional to the number of states in the interface. The direct use of complete subcomponents of the global system as interfaces, thus usually fails, and it is up to the system designer to describe smaller interfaces to be used in the reduction. To avoid having to verify the correctness of such manually generated interfaces, we propose automatic techniques to generate correct interfaces. The challenge is to produce interfaces small in size, yet effective for reduction. In this paper, we present techniques to structurally produce language over-approximations of labelled transition systems which can be used as correct interfaces, and combine them with refined interfaces. The techniques are applied to a number of case-studies, analysing the trade-off between interface size and effectiveness.
Type de document :
Communication dans un congrès
CSAW, Nov 2007, Valletta, Malta. 2007
Liste complète des métadonnées
Contributeur : Frederic Lang <>
Soumis le : vendredi 30 janvier 2009 - 19:19:14
Dernière modification le : jeudi 11 octobre 2018 - 08:48:03
Document(s) archivé(s) le : mardi 8 juin 2010 - 21:44:53


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00357623, version 1



Sandro Spina, Gordon Pace, Frederic Lang. Automatic Interface Generation for Compositional Verification. CSAW, Nov 2007, Valletta, Malta. 2007. 〈inria-00357623〉



Consultations de la notice


Téléchargements de fichiers