Model-driven Automaton Learning

OData support
Supervisor:
Tóth Tamás
Department of Measurement and Information Systems

Model-driven engineering is a widely used approach for designing complex cyber-physical systems that is based on the use of high-level system modeling languages. Models can be used for formal verification, which is important for safety-critical systems, e.g. vehicular automation. Moreover, the components of the system can be generated using automatic code generation, including monitoring components that continously check the expected behavior.

However, for numerous software components - mainly legacy and third-party components - there is often no precise specification given. The lack of a formal specification prevents the use of formal verification. Without a specification the expected behavior cannot be monitored. The construction of complex systems is especially challenging.

The goal of my work is to create a specialized algorithm to synthesize formal models of complex systems by observing the events of a black-box system. For this purpose I use state-of-the-art automaton learning algorithms. My goal is to extend these algorithms to focus the learning to efficiently capture the abstraction techniques used in engineering.

The novelty of my approach is a model-based input language and its combination with automaton learning algorithms. I developed a model-based automaton learning framework for synthesizing formal models of software components with complex states. I use a graph query language to focus the learning on important properties of the target component, while excluding unimportant details. Therefore the automaton learning algorithm produces the formal model of the target system. I demonstrate my approach with case studies.

As a result of my work, it is possible to learn the behavior of software components that have not been possible yet due to their complexity or data-dependent behavior. Additionally, the model produced during the learning can be used as documentation, to derive monitors for anomaly detection, or to create test inputs automatically.

Downloads

Please sign in to download the files of this thesis.