engleski

Modeling and Verification of Concurrent Programs

The paper addresses two approaches to concurrent software verification: SPIN verification models and Generalized Stochastic Petri Nets (GSPNs). The GSPN model of a concurrent program is derived directly from PROMELA code, input language for SPIN verification system, applying straightforward statement translation rules. The translation procedure ensures that a SPIN model and the corresponding GSPN model are formally equivalent, which enables the comparison of the modeling techniques. The main contribution of the paper is the comparison of results obtained by SPIN verification procedure with both structural and performance properties of the GSPN model.

nije evidentirano

nije evidentirano