Verification of Concurrent Assembly Programs with a Petri Net Based Safety Policy

被引：1

作者：

Wang, Shengyuan ^{[1
]}

Liang, Yingyi ^{[1
]}

Dong, Yuan ^{[1
]}

机构：

[1] Department of Computer Science and Technology, Tsinghua University, Beijing

来源：

Tsinghua Science and Technology | 2007年 / 12卷 / 06期

基金：

中国国家自然科学基金;

关键词：

machine level concurrent programming; Petri nets; safety policy; verification; verifying/certifying compilers;

D O I：

10.1016/S1007-0214(07)70176-1

中图分类号：

学科分类号：

摘要：

Concurrent programs written in a machine level language are being used in many areas but verification of such programs brings new challenges to the programming language community. Most of the studies in the literature on verifying the safety properties of concurrent programs are for high-level languages, specifications, or calculi. Therefore, more studies are needed on concurrency verification for machine level language programs. This paper describes a framework of a Petri net based safety policy for the verification of concurrent assembly programs, to exploit the capability of Petri nets in concurrency modeling. The concurrency safety properties can be considered separately using the net structure and by mixing Hoare logic and computational tree logic. Therefore, more useful higher-level safety properties can be specified and verified. © 2007 Tsinghua University Press.

引用

页码：684 / 690

页数：6

共 11 条

[1]

Necula G., Compiling with proofs [Ph. D. Dissertation], (1998)

[2]

Morrisett G., Crary K., Glew N., Walker D., Stack-based typed assembly language, Proc. Workshop on Types in Compilation, Kyoto, Japan, LNCS Vol. 1473, pp. 28-52, (1998)

[3]

Yu D., Hamid N., Shao Z., Building certified libraries for PCC: Dynamic storage allocation, Science of Computer Programming, 50, 1-3, pp. 101-127, (2004)

[4]

Hoare C., An axiomatic basis for computer programming, Communications of the ACM, 12, 10, pp. 576-580, (1969)

[5]

Hoare C., Communicating sequential processes, Communications of the ACM, 21, 8, pp. 666-677, (1978)

[6]

Milner R., Communicating and Mobile Systems: The π-Calculus, (1999)

[7]

Resig W., Petri Nets: An Introduction, Vol. 4 of EATCS Monographs on Theoretical Computer Science, (1985)

[8]

Chandy K., Misra J., Parallel Program Design: A Foundation, (1988)

[9]

Clarke E., Emerson E., Sistla J., Automatic verification of finite state concurrent systems using temporal logic specification, ACM Transactions on Programming Languages and Systems, 8, 20, pp. 244-263, (1986)

[10]

Roch S., Starke P., INA: Integrated Net Analyzer Version 2.2 Manual. Department of Computer Science, Humboldt-University of Berlin, April 1999

← 1 2 →