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

被引：0
|
作者：
Li, Juncao [1 ]
Xie, Fei [1 ]
Ball, Thomas [2 ]
Levin, Vladimir [2 ]
McGarvey, Con [2 ]
机构：
[1] Portland State Univ, Dept Comp Sci, Portland, OR 97207 USA
[2] Microsoft Corp, Redmond, WA 98052 USA
来源：
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS | 2010年 / 6013卷
基金：
美国国家科学基金会;
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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 Btichi Automaton Pushdown System model for co-verification, namely Btichi 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.
引用
收藏
页码：248 / +
页数：2
相关论文
共 50 条
  • [41] Re-useable hardware software co-verification of IP blocks
    Bruce, A
    Goodenough, J
    ELECTRONIC ENGINEERING DESIGN, 2002, 74 (908): : 20 - +
  • [42] Co-Verification Approach to Control Software Program for CPS
    Zhang Y.
    Dong Y.-W.
    Feng W.-L.
    Huang M.-X.
    Ruan Jian Xue Bao/Journal of Software, 2017, 28 (05): : 1144 - 1166
  • [43] Hardware and software co-verification from security perspective in SoC platforms
    Chen, Kejun
    Sun, Lei
    Deng, Qingxu
    JOURNAL OF SYSTEMS ARCHITECTURE, 2022, 122
  • [44] Software Hardware Co-Simulation and Co-Verification in Safety Critical System Design
    Shi, Jin
    Liu, Weichao
    Jiang, Ming
    Che, HuiJun
    Chen, Lei
    2013 IEEE INTERNATIONAL CONFERENCE ON INTELLIGENT RAIL TRANSPORTATION (ICIRT), 2013, : 71 - 74
  • [45] Hardware/software security co-verification and vulnerability detection: An information flow perspective
    Qin, Maoyuan
    Zhu, Jiacheng
    Mao, Baolei
    Hu, Wei
    INTEGRATION-THE VLSI JOURNAL, 2024, 94
  • [46] Efficient Reachability Analysis of Buchi Pushdown Systems for Hardware/Software Co-verification
    Li, Juncao
    Xie, Fei
    Ball, Thomas
    Levin, Vladimir
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 339 - +
  • [47] Software and Hardware Co-verification Technology Based on Virtual Prototyping of RF SoC
    Gao, Yuhan
    Liu, Lintao
    Du, Haoming
    Gong, Qiao
    2018 IEEE INTERNATIONAL CONFERENCE ON COMPUTER AND COMMUNICATION ENGINEERING TECHNOLOGY (CCET), 2018, : 244 - 247
  • [48] Hardware/software security co-verification and vulnerability detection: An information flow perspective
    Qin, Maoyuan
    Zhu, Jiacheng
    Mao, Baolei
    Hu, Wei
    Integration, 2024, 94
  • [49] Automata-theoretic approach to planning for temporally extended goals
    De Giacomo, G
    Vardi, MY
    RECENT ADVANCES IN AI PLANNING, 2000, 1809 : 226 - 238
  • [50] The hardware-software co-design and co-verification of SoC for an embedded home gateway
    Guo, Bing
    Shen, Yan
    Zhang, ChuanWu
    SEC 2008: PROCEEDINGS OF THE FIFTH IEEE INTERNATIONAL SYMPOSIUM ON EMBEDDED COMPUTING, 2008, : 288 - +
12345