maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2012-6-34-44mais-137Research ArticleОригинальные статьиArticlesДедуктивная верификация телекоммуникационных систем, представленных на языке СиDeductive Verification of Telecommunication Systems Written in CАнуреевИгорь СергеевичAnureevI. S.

старший научный сотрудник

старший научный сотрудник

anureev@iis.nsk.suИнститут систем информатики имени А.П. Ершова СО РАНРоссияИнститут систем информатики имени А.П. Ершова СО РАНRussian Federation2012120320151963444Copyright © Ануреев И.С., 20152015Ануреев И.С.Anureev I.S.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/137

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

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.

верификацияспецификацияоперационная семантикааксиоматическая семантикатрансформационная семантикателекоммуникационные системытелекоммуникационные протоколыverificationspecificationoperational semanticsaxiomatic semanticstransformational semanticstelecommunication systemstelecommunication protocolsРФФИReferencesАнуреев И.С. Метод элиминации структур данных, основанный на системах переписывания формул // Программирование. 1999. №4. С. 5–15.Ануреев И.С. Метод элиминации структур данных, основанный на системах переписывания формул // Программирование. 1999. №4. С. 5–15.Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Т. 17, №3. С. 5–28.Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Т. 17, №3. С. 5–28.Атучин М.М., Ануреев И.С. Атрибутные аннотации и их применение в дедуктивной верификации C-программ // Моделирование и анализ информационных систем. 2011. Т. 18, №4. С. 21–33.Атучин М.М., Ануреев И.С. Атрибутные аннотации и их применение в дедуктивной верификации C-программ // Моделирование и анализ информационных систем. 2011. Т. 18, №4. С. 21–33.Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Верификация C-программ в мультиязыковой системе СПЕКТР // Моделирование и анализ информационных систем. 2010. Т. 17, №4. С. 88–100.Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Верификация C-программ в мультиязыковой системе СПЕКТР // Моделирование и анализ информационных систем. 2010. Т. 17, №4. С. 88–100.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. №6. С. 1–13.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. №6. С. 1–13.Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. №6. С. 5–15.Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. №6. С. 5–15.Таненбаум Э. Компьютерные сети. 4-е издание. 2003. 992 с.Таненбаум Э. Компьютерные сети. 4-е издание. 2003. 992 с.Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008. №6. С. 1–20.Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008. №6. С. 1–20.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.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.Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1–29Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1–29Anureev I.S. Integrated approach to analysis and verification of imperative programs // Joint NCC&IIS Bulletin, Series Computer Science. 2011. Vol. 32. P. 1–18.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.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.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.Frama-C. http://frama-c.com/Frama-C. http://frama-c.com/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.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.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.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.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.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.Why3: Where Programs Meet Provers. http://why3.lri.fr/Why3: Where Programs Meet Provers. http://why3.lri.fr/

The authors declare that there are no conflicts of interest present.