Formal Modelling of Program Dependence Net for Software Model Checking

Abstract

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.