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 条
  • [1] An automata-theoretic approach to software verification
    Esparza, J
    DEVELOPMENTS IN LANGUAGE THEORY, PROCEEDINGS, 2003, 2710 : 21 - 21
  • [2] AN AUTOMATA-THEORETIC APPROACH TO PROTOCOL VERIFICATION
    VARDI, MY
    LECTURE NOTES IN COMPUTER SCIENCE, 1988, 335 : 73 - 73
  • [3] The automata-theoretic approach to verification of reactive systems
    Chebotarev A.N.
    Cybernetics and Systems Analysis, 2001, 37 (6) : 810 - 819
  • [4] An automata-theoretic approach to the verification of distributed algorithms
    Aiswarya, C.
    Bollig, Benedikt
    Gastin, Paul
    INFORMATION AND COMPUTATION, 2018, 259 : 305 - 327
  • [5] Panel: Hardware/software co-verification
    Smith, G
    Courtoy, M
    Kenefick, M
    DESIGN AUTOMATION CONFERENCE - PROCEEDINGS 1997, 1997, : 484 - 485
  • [6] The RESCUE Approach - Towards Compositional Hardware/Software Co-Verification
    Herber, Paula
    2014 IEEE INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING AND COMMUNICATIONS, 2014 IEEE 6TH INTL SYMP ON CYBERSPACE SAFETY AND SECURITY, 2014 IEEE 11TH INTL CONF ON EMBEDDED SOFTWARE AND SYST (HPCC,CSS,ICESS), 2014, : 721 - 724
  • [7] Hardware/Software Formal Co-Verification using Hardware Verification Techniques
    Nguyen, Minh D.
    Kunz, Wolfgang
    2012 FOURTH INTERNATIONAL CONFERENCE ON COMMUNICATIONS AND ELECTRONICS (ICCE), 2012, : 465 - 470
  • [8] Compositional reasoning for hardware/software co-verification
    Xie, Fei
    Yang, Guowu
    Song, Xiaoyu
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2006, 4218 : 154 - 169
  • [9] The challenge of hardware-software co-verification
    Manolios, Panagiotis
    VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 438 - 447
  • [10] Formal Techniques for Hardware/Software Co-Verification
    Kroening, Daniel
    Srivas, Mandayam
    2013 26TH INTERNATIONAL CONFERENCE ON VLSI DESIGN AND 2013 12TH INTERNATIONAL CONFERENCE ON EMBEDDED SYSTEMS (VLSID), 2013, : LVII - LVIII
12345