%0 Conference Proceedings
%T Generating Models of Infinite-State Communication Protocols using Regular Inference with Abstraction
%+ Uppsala University
%A Aarts, Fides
%A Jonsson, Bengt
%A Uijen, Johan
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B IFIP International Conference on Testing Software and Systems (ICTSS)
%C Natal, Brazil
%Y Alexandre Petrenko; Adenilso Simão; José Carlos Maldonado
%I Springer
%3 Testing Software and Systems
%V LNCS-6435
%P 188-204
%8 2010-11-08
%D 2010
%R 10.1007/978-3-642-16573-3_14
%Z Computer Science [cs]/Computer Science and Game Theory [cs.GT]Conference papers
%X In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models ofcommunication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control fow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with the protocol simulator ns-2, and generated a model of the SIP component as implemented in ns-2.
%G English
%Z TC 6
%Z WG 6.1
%L hal-00767416
%U https://inria.hal.science/hal-00767416
%~ CONNECT
%~ OPENAIRE
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-LNCS-6435