Learning Mealy Machines with Local Timers

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

Abstract

Active automata learning (AAL) algorithms infer accurate automata models of black box applications, letting developers verify the behavior of increasingly complex real-time systems (RTS). However, learning models of larger RTS often takes very long or is not feasible at all. We introduce Mealy machines with local timers, a new class of Mealy machines that permit multiple location-bound timers and that can be learned efficiently. We design an efficient learning algorithm for them and validate our method across diverse case studies ranging from automotive systems to smart home appliances, where we drastically reduce runtimes compared to the state-of-the-art approach, thus, making AAL available for a wide range of RTS.

Details

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering
EditorsYi Li, Sofiène Tahar
PublisherSpringer Science and Business Media B.V.
Pages47-64
Number of pages18
ISBN (electronic)978-981-99-7584-6
ISBN (print)978-981-99-7583-9
Publication statusPublished - 2023
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14308 LNCS
ISSN0302-9743

Conference

Title24th International Conference on Formal Engineering Methods, ICFEM 2023
Duration21 - 24 November 2023
CityBrisbane
CountryAustralia

Keywords

Keywords

  • active automata learning, real-time systems, timer-based Mealy machines