A verifiable low-level concurrent programming model based on colored Petri nets  

作　　者：WANG ShengYuan DONG Yuan 

机构地区：[1]Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China

出　　处：《Science China(Information Sciences)》2011年第10期2013-2027,共15页中国科学（信息科学）（英文版）

基　　金：supported by the National Natural Science Foundation of China (Grant Nos.90818019,60573017);the National High-Tech Research and Development Plan of China (Grant No.2008AA01Z102)

摘　　要：Concurrent programs written in a machine-level language are being used in many areas, but the verification of such programs brings various new challenges to the programming language community. Most of existing contributions on verifying the safety properties of concurrent programs are for high-level languages, specifications, or calculi in the literature. Due to the lack of abstraction at a low level, additional work is needed to extend these methods to machine-level language. This paper describes an approach to integrate Petri nets into low-level concurrent programs to form a new programming model （abstract machine）. A program in the programming model is a restricted version of colored Petri net, with transitions colored by assembly codes for machine-level threads, and places colored by shared data consisting of memory locations or registers. Existing analysis and verification approaches for usual Petri nets can be applied indirectly for such a low-level concurrent program.Concurrent programs written in a machine-level language are being used in many areas, but the verification of such programs brings various new challenges to the programming language community. Most of existing contributions on verifying the safety properties of concurrent programs are for high-level languages, specifications, or calculi in the literature. Due to the lack of abstraction at a low level, additional work is needed to extend these methods to machine-level language. This paper describes an approach to integrate Petri nets into low-level concurrent programs to form a new programming model （abstract machine）. A program in the programming model is a restricted version of colored Petri net, with transitions colored by assembly codes for machine-level threads, and places colored by shared data consisting of memory locations or registers. Existing analysis and verification approaches for usual Petri nets can be applied indirectly for such a low-level concurrent program.

关 键 词：low-level concurrent programs colored Petri nets abstract machine VERIFICATION 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论] TM711[自动化与计算机技术—计算机科学与技术]