Informacionnye TehnologiiInformacionnye TehnologiiИнформационные технологии1684-6400New Technologies Publishing House70218110.17587/it.31.59-64Information and telecommunications technologyИнформационно-телекоммуникационные технологииResearch ArticleAspects of formalization of the subscription protocolАспекты формализации абонентского протоколаSobolV. M.СобольВ. М.
Russian Federation

Software Consultant

консультант-программист

sobolvm@yandex.ruJSC "NIIAA"Научно-исследовательский институт автоматической аппаратуры ("НИИАА")1502202531259640402202604022026Copyright ©; 2025, Informacionnye TehnologiiCopyright ©; 2025, Информационные технологии2025Informacionnye TehnologiiИнформационные технологииhttps://journals.eco-vector.com/1684-6400/article/view/702181

The issues of process specification of the model of a specialized subscriber protocol of an automated system for the exchange of documentary information using Petri network notations and time logic are considered. The semantics of document exchange is determined by the paradigm of alternation of quasi-parallel input-output processes of a reacting system. The formalization of a number of properties of the semantics of an automated system in abstractions of temporal logic is shown.

Рассматриваются вопросы процессной спецификации модели специализированного абонентского протокола автоматизированной системы обмена документальной информацией с использованием нотаций сети Петри и временной логики. Семантика документального обмена определена парадигмой чередования квазипараллельных процессов ввода-вывода реагирующей системы. Показана формализация ряда свойств семантики автоматизированной системы в абстракциях темпоральной логики.

subscriber protocoldocument exchangesubscriber servicereactive systempropositional setKripke modeltemporal logicLTLабонентский протоколдокументальный обменабонентская службареактивная системапропозициональное множествомодель Крипкевременная логикаLTLLvov E. V. The military liaison Institute. History and modernity 1923—2008, Mytishchi, 2008. 270 p.Львов Е. В. Институт военной связи. История и современность 1923—2008 гг. // Военная мысль. 2008. № 3. С. 2—7.Zatsarinny A. A. Integrated system approach: the basis of the scientific and technical policy of the Office of the Chief of Communications of the Armed Forces of the Russian Federation, Thematic collection dedicated to the 85th anniversary of the Signal Corps., Moscow, Nauka, 2002, pp. 95—108.Зацаринный А. А. Комплексный системный подход основа научно-технической политики Управления начальника связи ВС РФ // Тематический сборник, посвященный 85-й годовщине Войск связи. М.: Наука, 2002. С. 95—108.Sobol V. M., Matyukhina E. N. Four Generations of Communication Complexes of Automated Process Control Systems of Special Purpose, Industrial Automated Control Systems and Controllers, 2013, no. 4, pp. 14—21.Соболь В. М. Матюхина Е. Н. Четыре поколения коммуникационных комплексов АСУТП специального назначения // Промышленные АСУ и контроллеры. 2013. № 4. С. 14—21.Kamkin A. S. Introduction to Formal Methods of Program Verification. Studies. Textbook of Lomonosov Moscow State University, Moscow, MAX Press, 2018, 272 p.Камкин А. С. Введение в формальные методы верификации программ. М.: МАКС Пресс, 2018. 272 с.Karpov Yu. G. Model checking. Verification of parallel and distributed software systems, SPb., BHV-Peterburg, 2010, 560 p.Карпов Ю. Г. MODEL CHECKING. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.Eremeev A. P., Kurilenko I. E. The branching-time temporal logiс and its application to intelligent decision support systems, Artificial Intelligence and Decision Making, 2011, iss. 1, pp. 14—26.Еремеев А. П., Куриленко И. Е. Темпоральные модели на основе логики ветвящегося времени в интеллектуальных системах // Decision Making. 2011. C. 14—26.Tumurov E. G. Technology specification of communication protocols. Preprint 146, Novosibirsk, Rossiyskaya akademiya nauk. Sibirskoe otdelenie. Institut sistem informatiki imeni A. P. Yershova, 2007.Тумуров Э. Г. Технология спецификации коммуникационных протоколов. Препринт 146. Новосибирск: Институт систем информатики имени А. П. Ершова. 2007.Sobol V. M. On the Infology of Documentary Exchange, Information Technologies and Computing Systems, 2023, no. 2, pp. 3—17.Соболь В. М. Об инфологии документального обмена // Информационные технологии и вычислительные системы. 2023. № 2. С. 3—17.Sobol V. M. Abstractions of the elements of the ASDO subscriber service, Trudy ХXII Rossiyskoy NTK "Novye informatsionnye tekhnologii v sistemakh svyazi i upravleniya, Kaluga, 2023, pp. 37—41.Соболь В. М. Абстракции элементов абонентской службы АСДО // Труды ХXII Российской НТК "Новые информационные технологии в системах связи и управления". 2023. С. 37—41.Korablin Yu. P., Shipov A. A. System models construction based on LTL formula equational characteristics, Programmnye produkty i sistemy, 2017, vol. 30, no. 1, pp. 61—66 (in Russian), DOI: 10.15827/0236-235X.030.1.061-066.Кораблин Ю. П., Шипов А. А. Построение моделей систем на базе эквациональной характеристики формул LTL // Программные продукты и системы. 2017. Т. 30, № 1. С. 61—66.