Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Алгоритм ветвей и границ для задачи коммивояжера не является алгоритмом прямого типа
Get PDFIn this paper, we consider the notion of a direct type algorithm introduced by V. A. Bondarenko in 1983. A direct type algorithm is a linear decision tree with some special properties. the concept of a direct type algorithm is determined using the graph of solutions of a combinatorial optimization problem. e vertices of this graph are all feasible solutions of a problem. Two solutions are called adjacent if there are input data for which these and only these solutions are optimal. A key feature of direct type algorithms is that their complexity is bounded from below by the clique number of the solutions graph. In 2015-2018, there were five papers published, the main results of which are estimates of the clique numbers of polyhedron graphs associated with various combinatorial optimization problems. the main motivation in these works is the thesis that the class of direct type algorithms is wide and includes many classical combinatorial algorithms, including the branch and bound algorithm for the traveling salesman problem, proposed by J. D. C. Little, K. G. Murty, D. W. Sweeney, C. Karel in 1963. We show that this algorithm is not a direct type algorithm. Earlier, in 2014, the author of this paper showed that the Hungarian algorithm for the assignment problem is not a direct type algorithm. us, the class of direct type algorithms is not so wide as previously assumed.В настоящей работе рассматривается понятие линейного разделяющего алгоритма прямого типа, введенное В. А. Бондаренко в 1983 г. Понятие алгоритма прямого типа определяется с помощью графа решений задачи комбинаторной оптимизации. Вершинами этого графа служат все допустимые решения задачи. Два решения называются смежными, если существуют входные данные, для которых эти решения и только они являются оптимальными. Ключевой особенностью алгоритмов прямого типа является то, что их трудоемкость оценивается снизу кликовым числом графа решений. В 2015–2018 гг. было опубликовано пять работ, основными результатами которых являются оценки кликовых чисел графов многогранников, ассоциированных с различными задачами комбинаторной оптимизации. В качестве основной мотивации в этих работах приводится тезис о том, что класс алгоритмов прямого типа является широким и включает в себя многие классические комбинаторные алгоритмы, в том числе алгоритм ветвей и границ для задачи коммивояжера, предложенный J. D. C. Little, K. G. Murty, D. W. Sweeney, C. Karel в 1963 г. Мы покажем, что этот алгоритм не является алгоритмом прямого типа. Ранее, в 2014 г., автором настоящей работы было показано, что венгерский алгоритм для задачи о назначениях не является алгоритмом прямого типа. Таким образом, класс алгоритмов прямого типа не является настолько широким, как предполагалось ранее
Эффективные алгоритмы проверки эквивалентности для некоторых классов автоматов
Get PDFFinite transducers, two-tape automata, and biautomata are related computational models descended from the concept of Finite-State Automaton. In these models an automaton controls two heads that read or write symbols on the tapes in the one-way mode. The computations of these three types of automata show many common features, and it is surprising that the methods for analyzing the behavior of automata developed for one of these models do not find suitable utilization in other models. The goal of this paper is to develop a uniform technique for building polynomial-time equivalence checking algorithms for some classes of automata (finite transducers, two-tape automata, biautomata, single-state pushdown automata) which exhibit certain features of the deterministic or unambiguous behavior. This new technique reduces the equivalence checking of automata to solvability checking of certain systems of equations over the semirings of languages or transductions. It turns out that such a checking can be performed by the variable elimination technique which relies on some combinatorial and algebraic properties of prefix-free regular languages. The main results obtained in this paper are as follows:1. Using the algebraic approach a new algorithm for checking the equivalence of states of deterministic finite automata is constructed; time complexity of this algorithm is O(n log n).2. A new class of prefix-free finite transducers is distinguished and it is shown that the developed algebraic approach provides the equivalence checking of transducers from this class in quadratic time (for real-time prefix-free transducers) and cubic (for prefix-free transducers with ɛ-transitions) relative to the sizes of analysed machines.3. It is shown that the equivalence problem for deterministic two-tape finite automata can be reduced to the same problem for prefix-free finite transducers and solved in cubic time relative to the size of the analysed machines.4. In the same way it is proved that the equivalence problem for deterministic finite biautomata can be solved in cubic time relative to the sizes of analysed machines.5. By means of the developed approach an efficient equivalence checking algorithm for the class of simple grammars corresponding to deterministic single-state pushdown automata is constructed.Конечные преобразователи, двухленточные автоматы и биавтоматы — взаимосвязанные вычислительные модели, ведущие свое происхождение от концепции конечного автомата. В вычислениях этих машин проявляется много общих черт, и удивительно, что методы анализа, разработанные для одной из указанных моделей, не находят подходящего применения в других моделях. Целью данной статьи является разработка единой методики построения быстрых алгоритмов проверки эквивалентности для некоторых классов автоматов (конечных преобразователей, двухленточных автоматов, биавтоматов, магазинных автоматов), которые демонстрируют определенные черты детерминированного или однозначное поведение. Этот новый метод сводит проверку эквивалентности автоматов к проверке разрешимости систем уравнений над полукольцами языков или бинарных отношений. Как оказалось, такую проверку достаточно просто провести методом исключения переменных, используя некоторые комбинаторные и алгебраические свойства регулярных префиксных языков. Основные результаты, полученные в этой статье, таковы.1. При помощи алгебраического метода построен новый алгоритм проверки эквивалентности детерминированных конечных автоматов, имеющий сложность по времени O(n log n).2. Выделен новый класс префиксных конечных трансдьюсеров и показано, что проверка эквивалентности трансдьюсеров из этого класса может быть осуществлена новым методом за время, квадратичное (для префиксных трансдьюсеров реального времени) и кубическое (для префиксных трансдьюсеров с ɛ-переходами) относительно размеров анализируемых автоматов.3. Показано, что проблема эквивалентности для детерминированных двухленточных конечных автоматов сводится к задаче проверки эквивалентности префиксных конечных трансдьюсеров и может быть решена за время, кубическое относительно их размеров.4. Аналогичным образом установлена разрешимость проблемы эквивалентности для детерминированных конечных биавтоматов за время, кубическое относительно их размеров.5. При помощи нового метода построен алгоритм проверки эквивалентности для простых грамматик, соответствующих детерминированным магазинным автоматам с одним состоянием
О задаче верификации моделей программ для одного расширения логики CTL*
Get PDFSequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace.К последовательным реагирующим системам относятся программы и устройства, которые работают с двумя потоками данных и осуществляют преобразование входных потоков данных в выходные потоки. К числу таких систем обработки информации относятся контроллеры, драйверы устройств, компьютерные интерпретаторы. Результатом работы таких вычислительных систем являются бесконечные последовательности пар событий типа запрос-отклик, и поэтому в качестве математических моделей для них наиболее часто используются конечные автоматы-преобразователи. Поведение автоматов-преобразователей представлено бинарными отношениями на бесконечных последовательностях, и традиционные прикладные темпоральные логики (HML, LTL, CTL, mu-исчисление) плохо подходят для этой цели, поскольку для интерпретации их формул используются omega-языки, а не бинарные отношения на omega-словах. Чтобы предоставить темпоральным логикам возможность определять свойства преобразований, которые характеризуют поведение реагирующих систем, мы ввели новые расширения этих логик, имеющие две отличительные особенности: 1) темпоральные операторы в расширениях этих логик параметризованы, и в качестве параметров используются языки в входном алфавите автоматов-преобразователей; 2) в качестве базовых предикатов используются языки в выходном алфавите автоматов-преобразователей. Ранее нами были исследованы выразительные возможности новых расширений Reg-LTL и Reg-CTL известных темпоральных логик линейного и ветвящегося времени LTL и CTL, в которых для параметризации темпоральных операторов и задания базовых предикатов разрешалось использовать только регулярные языки. Мы обнаружили, что такая параметризация увеличивает выразительные возможности темпоральной логики, но сохраняет разрешимость задачи проверки выполнимости формул на конечных моделях. Для указанных выше логик нами были разработаны алгоритмы верификации конечных автоматов-преобразователей. На следующем этапе изучения новых расширений темпоральной логики, предназначенных для спецификации и верификации последовательных реагирующих систем, мы обратились к задаче верификации этих систем с использованием темпоральной логики Reg-CTL*, которая является расширением обобщенной логики деревьев вычислений CTL*. В этой статье описан алгоритм проверки выполнимости формул Reg-CTL* на моделях конечных автоматов-преобразователей и показано, что эта задача принадлежит классу сложности ExpSpace
InnoChain: распределенный реестр для индустриального применения с формальной верификацией на всех уровнях реализации
Get PDFThe extent of formal verification methods applied to industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs' application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is required to ensure that the software implementation of the DLS nodes complies with this protocol. The verified software implementation of the protocol must run on a fairly reliable operating system. The so-called “smart contracts”, which are an important part of the applied implementations of specific business processes based on DLSs, must be verifiable as well. In this paper, we describe an ongoing industrial project that will result in a DLS verified at least at the four technological levels described above. We then share our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes.Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации и формальной верификации. Формальная спецификация и верификация протокола консенсуса необходима, но недостаточна. Необходимо удостовериться, что программная реализация узлов СРР соответствует данному протоколу. Верифицированная программная реализация протокола должна запускаться на достаточно надежной операционной системе. Так называемые “умные контракт”, которые являются важной частью прикладных реализаций конкретных бизнес-процессов на основе СРР, также должны быть верифицируемы.В данной работе мы описываем реализующийся в настоящее время индустриальный проект, результатом которого станет СРР, верифицированная по меньшей мере на четырех описанных выше технологических уровнях. Мы также описываем наш опыт формальной спецификации и верификации протокола HotStuff - отказоустойчивого протокола для гарантированного достижения консенсуса в присутствии византийских процессов и лидера
Динамическая модель развития пиринговой файлообменной сети
Get PDFIn this work, the model of development of the P2P file exchange network organized by a torrent tracker is considered. The model is constructed on the basis of ordinary differential equations. The phase variables describing a status of a torrent tracker and the network organized by it (in first approximation is the number of the users of the tracker who are actively participate in information exchange, and the number of active torrents) are defined, the factors influencing the change of users number and the number of torrents are analyzed. On the basis of the analysis the system of differential equations, in first approximation describing evolution of the file exchange network organized by the torrent tracker — a hard dynamic model of evolution of the torrent tracker is written. Equilibrium points of hard model of evolution of the tracker are investigated, their possible quantity and type is described. All configurations of the general provision, possible in a hard model of evolution of the torrent tracker are described. The phase portrait of the hard model is represented. On the basis of the analysis of the hard model the system of differential equations describing evolution of a file exchange network with accounting of dependence of new users inflow intensity on a total quantity of potential audience of the torrent tracker, and also dependences of speed of torrents extinction on the number of users falling on one torrent — a soft dynamic model of evolution of a torrent tracker is written. Equilibrium points of a soft model of tracker evolution are investigated, their possible quantity and type is described. All configurations of the general provision, possible in a soft model of evolution of the torrent tracker are described. Phase portraits of each configuration are represented. The ratio of parameters necessary for the stability of the tracker a stable status is received. The influence of different administrative measures on a stock of the tracker stability in whole is analyzed. The need of support of torrents by administration at highly specialized torrent trackers with small potential audience is shown.В данной работе рассматривается модель развития пиринговой файлообменной сети, организуемой одним торрент-трекером. Модель построена на основе обыкновенных дифференциальных уравнений. Определены фазовые переменные, описывающие состояние торренттрекера и организуемой им сети (в первом приближении – это количество пользователей трекера, активно участвующих в информационном обмене, и количество активных раздач), проанализированы факторы, влияющие на изменение количества пользователей и количества раздач. На основе анализа разработана система дифференциальных уравнений, в первом приближении описывающая эволюцию файлообменной сети, организуемой торрент-трекером, – жёсткая динамическая модель эволюции торрент-трекера. Исследованы особые точки жёсткой модели эволюции трекера, описано их возможное количество и тип. Описаны все конфигурации общего положения, возможные в жёсткой модели эволюции торрент-трекера. Изображён фазовый портрет жёсткой модели. На основе анализа жёсткой модели получена система дифференциальных уравнений, описывающая эволюцию файлообменной сети с учётом зависимости интенсивности притока новых пользователей от общего количества потенциальной аудитории торрент-трекера, а также зависимости скорости вымирания раздач от приходящегося на одну раздачу количества пользователей – мягкая динамическая модель эволюции торрент-трекера. Исследованы особые точки мягкой модели эволюции трекера, описано их возможное количество и тип. Описаны все конфигурации общего положения, возможные в мягкой модели эволюции торрент-трекера. Изображены фазовые портреты каждой конфигурации. Получено соотношение параметров, необходимое для устойчивости стабильного состояния трекера. Проанализировано влияние различных административных мер на запас устойчивости трекера в целом. Показана необходимость поддержки раздач администрацией на узкоспециализированных торрент-трекерах с малой потенциальной аудиторией
Особенности вычислительной реализации алгоритма оценки ляпуновских показателей систем с запаздыванием
Get PDFWe consider the computational implementation of the algorithm for Lyapunov exponents spectrum numerical estimation for delay differential equations. It is known that for such systems, as well as for boundary value problems, it is not possible to prove the well-known Oseledets theorem which allows us to calculate the required parameters very efficiently. Therefore, we can only talk about the estimates of the characteristics in some sense close to the Lyapunov exponents. In this paper, we propose two methods of linearized systems solutions processing. One of them is based on a set of impulse functions, and the other is based on a set of trigonometric functions. We show the usage flexibility of these algorithms in the case of quasi-stable structures when several Lyapunov exponents are close to zero. The developed methods are tested on a logistic equation with a delay, and these tests illustrate the “proximity” of the obtained numerical characteristics and Lyapunov exponents.Рассматривается вычислительная реализация алгоритма оценки спектра показателей Ляпунова для систем дифференциальных уравнений с запаздывающими аргументами. Учитывая, что для таких систем, а также для краевых задач не удается доказать известную теорему Оселедеца, которая позволяет эффективно вычислять искомые величины, приходится говорить лишь об оценках характеристических показателей, в каком-то смысле близких к ляпуновским. В данной работе предложены две методики обработки решений линеаризованных на аттракторе систем, одна из которых основана на базисе импульсных функций, а другая — на базисе тригонометрических функций. Продемонстрирована гибкость применения указанных алгоритмов в случае квазиустойчивых структур, когда несколько показателей Ляпунова близки к нулю. Разработанные методы тестируются на логистическом уравнении с запаздыванием. Полученные результаты иллюстрируют “близость” оцениваемых характеристик и показателей Ляпунова
Об автоматическом анализе практической стойкости обфусцирующих преобразований
Get PDFA method is developed for assessing the practical persistence of obfuscating transformations of programs based on the calculation of the similarity index for the original, obfuscated and deobfuscated programs. Candidates are proposed for similarity indices, which are based on such program characteristics as the control flow graph, symbolic execution time and degree of coverage for symbolic execution. The control flow graph is considered as the basis for building other candidates for program similarity indicators. On its basis, a new candidate is proposed for the similarity index, which, when calculated, finds the Hamming distance between the adjacency matrices of control flow graphs of compared programs. A scheme for estimating (analyzing) the persistence of obfuscating transformations is constructed, according to which for the original, obfuscated and deobfuscated programs, the characteristics of these programs are calculated and compared in accordance with the chosen comparison model. The developed scheme, in particular, is suitable for comparing programs based on similarity indices. This paper develops and implements one of the key units of the constructed scheme - a block for obtaining program characteristics compiled for the x86/x86 64 architecture. The developed unit allow to find the control flow graph, the time for symbolic execution and the degree of coverage for symbolic execution. Some results of work of the constructed block are given.Разрабатывается способ оценки практической стойкости обфусцирующих преобразований программ, основанный на вычислении показателя похожести для исходной, обфусцированной и деобфусцированной программ. Предлагаются кандидаты для показателей похожести, в основе вычисления которых лежат такие характеристики программ, как граф потока управления, время символьного выполнения и степень покрытия при символьном выполнении. Граф потока управления рассматривается как основа для построения других кандидатов для показателей похожести программ. На его основе предлагается новый кандидат для показателя похожести, при вычислении которого находится расстояние Хэмминга между матрицами смежности графов потока управления сравниваемых программ. Строится схема оценки (анализа) стойкости обфусцирующих преобразований, в соответствии с которой для исходной, обфусцированной и деобфусцированной программ вычисляются или находятся характеристики этих программ, которые сравниваются в соответствии с выбранной моделью сравнения. Разработанная схема, в частности, подходит для сравнения программ на основе показателей похожести. В работе разрабатывается и реализуется один из ключевых блоков построенной схемы – блок получения характеристик программ, скомпилированных для архитектуры x86/x86_64. Разработанный блок позволяет находить граф потока управления, время символьного выполнения и степень покрытия при символьном выполнении. Приводятся некоторые результаты работы построенного блока.
Визуальная веб-ориентированная среда динамического управления потоками данных в кампусных программно-конфигурируемых сетях
Get PDFNowadays new innovative approaches based on the technology of software defined networks (SDN) are gaining popularity in the field of computer networks (CN). SDN provide a flexible approach to the processing and control of data flows in CN by separating the control plane and data plane, as well as centralizing the representation of the entire network. In this paper, we propose a software infrastructure and a visual web-oriented environment (SIVE) for dynamic control of data flows in campus SDN based on OpenFlow protocol. It was proposed to use the SIVE as an integrated segment of the campus network of Ryazan State Radio Engineering University. The aim of the work is the development of the SIVE architecture in the form of UML class diagram description, as well as the creation of software methods for organizing effective network interaction of various software systems in SDN based on OpenFlow protocol. A hardware-software test bench based on HP Aruba 2920-24G equipment was developed to confirm the efficiency and reliability of the proposed SIVE. The offered SIVE is the basis for the development of a large class of software systems and SDN components based on OpenFlow protocol.В настоящее время в области компьютерных сетей (КС) широкую популярность получают инновационные подходы, основанные на технологии программно-конфигурируемых сетей (ПКС). ПКС позволяют обеспечить гибкий подход в обработке и управлении потоков данных в КС за счет разделения плоскости управления и передачи данных, а также централизации представления всей сети. В данной работе предложен прототип программной инфраструктуры и визуальной веб-ориентированной среды (ПИВС) динамического управления потоками данных в ПКС на основе протокола OpenFlow. Предложено использовать ПИВС в качестве интегрированного сегмента кампусной сети Рязанского государственного радиотехнического университета. Целью работы является разработка архитектуры ПИВС в виде описания UML диаграмм классов, а также создание программных методов для организации эффективного сетевого взаимодействия различных программных систем в ПКС на основе протокола OpenFlow. Для подтверждения эффективности и надежности предложенной ПИВС разработан программно-аппаратный стенд на базе оборудования HP Aruba 2920-24G. Предлагаемая в работе ПИВС является основой для разработки большого класса программных систем и компонентов ПКС на основе протокола OpenFlow
Иерархические периферийные вычисления
Get PDFThe computing paradigm based on the giant-like DC is replaced by a new paradigm. The urgency of this shift is caused by the requirements of new applications that actively use video, real-time interactivity, new mobile communication technologies, which today cannot be implemented without the usage of cloud computing and virtualization based on SDN&NFV technologies. The presentation considers the requirements dictated by these applications, outlines the architecture of this new paradigm which we call Hierarchical Edge Computing (HEC). Attention is focused on the fact that all these applications are distributed, become more and more real-time applications and require guaranteed quality of service in the networking operation. The main scientific problems that need to be solved for implementing this new paradigm are discussed.На смену вычислительной парадигме, основанной на giant-like ЦОДах, идет новая, основанная на сети мелких ЦОДов, образующих инфраструктуру для облачных вычислений. Эта смена объективна. Её актуальность обусловлена требованиями новых приложений, активно использующих видео, интерактивность в реальном времени, новые технологии мобильной связи, которые сегодня невозможно реализовать без облачных вычислений и виртуализации на основе технологий SDN&NFV. В статье рассмотрены требования, предъявляемые этими приложениями, предложена архитектура новой парадигмы, которую мы называем «Иерархическими периферийными вычислениями» (Hierarchical Edge Computing – HEC). Показано, что большинство современных приложений являются распределенными совокупностями сервисов реального времени, которые требуют гарантированного качества обслуживания и возможности динамически быть размещенными при работе на периферии сетей разных операторов. Обсуждаются основные научные проблемы, которые необходимо решить для реализации предлагаемой новой парадигмы
Построение бортовых сетей реального времени на основе технологии ПКС
Get PDFModern onboard equipment complexes (OEC) utilize AFDX and FC-AE-ASM-RT switched networks implementing a virtual link-based approach to real-time data transfer. The main drawback of these networks is their limited or absent support for dynamic reconfiguration of virtual links, which makes impossible the dynamical recomposition of OEC operation modes, particularly in case of multiple equipment failures. To remove these drawbacks, in this paper an approach is proposed to use software-defined networks (SDN) as onboard real-time networks. The proposed approach is based on implementation of a virtual link-based technology (similar to those used in AFDX and FC-AE-ASMRT) in an SDN supporting OpenFlow 1.3 protocol. The approach was implemented as a functional prototype and experimentally evaluated in a virtual network environment based on Ofsoftswitch13 software SDN switches and RUNOS controller. The experiments indicated that the proposed data exchange scheme allows the transfer of messages within the given limits on delay and jitter, and does not allow violation of constraints on a virtual link bandwidth. The experiments also confirmed that dynamic reconfiguration of virtual links in SDN does not interrupt the data transfer through unchanged virtual links. An important direction for future work is development of algorithms for dynamic creation of virtual link routes in course of OEC reconfiguration. The final goal of the work is to create an SDN-based network technology supporting both real-time data transfer and automatic network reconfiguration in case of OEC mode change, including parrying multiple failures.В интегрированных модульных комплексах бортового оборудования (КБО) используются коммутируемые сети AFDX и FC-AE-ASM-RT, реализующие основанный на виртуальных каналах подход к передаче данных в реальном времени. Основным недостатком этих сетей являются ограниченные или отсутствующие возможности динамической реконфигурации виртуальных каналов, что приводит к невозможности динамического формирования режимов функционирования КБО, в частности при множественных отказах оборудования. Для снятия выявленных ограничений в данной работе предложен подход к использованию программно-конфигурируемых сетей (ПКС) для построения бортовых сетей реального времени. Предложенный подход основан на реализации в сети ПКС, поддерживающей протокол OpenFlow1.3, механизма виртуальных каналов, аналогичного используемому в сетях AFDX и FC-AE-ASM-RT. Подход реализован в виде функционального прототипа и экспериментально апробирован в виртуальной сетевой среде, основанной на программных ПКС-коммутаторах Ofsoftswitch13 и сетевом контроллере RUNOS. Эксперименты показали, что предложенная схема передачи данных позволяет передавать сообщения с соблюдением заданных ограничений на задержку и джиттер, а также не допускает превышения ограничения на пропускную способность виртуального канала. Эксперименты также подтвердили, что динамическая реконфигурация виртуальных каналов в ПКС не нарушает передачу данных по не изменяемым виртуальным каналам. Важным направлением дальнейших исследований является разработка алгоритмов динамического формирования новых маршрутов виртуальных каналов в процессе реконфигурации КБО. Конечной целью работ является создание на основе ПКС сетевой технологии, обеспечивающей как передачу данных в реальном времени, так и автоматическое переконфигурирование сети при смене режимов функционирования КБО, в том числе при парировании множественных отказов