Дедуктивная верификация телекоммуникационных систем, представленных на языке Си


https://doi.org/10.18255/1818-1015-2012-6-34-44

Полный текст:


Аннотация

Предложен дедуктивный подход к верификации телекоммуникационных систем, представленных на языке C. Подход основан на расширении языка C декларативными операторами и сведении верификации параллельных взаимодействующих компонент телекоммуникационных систем к раздельной верификации компонент, представленных на расширенном языке. Рассмотрен пример верификации протокола передачи данных.


Об авторе

Игорь Сергеевич Ануреев
Институт систем информатики имени А.П. Ершова СО РАН
Россия
старший научный сотрудник


Список литературы

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/


Дополнительные файлы

Для цитирования: Ануреев И.С. Дедуктивная верификация телекоммуникационных систем, представленных на языке Си. Моделирование и анализ информационных систем. 2012;19(6):34-44. https://doi.org/10.18255/1818-1015-2012-6-34-44

For citation: 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

Просмотров: 238

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)