| layout | title | sidebar |
|---|---|---|
default |
LearnLib @ ASE 2013 |
learnlib |
{: .rounded}
- When: Tuesday, 12th of November 2013 (Morning)
- Where: ASE 2013, Silicon Valley
- What: 4h tutorial
- Who: Everyone interested in using active automata learning in software engineering
The two main aims of this tutorial are:
- familiarize the attendees with the technique of active automata learning: what it is, how it works, what its abilities and limitations are, and how it can be used in a software engineering context.
- educate the attendees in the usage of the free automata learning library LearnLib, by explaining technical concepts, illustrating common use-cases, and specifically emphasize how it’s generic architecture can be used to easily integrate it in their software.
Below you find a release of LearnLib specifically prepared for this tutorial. Downloading it and setting it up in your preferred IDE before the tutorial is recommended. Please contact us if you have trouble setting up LearnLib.
- [Libraries (learnlib-ase2013-libraries.zip)]({{ 'assets/files/learnlib-ase2013-libraries.zip' | relative_url}}): This archive contains the libraries (JAR files) required for using LearnLib.
- [JavaDocs (learnlib-ase2013-javadoc.zip)]({{ 'assets/files/learnlib-ase2013-javadoc.zip' | relative_url}}): This archive contains JAR files with the corresponding Javadoc documentation for LearnLib and AutomataLib.
This lecture will provide an introduction to active learning of Mealy machines, an automata model particularly suited for modeling the behavior of realistic reactive systems. Active learning is characterized by its alternation of an exploration phase and a testing phase. During exploration phases so-called membership queries are used to construct hypothesis models of a system under learning. In testing phases so-called equivalence queries are used to compare respective hypothesis models to the actual system. These two phases are iterated until a valid model of the target system is produced. We will stepwise elaborate on this simple algorithmic pattern, its underlying correctness arguments, its limitations, and, in particular, methods to overcome apparent hurdles for practical application. This comprises ways to address real world applications, as well as the treatment of infinite data domains by abstraction refinement.
LearnLib is a framework for model-based construction of dedicated learning solutions on the basis of extensible component libraries, which comprise various methods and tools to deal with realistic systems including test harnesses, reset mechanisms and abstraction/refinement techniques. The tutorial will comprise realistic experimentation, like test-based extraction of the user process from Web applications. The goal is to provide participants with hands-on experience with a revolutionary new approach to system-level dynamic validation.
Edit 2013/11/12: [LearnLib Slides]({{ 'assets/pdf/learnlib.pdf' | relative_url}})
Most systems in use today lack adequate specification or make use of underspecified or even unspecified components. In fact, the much propagated component-based software design style typically leads to under-specified systems, as most libraries only provide partial specifications of their components. Moreover, typically, revisions and last minute changes hardly enter the system specification. This hampers the application of any kind of formal validation techniques like model based testing or model checking. Active Automata Learning has been proposed as a technique to apply model-based techniques in scenarios where models are either unavailable or possibly incomplete or erroneous.
Characteristic for active learning automata learning is its iterative alternation between a "testing" phase for completing the transitions relation of the model aggregated from the observed behavior, and an equivalence checking phase, which either signals success or provides a counterexample, i.e., a behavior that distinguishes the current aggregate (called hypothesis) from the system to be learned.
This technique, which originally has been introduced for dealing with formal languages, works very well also for reactive systems, whenever the chosen interpretation of the stimuli and reactions leads to a deterministic language. For such systems, active automata learning can be regarded as regular extrapolation, i.e., as a technique to construct the best regular model being consistent with the observations made.
In this tutorial we present LearnLib, a free, open source Java library for active automata learning and show how LearnLib can be used to infer models of software systems. The open source version of LearnLib is the result of 10 years of research and development: It is the result of a redesign and reimplementation of the closed source LearnLib, which has originally been designed to systematically build finite state machine models of unknown real world systems (Telecommunications Systems, Web Services, etc.).
A decade of experience in the field led to the construction of a platform for experimentation with different learning algorithms as well as for statistically analyzing their characteristics in terms of learning effort, run time and memory consumption. More importantly, LearnLib provides a lot of infrastructure, enabling easy application in the domain of software systems.
Falk Howar is a Postdoctoral Fellow at Carnegie Mellon University, Silicon Valley. He received his Ph.D. from TU Dortmund in Germany, where he has worked in Bernhard Steffen’s Programming Systems group. His research focuses on using active automata learning techniques for the ex-post construction of models of software systems. Falk is one of the maintainers of LearnLib and has contributed to LearnLib for the past 5 years.
Malte Isberner is a PhD candidate in the group of Bernhard Steffen. He currently works as a research programmer at Carnegie Mellon University, Silicon Valley, where he works on the verification of flight critical systems. Malte is one of the maintainers of LearnLib.
Bernhard Steffen became 1993 Full Professor for Programming Systems at the University of Passau. He holds the Chair of Programming Systems and Compiler Construction at the University of Dortmund. He is author of over 200 refereed papers concerning various aspects of formal (verification) methods and tools for program analysis, compiler optimization, model generation, testing, and service-oriented software development. He is founder and Editor in Chief of Software Tools for Technology Transfer (STTT), Springer Verlag, and co-founder and Steering Committee Member of TACAS, the Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems. In 2004 he co-founded ISoLA (Int. Symposium on Leveraging Applications of Formal Methods, Verification and Validation).