Dissertation/Thesis Abstract

An Automata-Theoretic Approach to Hardware/Software Co-verification
by Li, Juncao, Ph.D., Portland State University, 2010, 215; 3439215
Abstract (Summary)

Hardware/Software (HW/SW) interfaces are pervasive in computer systems. However, many HW/SW interface implementations are unreliable due to their intrinsically complicated nature. In industrial settings, there are three major challenges to improving reliability. First, as there is no systematic framework for HW/SW interface specifications, interface protocols cannot be precisely conveyed to engineers. Second, as there is no unifying formal model for representing the implementation semantics of HW/SW interfaces accurately, some critical properties cannot be formally verified on HW/SW interface implementations. Finally, few automatic tools exist to help engineers in HW/SW interface development.

In this dissertation, we present an automata-theoretic approach to HW/SW co-verification that addresses these challenges. We designed a co-specification framework to formally specify HW/SW interface protocols; we synthesized a hybrid B¨uchi Automaton Pushdown System, namely Büchi Pushdown System (BPDS), as the unifying formal model for HW/SW interfaces; and we created a co-verification tool, CoVer that implements our model checking algorithms and realizes our reduction algorithms for BPDS.

The application of our approach to the Windows device/driver framework has resulted in the detection of fifteen specification issues. Furthermore, utilizing CoVer, we discovered twelve real bugs in five drivers. These non-trivial findings have demonstrated the significance of our approach in industrial applications.

Indexing (document details)
Advisor: Xie, Fei
Commitee: Ball, Thomas, Li, Fu, Li, Jingke, Singh, Suresh, York, Bryant W.
School: Portland State University
Department: Computer Science
School Location: United States -- Oregon
Source: DAI-B 72/03, Dissertation Abstracts International
Source Type: DISSERTATION
Subjects: Computer science
Keywords: Büchi automaton, Büchi pushdown system (bpds), Co-verification, Hardware, Pushdown system, Software
Publication Number: 3439215
ISBN: 9781124440705
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy
ProQuest