Active Automata Learning with Adaptive Distinguishing Sequences

The ever-growing complexity of today's soft-and hardware makes testing both an indispensable necessityand a challenging task. At the given scale, manual testing is unfeasible, which raises the urge for automated approaches. At the same time, the ongoing digitalization ofsecurity-and safety-centric applications requires exhaustive verification of key properties. A field of research that tackles these problems and has yielded sophisticating results is that of model-based testing [Bro 05] and model checking [BK08]. Formal verification methods, depending on the scenario, allow the automated generation of tests or the automated evaluation of test properties. Being based on formal models, a successful verification is also able to provably guarantee certain properties of the system under testing. Key to a successful application of these techniques is a formal specification of the target system. This requirement, however, poses a problem to many real-world applications: Thelack of formal specifications for software or hardware hinders the employment of formal verification methods. Creating formal specifications for soft-or hardware components is not only a tedious task but also prone to errors.