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

作者：Wang ShengYuan^*; Dong Yuan

来源：Science China Information Sciences, 2011, 54(10): 2013-2027.

DOI：10.1007/s11432-011-4300-1

• low-level concurrent programs
• colored Petri nets
• abstract machine
• verification

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.

• 出版日期2011-10
• 单位清华大学