Finite Automata synthesis from Interactions
Interactions are graphical models representing communication flows between actors. Well-known interaction languages include UML Sequence Diagrams or Message Sequence Charts. Even though interactions allow for concise and intuitive specifications, their use remains limited in formal verification, partly because the subsets of formalized languages often lack expressiveness. As many verification methods, such as model-checking or runtime verification, are routinely available for finite automata, we propose a new approach to generate finite automata from an expressive interaction language with operators such as the concurrent region. Our approach leverages an operational semantics to compute derivatives of an interaction and assimilate them to states of a finite automata. In addition, we use term rewriting to merge states on-the-fly so as to obtain small automata without relying on costly a-posteriori minimization techniques.
Sun 14 AprDisplayed time zone: Lisbon change
11:00 - 12:30 | Automata and applicationsFormaliSE 2024 at Eugénio de Andrade Chair(s): Domenico Bianculli University of Luxembourg | ||
11:00 30mTalk | Contract Automata: A Specification Language for Mode-Based Systems FormaliSE 2024 Alexander Weigl Karlsruhe Institute for Technology, Joshua Bachmeier FZI Forschungszentrum Informatik, Bernhard Beckert Karlsruhe Institute of Technology, Mattias Ulbrich Karlsruhe Institute of Technology | ||
11:30 30mTalk | Finite Automata synthesis from Interactions FormaliSE 2024 Erwan Mahe Université Paris-Saclay, CEA, List, Boutheina Bannour Université Paris-Saclay, CEA, List, Christophe Gaston Université Paris-Saclay, CEA, List, Arnault Lapitre Université Paris-Saclay, CEA, List, Pascale Le Gall CentraleSupelec | ||
12:00 30mTalk | Preprocessing is What You Need: Understanding and Predicting the Complexity of SAT-based Uniform Random Sampling FormaliSE 2024 Olivier Zeyen University of Luxembourg, SnT, Maxime Cordy University of Luxembourg, Luxembourg, Gilles Perrouin Fonds de la Recherche Scientifique - FNRS & University of Namur, Mathieu Acher University of Rennes, France / Inria, France / CNRS, France / IRISA, France |