Generating models of infinite-state communication protocols using regular inference with abstraction

Abstract. In order to facilitate model-based verification and valida-tion, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference tech-niques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant im-pact on control flow 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 in-formation 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.