Verification of embedded systems is challenging whenever control programs rely on black-box hardware components. Unless precise specifications of such components are fully available, learning their structured models is a powerful enabler for verification, 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 test our approach by combining learning and verification to assess the correctness of grey-box programs relying on FIFO register circuitry to control an elevator system.

Learning for verification in embedded systems: A case study

KHALILI, ALI;NARIZZANO, MASSIMO;TACCHELLA, ARMANDO
2016

Abstract

Verification of embedded systems is challenging whenever control programs rely on black-box hardware components. Unless precise specifications of such components are fully available, learning their structured models is a powerful enabler for verification, 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 test our approach by combining learning and verification to assess the correctness of grey-box programs relying on FIFO register circuitry to control an elevator system.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11567/863943
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact