Verification of Modular Systems with Unknown Components Combining Testing and Inference

Autor: Groz, Roland, Li, Keqin, Petrenko, Alexandre
Přispěvatelé: Drakkar, Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), SAP Research (SAP Research), Centre de Recherche Informatique de Montréal = Computer Research Institute of Montréal (CRIM), LIG, Validation de Systèmes, Composants et Objets logiciels (VASCO), SAP Research [Sophia Antipolis], SAP Research, EU FP7 Project no. 257876, 'SPaCIoS: Secure Provision and Consumption in the Internet of Services' (www.spacios.eu), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), Centre de Recherche Informatique de Montréal (CRIM)
Jazyk: angličtina
Rok vydání: 2012
Předmět:
Zdroj: [Research Report] RR-LIG-028, LIG. 2012
ISSN: 2105-0422
Popis: Les rapports de recherche du LIG - ISSN: 2105-0422; Verification of a modular system composed of communicating components is a difficult problem, especially when the formal specifications, i.e., models of the components are not available. Conventional testing techniques are not efficient in detecting erroneous interactions of components because interleavings of internal events are difficult to reproduce in a modular system. The problem of detecting intermittent errors and other compositional problems in the absence of components’ models is addressed in this paper. A method to infer a controllable approximation of communicating components through testing is elaborated. The inferred finite state models of components are used to detect compositional problems in the system through reachability analysis. To confirm a flaw in a particular component, a witness trace is used to construct a test applied to the component in isolation. The models are refined at each analysis step thus making the approach iterative.
Databáze: OpenAIRE