@ 2013 - Site Map - Credits

Model-based techniques for verification and calidation of reactive systems, including model checking and model-based testing, have witnessed drastic advances in the last decades. They require formal models that specify the intended behavior of system components, which ideally should be developed during specification and design.  However, constructing models typically requires significant manual effort, implying that in practice often models are not available, or become outdated as a system evolves. Automated support for generating such models would therefore be very useful.

In this tutorial, we will cover techniques for constructing models of components in reactive systems from observations of their external behavior, i.e., using a black-box approach to the generation of models.

This can be done using techniques from automata learning (aka. regular inference). We will cover existing approaches to automata learning, including the assumptions they make on the component that is being investigated. There are close connections between automata learning and the problem of conformance testing for finite automata, which will also be covered. Thereafter we will consider approaches towards extending learning techniques towards enriched automata formalisms, including subclasses of timed automata.