@PhDThesis{ itlic:2006-003,
author = {Therese Berg},
title = {Regular Inference for Reactive Systems},
school = {Department of Information Technology, Uppsala University},
department = {Division of Computer Systems},
year = {2006},
number = {2006-003},
type = {Licentiate thesis},
month = apr,
day = {27},
pages = {132},
abstract = {Models of reactive systems play a central role in many
techniques for verification and analysis of reactive
systems. Both a specification of the system and the
abstract behavior of the system can be expressed in a
formal model. Compliance with the functional parts in the
specification can be controlled in different ways. Model
checking techniques can be applied to a model of the system
or directly to source code. In testing, model-based
techniques can generate test suites from specification. A
bottleneck in model-based techniques is however to
construct a model of the system. This work concerns a
technique that automatically constructs a model of a system
without access to specification, code or internal
structure. We assume that responses of the system to
sequences of input can be observed. In this setting, so
called regular inference techniques build a model of the
system based on system responses to selected input
sequences.
There are three main contributions in this thesis. The
first is a survey on the most well-known techniques for
regular inference. The second is an analysis of Angluin's
algorithm for regular inference on synthesized examples. On
a particular type of examples, with prefix-closed
languages, typically used to model reactive systems, the
required number of input sequences grow approximately
quadratically in the number of transitions of the system.
However, using an optimization for systems with
prefix-closed languages we were able to reduce the number
of required input sequences with about 20\%. The third
contribution is a developed regular inference technique for
systems with parameters. This technique aims to better
handle entities of communications protocols where messages
normally have many parameters of which few determine the
subsequent behavior of the system. Experiments with our
implementation of the technique confirm a reduction of the
required number of input sequences, in comparison with
Angluin's algorithm.}
}