Verification of data-intensive embedded systems
- Massimo Narizzano
- Armando Tacchella
(2023). ECMS 2023, 37th Proceedings
Edited by: Enrico Vicario, Romeo Bandinelli, Virginia Fani, Michele Mastroianni, European Council for Modelling and Simulation.
ISSN: 2522-2422 (ONLINE)
ISSN: 2522-2414 (PRINT)
ISSN: 2522-2430 (CD-ROM)
ISBN: 978-3-937436-79-1 (CD) Communications of the ECMS Volume 37, Issue 1, June 2023, Florence, Italy June 20th – June 23rd, 2023
Massimo narizzano, Armando tacchella (2023). Verification of Data-Intensive Embedded Systems, ECMS 2023, Proceedings Edited by: Enrico Vicario, Romeo Bandinelli, Virginia Fani, Michele Mastroianni, European Council for Modelling and Simulation. doi:10.7148/2023-0521
Verification of embedded software relying on black-box hardware is challenging whenever precise specifications of the underlying systems are incomplete or not available. Learning structured hardware models is a powerful enabler of verification in these cases, but it can be inefficient when the system to be learned is data-intensive rather than control-intensive. We contribute a methodology to attack this problem based on a specific class of automata which are well suited to model systems wherein data paths are known to be decoupled from control paths. We show the effectiveness of our approach by combining learning and verification to assess the correctness of embedded programs relying on FIFO register circuitry to control an elevator system.