Compositional verification for component-based systems and applicationReportar como inadecuado

Compositional verification for component-based systems and application - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Published in: IET Software (ISSN: 17518806), vol. 4, num. 3, p. 181 - 193 Publication date: 2010

The authors present a compositional method for the verification of component-based systems described in a subset of the behaviour-interaction- priority language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants are over-approximations of components' reachability sets. Interaction invariants are global constraints on the states of components involved in interactions. The method has been implemented in the D-Finder tool and has been applied for checking deadlock-freedom. The experimental results on non-trivial examples show that this method allows either to prove deadlock-freedom or to identify very few deadlock configurations that can be analysed by using state-space exploration. © 2010 The Institution of Engineering and Technology.

Keywords: Data transfer ; Space research Reference EPFL-ARTICLE-185008doi:10.1049/iet-sen.2009.0011

Autor: Bensalem, S.; Bozga, M.; Nguyen, T.-H.; Sifakis, J.


Documentos relacionados