Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений
Ключевые слова:
базовые протоколы, верификация, ключевые агенты, операционная семантика, логика безопасности, телекоммуникационные системы, помеченные системы переходов, язык спецификаций SDL, язык спецификаций Dynamic-REAL, система верификации SPIN, системы конечных автоматов, раскрашенные сети ПетриАннотация
В работе описываются разработанные авторами инструментальные средства и комплексный подход на их основе, при котором методы и средства анализа и верификации обеспечены для представителей всех четырех основных классов языков, на которых обычно описываются телекоммуникационные приложения: языки выполняемых спецификаций общего назначения (SDL), языки для описания и анализа укрупненных образцов поведения и выявления зависимостей между ними в сложных системах (UCM), специализированные языки, ориентированные на верификацию спецификаций телекоммуникационных систем (язык интерпретированных MSC диаграмм, язык взаимодействующих конечных автоматов, язык Dynamic-REAL) и индустриальные императивные языки (C/С++). Верификация спецификаций дополняется автоматизированным построением тестовых наборов, обеспечивающих заданную степень покрытия исходных поведенческих требований, причем эти тестовые наборы оптимизированы по заданным критериям производительности. Исполнение тестов происходит в среде автоматизированного тестирования на моделях систем, либо непосредственно на их реализациях, погруженных в соответствующие программные оболочки, обеспечивающие взаимодействие тестируемой системы с тестовым окружением. Тестовая оболочка позволяет одновременно с прогоном тестов проводить автоматизированный анализ результатов тестирования.Литература
Ануреев И.С. Дедуктивная верификация телекоммуникационных систем, представленных на языке Си//Моделирование и анализ информационных систем. 2012. 19. 410. (в печати)
Ануреев И.С. Типовые примеры использования языка Atoment//Моделирование и анализ информационных систем. 2011. 18. 4. C. 7-20
Баранов С.Н., Котляров В.П. Формальная модель требований, используемая в процессе генерации кода приложения и кода тестов//Моделирование и анализ информационных систем. 2011. 18. 4. C. 118-130
Баранов С.Н., Котляров В.П., Летичевский А.А. Индустриальная технология автоматизации тестирования мобильных устройств на основе верифицированных поведенческих моделей проектных спецификаций требований// Труды междунар. науч. конф. «Космос, астрономия и программирование». 2008. C. 134-145
Белоглазов Д.М., Машуков М.Ю., Непомнящий В.А. Верификация телекоммуникационных систем, специфицированных взаимодействующими конечными автоматами, с помощью раскрашенных сетей Петри//Моделирование и анализ информационных систем. 2011. 18. 4. C. 144-156
Дробинцев П.Д., Колчин А.В., Котляров В.П., Летичевский А.А., Песчаненко В.С. Подход к конкретизации тестовых сценариев в рамках технологии автоматизации тестирования промышленных программных проектов//Моделирование и анализ информационных систем. 2012. 4(в печати)
Колчин А.В. Автоматический метод динамического построения абстракций состояний формальной модели//Кибернетика и системный анализ. 2010. 4. C. 70-90
Колчин А.В. Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем//Проблемы программирования. 2008. 4. C. 5-12
Колчин А.В. Оптимизация проверки выполнимости переходов при верификации формальных моделей//Проблемы программирования. 2012. 2-3. C. 201-210
Колчин А.В., Котляров В.П., Дробинцев П.Д. Метод генерации тестовых сценариев в среде инсерционного моделирования//Управляющие системы и машины. 2012. 69. (в печати)
Летичевский А.А., Годлевский А.Б., Летичевский А.А.(мл.), Потиенко С.В., Песчаненко В.С. Свойства предикатного трансформера системы VRS//Кибернетика и системный анализ. 2010. 4. C. 3-16
Летичевский А.А., Капитонова Ю.В., Волков В.А., и др. Спецификация систем с помощью базовых протоколов//Кибернетика и Системный Анализ. 2005. 4. C. 3-21
Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Верификация C-программ в мультиязыковой системе СПЕКТР//Моделирование и анализ информационных систем. 2010. 17. 4. C. 88-100
Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика//Программирование. 2002. 6. C. 1-13
Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel//Программирование. 2003. 6. C. 65-80
Непомнящий В.А., Бодин Е.В., Веретнов С.О. Моделирование и верификация распределенных систем, представленных на языке SDL, с помощью языка Dynamic-REAL. 2010. 156. 44 с.
Непомнящий В.А., Бодин Е.В., Веретнов С.О. Применение языка Dynamic-REAL для анализа и верификации распределенных систем, специфицированных на языке SDL. 2011. №161. 52 с.
Непомнящий В.А., Бодин Е.В., Веретнов С.О. Язык спецификаций распределенных систем Dynamic-REAL. 2007. № 147. 42 с.
Никифоров И.В., Васин А.А., Котляров В.П. Анализ зависимостей по данным в UCM проекте// Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада 27 марта 2012 г. 2012. C. 71-72
Никифоров И.В., Петров А.В., Юсупов Ю.В. Генерация формальной модели системы по требованиям, заданным в нотации USE CASE MAPS//Научно-технические ведомости СПбГПУ. 4(103). 2010. C. 191-195
Потиенко С.В. Организация базы знаний о переходах системы с атрибутами перечислимых типов//Управляющие системы и машины. 2012. 69. (в печати)
Потиенко С.В. Статическая проверка требований и подходы к решению проблемы достижимости//Искусственный интеллект. 2009. 1. C. 192-197
Потиенко С.В., Колчин А.В. Представление SDL-спецификаций в виде базовых протоколов//Искусственный интеллект. 2006. 4. C. 42-52
Потиенко С.В., Колчин А.В. Трансляция MSC сценариев в язык базовых протоколов//Искусственный интеллект. 2007. 3. C. 428-435
Таненбаум Э. Компьютерные сети. 4-е издание. 2003. 992. с.
Anureev I.S. Integrated approach to analysis and verification of imperative programs//Joint NCC & IIS Bulletin. Series Computer Science. 2011. 32. C. 1-18
Anureev I.S. Introduction to the Atoment language//Joint NCC & IIS Bulletin. Series Computer Science. 2010. 31. C. 1-16
Anureev I.S. Program specific transition systems//Joint NCC & IIS Bulletin. Series Computer Science. 2012. 32. 21 p. (to appear)
Baranov S., Kotlyarov V. A Formal Application Model for Code and Test Generation//Automatic Control and Computer Sciences. 2012. 46. 7. C. 371-378
Baranov S., Kotlyarov V., Weigert T. Varifiable Coverage Criteria For Automated Tesdting. SDL2011: Integrating System and Software Modeling. Lecture Notes in Computer Science. 2012. 7083. C. 79-89
Beck K. Test-Driven Development by Example. 2003
Beloglazov D., Nepomniaschy V. A Two-Level Approach for Modeling and Verification of Telecommunication Systems// PSI-2003. Proс. of Conf. Lect. Notes Comput. Sci.). 2010. 5947. C. 70-85
Ben-Ari M. Principles of Spin. 2008. C. 216
Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST//Int J Softw Tools Technol Transfer. 2007. 9P. 505-525
Buhr R.J.A. and Casselman R.S. Use Case Maps for Object-Oriented Systems. 1996
Cimatti A., Clarke E. M., Giunchiglia E., and others CBMC - Bounded Model Checking for ANSI-C (electronic) http://www.cs.cmu.edu/~modelcheck/cbmc
Godefroid P. NuSMV 2: An OpenSource Tool for Symbolic Model Checking// Proceeding of International Conf. on Computer-Aided Verification. 2002. C. 359-364
Godefroid P. Partial-order methods for the verification of concurrent systems – an approach to the state-explosion problem. Lecture notes in computer science. 1996. 1032. C. 143
Ip C., Dill D. Software model checking: the VeriSoft approach// Formal methods in system design. Springer science. 2005. 26. C. 77-101
Verifying Systems with Replicated Components in Murphi// International Conf. on Computer-Aided Verification. 1996. C. 147-158
ITU-T Recommendation Z.120: Message sequence chart (MSC). October, 1996. C. (electronic) http://eu.sabotage.org/www/ITU/Z/Z0120e.pdf
ITU-T Recommendation Z.151 : User requirements notation (URN) - Language definition. September, 2003. C. (electronic) http://www.itu.int/rec/T-REC-Z.151-200811-I/en
Kaner C., Falk J., Nguyen H. Q. Testing Computer Software (2nd ed.). 1999
Letichevsky A. et al. Basic protocols, message sequence charts, and the verification of requirements specifications//Computer Networks: The International Journal of Computer and Telecommunications Networking. 49. 5. 2005. C. 661- 675
Nepomniaschy V.A., Anureev I.S., Promsky A.V. Verification-oriented language C-light and its structural operational semantics// PSI-2003. Proc. of Conf. Lect. Notes Comput. Sci. 2003. 2890. C. 1-5
Nepomniaschy V.A., Shilov N.V., Bodin E.V., Kozura V.E. Basic-REAL: integrated approach for design, specification and verification of distributed systems// Proc. of IFM 2002. Lect. Notes Comput. Sci. 2002. 2335. C. 69-88
Peled D. Combining partial order reductions with on-the-fly model checking//Journal of Formal Methods in System Design. 1996. 8. 1. C. 39-64
VCEGAR - Verilog Counterexample Guided Abstraction and Refinement. C. (electronic) http://www.cs.cmu.edu/~modelcheck/vcegar
Veselov A.O., Kotlyarov V. P. Testing automation of projects in telecommunication domain// Proceedings of the 4th Spring/Summer Young Researchers’ Colloquium on Software Engineering. June 1-2, 2010. C. 81-86
Ануреев И.С. Типовые примеры использования языка Atoment//Моделирование и анализ информационных систем. 2011. 18. 4. C. 7-20
Баранов С.Н., Котляров В.П. Формальная модель требований, используемая в процессе генерации кода приложения и кода тестов//Моделирование и анализ информационных систем. 2011. 18. 4. C. 118-130
Баранов С.Н., Котляров В.П., Летичевский А.А. Индустриальная технология автоматизации тестирования мобильных устройств на основе верифицированных поведенческих моделей проектных спецификаций требований// Труды междунар. науч. конф. «Космос, астрономия и программирование». 2008. C. 134-145
Белоглазов Д.М., Машуков М.Ю., Непомнящий В.А. Верификация телекоммуникационных систем, специфицированных взаимодействующими конечными автоматами, с помощью раскрашенных сетей Петри//Моделирование и анализ информационных систем. 2011. 18. 4. C. 144-156
Дробинцев П.Д., Колчин А.В., Котляров В.П., Летичевский А.А., Песчаненко В.С. Подход к конкретизации тестовых сценариев в рамках технологии автоматизации тестирования промышленных программных проектов//Моделирование и анализ информационных систем. 2012. 4(в печати)
Колчин А.В. Автоматический метод динамического построения абстракций состояний формальной модели//Кибернетика и системный анализ. 2010. 4. C. 70-90
Колчин А.В. Метод направления поиска и генерации тестовых сценариев при верификации формальных моделей асинхронных систем//Проблемы программирования. 2008. 4. C. 5-12
Колчин А.В. Оптимизация проверки выполнимости переходов при верификации формальных моделей//Проблемы программирования. 2012. 2-3. C. 201-210
Колчин А.В., Котляров В.П., Дробинцев П.Д. Метод генерации тестовых сценариев в среде инсерционного моделирования//Управляющие системы и машины. 2012. 69. (в печати)
Летичевский А.А., Годлевский А.Б., Летичевский А.А.(мл.), Потиенко С.В., Песчаненко В.С. Свойства предикатного трансформера системы VRS//Кибернетика и системный анализ. 2010. 4. C. 3-16
Летичевский А.А., Капитонова Ю.В., Волков В.А., и др. Спецификация систем с помощью базовых протоколов//Кибернетика и Системный Анализ. 2005. 4. C. 3-21
Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Верификация C-программ в мультиязыковой системе СПЕКТР//Моделирование и анализ информационных систем. 2010. 17. 4. C. 88-100
Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика//Программирование. 2002. 6. C. 1-13
Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel//Программирование. 2003. 6. C. 65-80
Непомнящий В.А., Бодин Е.В., Веретнов С.О. Моделирование и верификация распределенных систем, представленных на языке SDL, с помощью языка Dynamic-REAL. 2010. 156. 44 с.
Непомнящий В.А., Бодин Е.В., Веретнов С.О. Применение языка Dynamic-REAL для анализа и верификации распределенных систем, специфицированных на языке SDL. 2011. №161. 52 с.
Непомнящий В.А., Бодин Е.В., Веретнов С.О. Язык спецификаций распределенных систем Dynamic-REAL. 2007. № 147. 42 с.
Никифоров И.В., Васин А.А., Котляров В.П. Анализ зависимостей по данным в UCM проекте// Технологии Microsoft в теории и практике программирования. Материалы межвузовского конкурса-конференции студентов, аспирантов и молодых ученых Северо-Запада 27 марта 2012 г. 2012. C. 71-72
Никифоров И.В., Петров А.В., Юсупов Ю.В. Генерация формальной модели системы по требованиям, заданным в нотации USE CASE MAPS//Научно-технические ведомости СПбГПУ. 4(103). 2010. C. 191-195
Потиенко С.В. Организация базы знаний о переходах системы с атрибутами перечислимых типов//Управляющие системы и машины. 2012. 69. (в печати)
Потиенко С.В. Статическая проверка требований и подходы к решению проблемы достижимости//Искусственный интеллект. 2009. 1. C. 192-197
Потиенко С.В., Колчин А.В. Представление SDL-спецификаций в виде базовых протоколов//Искусственный интеллект. 2006. 4. C. 42-52
Потиенко С.В., Колчин А.В. Трансляция MSC сценариев в язык базовых протоколов//Искусственный интеллект. 2007. 3. C. 428-435
Таненбаум Э. Компьютерные сети. 4-е издание. 2003. 992. с.
Anureev I.S. Integrated approach to analysis and verification of imperative programs//Joint NCC & IIS Bulletin. Series Computer Science. 2011. 32. C. 1-18
Anureev I.S. Introduction to the Atoment language//Joint NCC & IIS Bulletin. Series Computer Science. 2010. 31. C. 1-16
Anureev I.S. Program specific transition systems//Joint NCC & IIS Bulletin. Series Computer Science. 2012. 32. 21 p. (to appear)
Baranov S., Kotlyarov V. A Formal Application Model for Code and Test Generation//Automatic Control and Computer Sciences. 2012. 46. 7. C. 371-378
Baranov S., Kotlyarov V., Weigert T. Varifiable Coverage Criteria For Automated Tesdting. SDL2011: Integrating System and Software Modeling. Lecture Notes in Computer Science. 2012. 7083. C. 79-89
Beck K. Test-Driven Development by Example. 2003
Beloglazov D., Nepomniaschy V. A Two-Level Approach for Modeling and Verification of Telecommunication Systems// PSI-2003. Proс. of Conf. Lect. Notes Comput. Sci.). 2010. 5947. C. 70-85
Ben-Ari M. Principles of Spin. 2008. C. 216
Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST//Int J Softw Tools Technol Transfer. 2007. 9P. 505-525
Buhr R.J.A. and Casselman R.S. Use Case Maps for Object-Oriented Systems. 1996
Cimatti A., Clarke E. M., Giunchiglia E., and others CBMC - Bounded Model Checking for ANSI-C (electronic) http://www.cs.cmu.edu/~modelcheck/cbmc
Godefroid P. NuSMV 2: An OpenSource Tool for Symbolic Model Checking// Proceeding of International Conf. on Computer-Aided Verification. 2002. C. 359-364
Godefroid P. Partial-order methods for the verification of concurrent systems – an approach to the state-explosion problem. Lecture notes in computer science. 1996. 1032. C. 143
Ip C., Dill D. Software model checking: the VeriSoft approach// Formal methods in system design. Springer science. 2005. 26. C. 77-101
Verifying Systems with Replicated Components in Murphi// International Conf. on Computer-Aided Verification. 1996. C. 147-158
ITU-T Recommendation Z.120: Message sequence chart (MSC). October, 1996. C. (electronic) http://eu.sabotage.org/www/ITU/Z/Z0120e.pdf
ITU-T Recommendation Z.151 : User requirements notation (URN) - Language definition. September, 2003. C. (electronic) http://www.itu.int/rec/T-REC-Z.151-200811-I/en
Kaner C., Falk J., Nguyen H. Q. Testing Computer Software (2nd ed.). 1999
Letichevsky A. et al. Basic protocols, message sequence charts, and the verification of requirements specifications//Computer Networks: The International Journal of Computer and Telecommunications Networking. 49. 5. 2005. C. 661- 675
Nepomniaschy V.A., Anureev I.S., Promsky A.V. Verification-oriented language C-light and its structural operational semantics// PSI-2003. Proc. of Conf. Lect. Notes Comput. Sci. 2003. 2890. C. 1-5
Nepomniaschy V.A., Shilov N.V., Bodin E.V., Kozura V.E. Basic-REAL: integrated approach for design, specification and verification of distributed systems// Proc. of IFM 2002. Lect. Notes Comput. Sci. 2002. 2335. C. 69-88
Peled D. Combining partial order reductions with on-the-fly model checking//Journal of Formal Methods in System Design. 1996. 8. 1. C. 39-64
VCEGAR - Verilog Counterexample Guided Abstraction and Refinement. C. (electronic) http://www.cs.cmu.edu/~modelcheck/vcegar
Veselov A.O., Kotlyarov V. P. Testing automation of projects in telecommunication domain// Proceedings of the 4th Spring/Summer Young Researchers’ Colloquium on Software Engineering. June 1-2, 2010. C. 81-86
Опубликован
2013-06-01
Как цитировать
Ануреев, И. С., Баранов, С. Н., Белоглазов, Д. М., Дробинцев, П. Д., Колчин, А. В., Котляров, В. П., Летичевский, А. А., Летичевский, А. А., Непомнящий, В. А., Никифоров, И. В., Потиенко, С. В., Прийма, Л. В., Тютин, Б. В., & Бодин, Е. М. (2013). Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений. Труды СПИИРАН, 3(26), 349-383. https://doi.org/10.15622/sp.26.22
Раздел
Статьи
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
