Verification in concurrent programming with Petri nets structural techniques

被引：9

作者：

Barkaoui, K ^{[1
]}

Pradat-Peyre, JF ^{[1
]}

机构：

[1] Conservatoire Natl Arts & Metiers, Lab CEDRIC, Paris, France

来源：

THIRD IEEE INTERNATIONAL HIGH-ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS | 1998年

关键词：

D O I：

10.1109/HASE.1998.731604

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper deals with verification of flow control in concurrent programs. We use,Ada language model as reference. After translation of Ada programs into Petri nets (named Ada nets for Ada programs), Ice show how one can fully exploit the relationship between the behavior of the concurrent program and the structure of the corresponding Petri net. Using the siphon structure, Me precise some structural conditions for behavioral properties such as deadlock-freeness and likeness that correct concurrent programs must satisfy. These conditions carl be proved or disproved using efficient algorithms. We provide also a formal justification of guidelines (such as client/server paradigm) that programmers observe traditionally in order to built correct concurrent programs. Several examples are presented to show the effectiveness of using structure theory of Petri nets for static analysis of concurrent programs.

引用

页码：124 / 133

页数：10