Portal de Periódicos da CAPES

An Automata-Theoretic Approach to Hardware/Software Co-verification

2010; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-642-12029-9_18

1611-3349

Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin, Con McGarvey,

Security and Verification in Computing

In this paper, we present an automata-theoretic approach to Hardware/ Software (HW/SW) co-verification. We designed a co-specification framework describing HW/SW systems; synthesized a hybrid Büchi Automaton Pushdown System model for co-verification, namely Büchi Pushdown System (BPDS), from the co-specification; and built a software tool for deciding reachability of BPDS models. Using our approach, we succeeded in co-verifying the Windows driver and the hardware model of the PIO-24 digital I/O card, finding a previously undiscovered software bug. In addition, our experiments have shown that our co-verification approach performs well in terms of time and memory usages.