FORMAL MODELLING OF PROGRAM DEPENDENCE NET FOR SOFTWARE MODEL CHECKING

被引：0
|
作者：
Li, Shuo [1 ]
Ding, Zhijun [2 ]
Pan, Meiqin [3 ]
机构：
[1] Taishan Univ, Sch Informat Sci & Technol, Tai An 271000, Peoples R China
[2] Tongji Univ, Dept Comp Sci, Shanghai 201804, Peoples R China
[3] Shanghai Int Studies Univ, Sch Business & Management, Shanghai 200083, Peoples R China
来源：
COMPUTING AND INFORMATICS | 2024年 / 43卷 / 05期
关键词：
Formal modelling; operational semantics; PThread; PDNet; LTL; VERIFICATION;
D O I：
10.31577/cai202451161
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Program dependence net (PDNet) is a kind of Petri nets which can represent concurrent systems and software to apply the automata-theoretic approach for software model checking on Linear Temporal Logic (LTL). This paper presents a formal modelling method to construct a PDNet which is consistent with the behavior of multi-threaded C programs (PThread programs) from a source code. For concurrent programs with a function call and POSIX threads, we propose the formal operational semantics by the labeled transition system (LTS). We formalize the statements by the basic PDNet structure based on LTS operational semantics. Then, we propose the formal modelling method to build a basic flow to simulate the execution of PThread programs. Finally, we give a case study to illustrate the formal modelling method for verifying PThread programs on LTL properties.
引用
收藏
页码：1161 / 1184
页数：24
相关论文
共 50 条
  • [21] Formal Model for Checking the Interoperability Between the Components of the IoT system
    Timenko, A., V
    Shkarupylo, V. V.
    Oliinyk, A. O.
    Hrushko, S. S.
    PROBLEMELE ENERGETICII REGIONALE, 2019, (1-1): : 69 - 78
  • [22] Context-bounded model checking of concurrent software
    Qadeer, S
    Rehof, J
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 93 - 107
  • [23] SOFTWARE MODEL CHECKING WITH EXPLICIT SCHEDULER AND SYMBOLIC THREADS
    Cimatti, Alessandro
    Narasamdya, Iman
    Roveri, Marco
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (02)
  • [24] Between Testing and Verification: Dynamic Software Model Checking
    Godefroid, Patrice
    DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2016, 45 : 99 - 116
  • [25] EUFORIA: Complete Software Model Checking with Uninterpreted Functions
    Bueno, Denis
    Sakallah, Karem A.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2019, 2019, 11388 : 363 - 385
  • [26] Efficient Modular Glass Box Software Model Checking
    Roberson, Michael
    Boyapati, Chandrasekhar
    ACM SIGPLAN NOTICES, 2010, 45 (10) : 4 - 21
  • [27] Efficient software model checking of data structure properties
    Darga, Paul T.
    Boyapati, Chandrasekhar
    ACM SIGPLAN NOTICES, 2006, 41 (10) : 363 - 381
  • [28] Model Checking Applied to Embedded Software of University Satellite
    Alencar, Waldo A. F.
    Villani, Emilia
    JOURNAL OF CONTROL AUTOMATION AND ELECTRICAL SYSTEMS, 2014, 25 (01) : 126 - 136
  • [29] On-the-Fly Decomposition of Specifications in Software Model Checking
    Apel, Sven
    Beyer, Dirk
    Mordan, Vitaly
    Mutilin, Vadim
    Stahlbauer, Andreas
    FSE'16: PROCEEDINGS OF THE 2016 24TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON FOUNDATIONS OF SOFTWARE ENGINEERING, 2016, : 349 - 361
  • [30] Software Model Checking Using Languages of Nested Trees
    Alur, Rajeev
    Chaudhuri, Swarat
    Madhusudan, P.
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2011, 33 (05):
12345