Modular verification of software components in C

被引:108
|
作者
Chaki, S [1 ]
Clarke, E [1 ]
Groce, A [1 ]
Jha, S [1 ]
Veith, H [1 ]
机构
[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
关键词
D O I
10.1109/ICSE.2003.1201217
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We present a new methodology for automatic verification of C programs against finite state machine specifications. Our approach is compositional, naturally enabling us to decompose the verification of large software systems into subproblems of manageable complexity. The decomposition reflects the modularity in the software design. We use weak simulation as the notion of conformance between the program and its specification. Following the abstract-verify-refine paradigm, our tool MAGIC first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, simulation is checked via a reduction to Boolean satisfiability. MAGIC is able to interface with several publicly available theorem provers and SAT solvers. We report experimental results with procedures from the Linux kernel and the OpenSSL toolkit.
引用
收藏
页码:385 / 395
页数:11
相关论文
共 50 条
  • [1] Modular verification of software components in C
    Chaki, S
    Clarke, EM
    Groce, A
    Jha, S
    Veith, H
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2004, 30 (06) : 388 - 402
  • [2] Engineering and Employing Reusable Software Components for Modular Verification
    Welch, Daniel
    Sitaraman, Murali
    [J]. MASTERING SCALE AND COMPLEXITY IN SOFTWARE REUSE (ICSR 2017), 2017, 10221 : 139 - 154
  • [3] Modular verification of reconfigurable components
    Tesanovic, A
    Nadjm-Tehrani, S
    Hansson, J
    [J]. COMPONENT-BASED SOFTWARE DEVELOPMENT FOR EMBEDDED SYSTEMS: AN OVERVIEW OF CURRENT RESEARCH TRENDS, 2005, 3778 : 59 - 81
  • [4] Development a modular factory with modular software components
    Jumyung, U. M.
    Fischer, Klaus
    Spieldenner, Torsten
    Kolberg, Dennis
    [J]. 27TH INTERNATIONAL CONFERENCE ON FLEXIBLE AUTOMATION AND INTELLIGENT MANUFACTURING, FAIM2017, 2017, 11 : 922 - 930
  • [5] Towards Static Modular Software Verification
    Department of Software Engineering, Technische Universität Berlin, Ernst-Reuter-Platz 7, Berlin
    10587, Germany
    [J]. Lect. Notes Informatics (LNI), Proc. - Series Ges. Inform. (GI), (147-153):
  • [6] Modular Verification of Interrupt-Driven Software
    Sung, Chungha
    Kusano, Markus
    Wang, Chao
    [J]. PROCEEDINGS OF THE 2017 32ND IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE'17), 2017, : 206 - 216
  • [7] The influence of software module systems on modular verification
    Li, HC
    Fisler, K
    Krishnamurthi, S
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 60 - 78
  • [8] On Conditions for Modular Verification in Systems of Synchronising Components
    Drabik, Peter
    Maggiolo-Schettini, Andrea
    Milazzo, Paolo
    [J]. FUNDAMENTA INFORMATICAE, 2012, 120 (3-4) : 259 - 274
  • [9] Compatibility of software components - Modeling and verification
    Craig, D. C.
    Zuberek, W. M.
    [J]. DEPCOS-RELCOMEX 2006, 2006, : 11 - +
  • [10] Software Components of the Thorvald II Modular Robot
    Grimstad, Lars
    From, Pal Johan
    [J]. MODELING IDENTIFICATION AND CONTROL, 2018, 39 (03) : 157 - 165