Deductive Verification of Telecommunication Systems Written in C
https://doi.org/10.18255/1818-1015-2012-6-34-44
Abstract
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.
About the Author
I. S. Anureev
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
старший научный сотрудник
Russian Federation
старший научный сотрудник
References
1. Ануреев И.С. Метод элиминации структур данных, основанный на системах переписывания формул // Программирование. 1999. №4. С. 5–15.
2. Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Т. 17, №3. С. 5–28.
3. Атучин М.М., Ануреев И.С. Атрибутные аннотации и их применение в дедуктивной верификации C-программ // Моделирование и анализ информационных систем. 2011. Т. 18, №4. С. 21–33.
4. Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Верификация C-программ в мультиязыковой системе СПЕКТР // Моделирование и анализ информационных систем. 2010. Т. 17, №4. С. 88–100.
5. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. №6. С. 1–13.
6. Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. №6. С. 5–15.
7. Таненбаум Э. Компьютерные сети. 4-е издание. 2003. 992 с.
8. Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008. №6. С. 1–20.
9. Alkassar E., Hillebrand M.A., Paul W., Petrova E. Automated Verification of a Small Hypervisor // Proc. of VSTTE 2010. Lect. Notes Comput. Sci. 2010. Vol. 6217. P. 40–54.
10. Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1–29
11. Anureev I.S. Integrated approach to analysis and verification of imperative programs // Joint NCC&IIS Bulletin, Series Computer Science. 2011. Vol. 32. P. 1–18.
12. Cohen E., Dahlweid M., Hillebrand M., at el. VCC: A Practical System for Verifying Concurrent C // Proc. of TPHOLs 2009. Lect. Notes Comput. Sci. 2009. Vol. 5674. P. 23–42.
13. Frama-C. http://frama-c.com/
14. Leinenbach D., Santen T. Verifying the Microsoft Hyper-V Hypervisor with VCC // Proc. of FM 2009. Lect. Notes Comput. Sci. 2009. Vol. 5850. P. 806–809.
15. Nepomniaschy V.A., Anureev I.S., Promsky A.V. Verification-oriented language Clight and its structural operational semantics // PSI-2003. Proc. of Conf. Lect. Notes Comput. Sci. 2003. Vol. 2890. P. 1–5.
16. Sharma B., Dhodapkar S.D., Ramesh S. Assertion Checking Environment(ACE) for Formal Verification of C Programs // Proc. of SAFECOMP 2002. Lect. Notes Comput. Sci. 2002. Vol. 2434. P. 284–295.
17. Why3: Where Programs Meet Provers. http://why3.lri.fr/
Review
For citations:
Anureev I.S. Deductive Verification of Telecommunication Systems Written in C. Modeling and Analysis of Information Systems. 2012;19(6):34-44. (In Russ.) https://doi.org/10.18255/1818-1015-2012-6-34-44
Views:
983
Email this article 