Geodesic
Deductive Verification of Telecommunication Systems Written~in~C
Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 6, pp. 34-44.

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

A deductive approach to verification of telecommunication systems written in C is proposed. The approach is based on the extension of C by declarative statements and on reduction of verification of parallel communicating components of these systems to separate verification of components written in this extension. An example of verification of a data link protocol is considered.
Keywords: verification, specification, operational semantics, axiomatic semantics, transformational semantics, telecommunication systems
Mots-clés : telecommunication protocols. 
@article{MAIS_2012_19_6_a2,
     author = {I. S. Anureev},
     title = {Deductive {Verification} of {Telecommunication} {Systems} {Written~in~C}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {34--44},
     publisher = {mathdoc},
     volume = {19},
     number = {6},
     year = {2012},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a2/}
}
TY  - JOUR
AU  - I. S. Anureev
TI  - Deductive Verification of Telecommunication Systems Written~in~C
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2012
SP  - 34
EP  - 44
VL  - 19
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a2/
LA  - ru
ID  - MAIS_2012_19_6_a2
ER  - 
%0 Journal Article
%A I. S. Anureev
%T Deductive Verification of Telecommunication Systems Written~in~C
%J Modelirovanie i analiz informacionnyh sistem
%D 2012
%P 34-44
%V 19
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a2/
%G ru
%F MAIS_2012_19_6_a2
I. S. Anureev. Deductive Verification of Telecommunication Systems Written~in~C. Modelirovanie i analiz informacionnyh sistem, Tome 19 (2012) no. 6, pp. 34-44. http://geodesic.mathdoc.fr/item/MAIS_2012_19_6_a2/

[1] I. S. Anureev, “Metod eliminatsii struktur dannykh, osnovannyi na sistemakh perepisyvaniya formul”, Programmirovanie, 1999, no. 4, 5–15 | Zbl

[2] I. S. Anureev, I. V. Maryasov, V. A. Nepomnyaschii, “Verifikatsiya C-programm na osnove smeshannoi aksiomaticheskoi semantiki”, Modelirovanie i analiz informatsionnykh sistem, 17:3 (2010), 5–28

[3] M. M. Atuchin, I. S. Anureev, “Atributnye annotatsii i ikh primenenie v deduktivnoi verifikatsii C-programm”, Modelirovanie i analiz informatsionnykh sistem, 18:4 (2011), 21–33

[4] V. A. Nepomnyaschii, I. S. Anureev, M. M. Atuchin, I. V. Maryasov, A. A. Petrov, A. V. Promskii, “Verifikatsiya C-programm v multiyazykovoi sisteme SPEKTR”, Modelirovanie i analiz informatsionnykh sistem, 17:4 (2010), 88–100

[5] V. A. Nepomnyaschii, I. S. Anureev, I. N. Mikhailov, A. V. Promskii, “Na puti k verifikatsii S programm. Yazyk C-light i ego formalnaya semantika”, Programmirovanie, 2002, no. 6, 1–13

[6] V. A. Nepomnyaschii, I. S. Anureev, A. V. Promskii, “Na puti k verifikatsii S programm. Aksiomaticheskaya semantika yazyka C-kernel”, Programmirovanie, 2003, no. 6, 5–15

[7] E. Tanenbaum, Kompyuternye seti, 4-e izdanie, 2003, 992 pp. | Zbl

[8] N. V. Shilov, I. S. Anureev, E. V. Bodin, “O generatsii uslovii korrektnosti dlya imperativnykh programm”, Programmirovanie, 2008, no. 6, 1–20 | MR

[9] E. Alkassar, M. A. Hillebrand, W. Paul, E. Petrova, “Automated Verification of a Small Hypervisor”, Proc. of VSTTE 2010, Lect. Notes Comput. Sci., 6217, 2010, 40–54

[10] I. S. Anureev, “A three-stage method of C program verification”, Joint NCC Bulletin. Ser. Computer Science, 28 (2008), 1–29 | Zbl

[11] I. S. Anureev, “Integrated approach to analysis and verification of imperative programs”, Joint NCC Bulletin. Ser. Computer Science, 32 (2011), 1–18

[12] E. Cohen, M. Dahlweid, M. Hillebrand at el., “VCC: A Practical System for Verifying Concurrent C”, Proc. of TPHOLs 2009, Lect. Notes Comput. Sci., 5674, 2009, 23–42 | MR

[13] Frama-C http://frama-c.com/

[14] D. Leinenbach, T. Santen, “Verifying the Microsoft Hyper-V Hypervisor with VCC”, Proc. of FM 2009, Lect. Notes Comput. Sci., 5850, 2009, 806–809

[15] V. A. Nepomniaschy, I. S. Anureev, A. V. Promsky, “Verification-oriented language C-light and its structural operational semantics”, PSI-2003. Proc. of Conf., Lect. Notes Comput. Sci., 2890, 2003, 1–5

[16] B. Sharma, S. D. Dhodapkar, S. Ramesh, “Assertion Checking Environment (ACE) for Formal Verification of C Programs”, Proc. of SAFECOMP 2002, Lect. Notes Comput. Sci., 2434, 2002, 284–295

[17] Why3: Where Programs Meet Provers http://why3.lri.fr/