Verification Of Data-Intensive Embedded Systems

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.