Geodesic
Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets
Modelirovanie i analiz informacionnyh sistem, Tome 16 (2009) no. 1, pp. 92-111.

Voir la notice de l'article provenant de la source Math-Net.Ru

Formal proving of program correctness is the only reliable method that ensures proper functioning of program systems. Existing verification methods are quite complicated in practice, that obstructs their extensive application. In this article an approach using “Design By Contract” conception is proposed, where class protocols formulated in terms of Petri nets makes it possible to analyze workability of classes and programs separately that facilitates the procedure of program correctness checking.
Keywords: programming languages, formal program verification, object-oriented programming, Petri nets. 
@article{MAIS_2009_16_1_a6,
     author = {D. I. Kharitonov},
     title = {Separable object-oriented program verification with {C++} class protocol definition in terms of {Petri} nets},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {92--111},
     publisher = {mathdoc},
     volume = {16},
     number = {1},
     year = {2009},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2009_16_1_a6/}
}
TY  - JOUR
AU  - D. I. Kharitonov
TI  - Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2009
SP  - 92
EP  - 111
VL  - 16
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2009_16_1_a6/
LA  - ru
ID  - MAIS_2009_16_1_a6
ER  - 
%0 Journal Article
%A D. I. Kharitonov
%T Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets
%J Modelirovanie i analiz informacionnyh sistem
%D 2009
%P 92-111
%V 16
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2009_16_1_a6/
%G ru
%F MAIS_2009_16_1_a6
D. I. Kharitonov. Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets. Modelirovanie i analiz informacionnyh sistem, Tome 16 (2009) no. 1, pp. 92-111. http://geodesic.mathdoc.fr/item/MAIS_2009_16_1_a6/

[1] N. A. Anisimov, “Formalnaya model dlya razrabotki i formalnogo opisaniya protokolov”, Avtomatika i vychislitelnaya tekhnika, 6 (1988), 3–10 | MR

[2] N. A. Anisimov, E. A. Golenkov, D. I. Kharitonov, “Kompozitsionalnyi podkhod k razrabotke parallelnykh i raspredelennykh sistem na osnove setei Petri”, Programmirovanie, 6 (2001), 30–43 | MR | Zbl

[3] O. L. Bandman, “Proverka korrektnosti setevykh protokolov s pomoschyu setei Petri”, Avtomatika i vychislitelnaya tekhnika, 6 (1986), 82–91

[4] V. A. Nepomnyaschii, O. M. Ryakin, Prikladnye metody verifikatsii programm, Radio i svyaz, M., 1988

[5] A. P. Lisitsa, A. P. Nemytykh, “Verifikatsiya kak parametrizovannoe testirovanie (eksperimenty s superkompilyatorom SCP4)”, Programmirovanie, 1 (2007), 22–34 | Zbl

[6] V. A. Nepomnyaschii, I. S. Anureev, I. N. Mikhailov, A. V. Promskii, “Na puti k verifikatsii S-programm. Yazyk C-light”, Konferentsiya, posvyaschennaya 90-letiyu so dnya rozhdeniya Alekseya Andreevicha Lyapunova, Tezisy dokladov, Novosibirsk, 2001

[7] V. A. Nepomnyaschii, I. S. Anureev, I. V. Dubranovskii, A. V. Promskii, “Na puti k verifikatsii S#-programm: Trëkhurovnevyi podkhod”, Programmirovanie, 4 (2006), 4–20

[8] V. V. Lipaev, “Metodologiya verifikatsii i testirovaniya krupnomasshtabnykh programmnykh sredstv”, Programmirovanie, 4 (2003), 7–24

[9] B. Meier, Ob'ektno-orientirovannoe konstruirovanie programmnykh sistem, Russkaya redaktsiya, M., 2005

[10] C. A. R. Hoare, “An Axiomatic Basis for Computer Programming”, Comm. ACM, 12, no. 10, The Queen's University of Belfast, Northern Ireland, 1969, 576–580 | Zbl

[11] K. A. Petri, Kommunication mit Automaten, Schriften des Rheinish, Westfalischen Institutes fur Instrumentelle Mathematik and der Universitat, Bonn, 1962

[12] P. Müller, Modular Specification and Verification of Object-Oriented Programs, Springer-Verlag, 2001

[13] M. Barnett, R. DeLine, M. Fähndrich, K. Rustan, M. Leino, W. Schulte, “Verification of Object-Oriented Programs with Invariants”, Journal of Object Technology, 3 (2004), 27–56 | DOI

[14] J. Quielle, J. Sifakis, “Specification and verification of concurrent systems in CESAR”, Proceedings 5-th International Symposium on Programming, LNCS, 137, 1982, 337–351 | MR

[15] E. M.Clarke, E. A. Emerson, “Synthesis of synchronisation skeletons for branching time logic”, Logic of Programs, LNCS, 131, 1981, 52–71 | MR