maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1103Research ArticleОригинальные статьиArticlesФормальная модель требований, используемая в процессе генерации кода приложения и кода тестовA Formal Requirements Model, Used in the Process of Application Code and Test Code GenerationБарановСергей НиколаевичBaranovS. N.SNBaranov@gmail.comКотляровВсеволод ПавловичKotlyarovV. P.vpk@spbstu.ruСанкт-Петербургский государственный политехнический университетRussian Federation201120122011184118130Copyright © Баранов С.Н., Котляров В.П., 20112011Баранов С.Н., Котляров В.П.Baranov S.N., Kotlyarov V.P.Данная работа распространяется под лицензией 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/1103

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

The considered model is used in manual development of application specifications and is based on the theory of basic protocols and respective symbolic verification tools. Means to limit the behavioral characteristics of the model still matching the source requirements are discussed. If the model is verified successfully, the executable code of the application and the respective test code are generated from the model. The technique of using the developed model is described.

модель требованийповеденческие трассыбазовые протоколыобласть определения моделиrequirements modelbehavior tracesbasic protocolsmodel scopeReferencesLetichevsky A.A., Kapitonova J.V., Volkov V.A., Vyshemirskii V.V., Letichevsky Jr. A.A. Insertion Programming // Cybernetics and Systems Analysis. 2003. Volume 39, Issue 1 (January 2003). P. 16-26.Letichevsky A.A., Kapitonova J.V., Volkov V.A., Vyshemirskii V.V., Letichevsky Jr. A.A. Insertion Programming // Cybernetics and Systems Analysis. 2003. Volume 39, Issue 1 (January 2003). P. 16-26.Letichevsky A.A., Kapitonova J.V., Kotlyarov V.P., Letichevsky O.O., Volkov V.V., Baranov S.N., Weigert T. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Proc of ISSRE04 Workshop on Integrated Reliability Engineering (ISSRE04:WITUL), IRISA, Rennes France, 2004.Letichevsky A.A., Kapitonova J.V., Kotlyarov V.P., Letichevsky O.O., Volkov V.V., Baranov S.N., Weigert T. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Proc of ISSRE04 Workshop on Integrated Reliability Engineering (ISSRE04:WITUL), IRISA, Rennes France, 2004.Летичевский О.А. Верификация и тестирование интерактивных систем, специфицированных базовыми протоколами: дис. ... канд. физ.-мат. наук. Киев, 2005. 138 с.Летичевский О.А. Верификация и тестирование интерактивных систем, специфицированных базовыми протоколами: дис. ... канд. физ.-мат. наук. Киев, 2005. 138 с.Baranov S., Kotlyarov V., Letichevsky A., Drobintsev P. The technology of Automation Verification and Testing in Industrial Projects // Proc. of St. Petersburg IEEE Chapter, International Conference, May 18-21. St.Petersburg, Russia, 2005. P. 81-86.Baranov S., Kotlyarov V., Letichevsky A., Drobintsev P. The technology of Automation Verification and Testing in Industrial Projects // Proc. of St. Petersburg IEEE Chapter, International Conference, May 18-21. St.Petersburg, Russia, 2005. P. 81-86.Letichevsky A., Gilbert D. A Model for Interaction of Agents and Environments // D.Bert, C.Choppy, P.Moses (Eds), Resent Trends in Algebraic Development Techniques. 1999. LNCS 1827. P. 311-328.Letichevsky A., Gilbert D. A Model for Interaction of Agents and Environments // D.Bert, C.Choppy, P.Moses (Eds), Resent Trends in Algebraic Development Techniques. 1999. LNCS 1827. P. 311-328.Колчин А.В. Разработка инструментальных средств для проверки формальных моделей асинхронных систем: дис. ... канд. физ.-мат. наук. Киев, 2009. 140 с.Колчин А.В. Разработка инструментальных средств для проверки формальных моделей асинхронных систем: дис. ... канд. физ.-мат. наук. Киев, 2009. 140 с.Baranov S., Kapitonova J., Letichevsky A., Kolchin A., Letichevsky A. (Jr)., Radchenko V., Potiyenko S., Volkov V. Tools For Requirements Capturing Based on the Technology of Basic Protocols // Proc. of St. Petersburg IEEE Chapter, International Conference, May 18-21. St. Petersburg, Russia, 2005. P. 92-97.Baranov S., Kapitonova J., Letichevsky A., Kolchin A., Letichevsky A. (Jr)., Radchenko V., Potiyenko S., Volkov V. Tools For Requirements Capturing Based on the Technology of Basic Protocols // Proc. of St. Petersburg IEEE Chapter, International Conference, May 18-21. St. Petersburg, Russia, 2005. P. 92-97.Баранов С.Н., Котляров В.П., Летичевский А.А. Индустриальная технология автоматизации тестирования мобильных устройств на основе верифицированных поведенческих моделей проектных спецификаций требований: Международная научная конференция: космос, астрономия и программирование. Лавровские чтения. 20-22 мая, мат.-мех. факультет СПбГУ. СПб, 2008. С.134-145.Баранов С.Н., Котляров В.П., Летичевский А.А. Индустриальная технология автоматизации тестирования мобильных устройств на основе верифицированных поведенческих моделей проектных спецификаций требований: Международная научная конференция: космос, астрономия и программирование. Лавровские чтения. 20-22 мая, мат.-мех. факультет СПбГУ. СПб, 2008. С.134-145.Recommendation ITU-T Z.151 User requirements notation (URN) - Language Definition, 2008.Recommendation ITU-T Z.151 User requirements notation (URN) - Language Definition, 2008.

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