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 条

[1] Change-aware model checking for evolving concurrent programs based on Program Dependence Net
Li, Shuo
Chen, Cheng
Huang, Zheng
Ding, Zhijun
JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS, 2023, 36 (06)
[2] Deductively Verified Program Models for Software Model Checking
Amilon, Jesper
Gurov, Dilian
LEVERAGING APPLICATIONS OF FORMAL METHOD, VERIFICATION AND VALIDATION: SPECIFICATION AND VERIFICATION, PT III, ISOLA 2024, 2025, 15221 : 8 - 25
[3] Checking Critical Software Systems: A Formal Proposal
Mendoza Morales, Luis E.
Capel, Manuel I.
PROCEEDINGS 2016 10TH INTERNATIONAL CONFERENCE ON THE QUALITY OF INFORMATION AND COMMUNICATIONS TECHNOLOGY (QUATIC), 2016, : 160 - 163
[4] Software Model Checking
Jhala, Ranjit
Majumdar, Rupak
ACM COMPUTING SURVEYS, 2009, 41 (04)
[5] Interoperability Constraints and Requirements Formal Modelling and Checking Framework
Chapurlat, Vincent
Roque, Matthieu
ADVANCES IN PRODUCTION MANAGEMENT SYSTEMS: NEW CHALLENGES, NEW APPROACHES, 2010, 338 : 219 - 226
[6] Model Checking of Software for Microcontrollers
Schlich, Bastian
ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2010, 9 (04)
[7] Software Model Checking SystemC
Cimatti, Alessandro
Narasamdya, Iman
Roveri, Marco
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2013, 32 (05) : 774 - 787
[8] A tool for visual and formal modelling of software designs
Amalio, Nuno
Glodt, Christian
SCIENCE OF COMPUTER PROGRAMMING, 2015, 98 : 52 - 79
[9] Model Checking Software in Cyberphysical Systems
Sirjani, Marjan
Lee, Edward A.
Khamespanah, Ehsan
2020 IEEE 44TH ANNUAL COMPUTERS, SOFTWARE, AND APPLICATIONS CONFERENCE (COMPSAC 2020), 2020, : 1017 - 1026
[10] The role of model checking in software engineering
Karna, Anil Kumar
Chen, Yuting
Yu, Haibo
Zhong, Hao
Zhao, Jianjun
FRONTIERS OF COMPUTER SCIENCE, 2018, 12 (04) : 642 - 668

← 1 2 3 4 5 →