Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Frederic Lang Connect in order to contact the contributor
Submitted on : Friday, January 30, 2009 - 7:19:14 PM
Last modification on : Tuesday, August 2, 2022 - 4:24:20 AM
Long-term archiving on: : Tuesday, June 8, 2010 - 9:44:53 PM


Files produced by the author(s)


  • HAL Id : inria-00357623, version 1


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



Record views


Files downloads