?
A formal model and verification problems for Software Defined Networks
Automatic Control and Computer Sciences. 2014. Vol. 48. No. 7. P. 398-406.
Smeliansky R. L., Chemeritsky E. V., Захаров В. А.
Переводчик: Захаров В. А.
Научное направление:
Компьютерные науки
Приоритетные направления:
компьютерно-математическое
Язык:
английский
Захаров В. А., Чемерицкий Е. В., Automatic Control and Computer Sciences 2015 Vol. 49 No. 7
Designing of network update algorithms is an important line of research in the development of software for new generation of telecommunication networks – Software Defined Networks. A specific case of Network Update Problem is that of seamless recovering of network configurations after the loss of some forwarding rules as it may happens e.g. due ...
Добавлено: 13 октября 2015 г.
Захаров В. А., Чемерицкий Е. В., Моделирование и анализ информационных систем 2014 Т. 21 № 6 С. 57-69
Разработка алгоритмов реконфигурирования сетей является важным направлением развития программного обеспечения для телекоммуникационных сетей нового поколения --- программно конфигурируемых сетей. Частный случай проблемы реконфигурирования сетей --- это задача плавного восстановления заданной сетевой конфигурации, после того как некоторые правила коммутации пакетов были удалены из таблиц коммутаторов (например, по истечении срока их активности). В данной статье проведено исследование ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Чемерицкий Е. В., , in : Proceedings of 2014 International Science and Technology Conference "Modern Networking Technologies (MoNeTec): SDN&NFV Next Generation of Computational Infrastructure", Moscow, Russia, October 27-29, 2014. : M. : Max press, 2014. P. 47-52.
Добавлено: 13 октября 2015 г.
Захаров В. А., Смелянский Р. Л., Чемерицкий Е. В., Моделирование и анализ информационных систем 2013 Т. 20 № 6 С. 33-48
Программно-коммутируемые сети (ПКС) --- это класс компьютерных телекоммуникационных сетей, появившийся несколько лет назад в стремлении упростить проектирование и повысить гибкость управления сетями за счет разделения потоков данных (пакетов) и потоков управления (сообщений и команд), циркулирующие в сетях. ПКС представляет собой распределенную систему, в которой один или несколько контроллеров управляют множеством сетевых коммутаторов, обеспечивающих продвижение пакетов ...
Добавлено: 30 сентября 2015 г.
Камкин А. С., М. : МАКС Пресс, 2018
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018
Добавлено: 26 октября 2018 г.
Захаров В. А., Коннов И. В., Моделирование и анализ информационных систем 2010 Т. 17 № 4 С. 78-87
Наиболее значительную трудность для всех инструментальных средств верификации моделей программ
создает эффект комбинаторного взрыва. Один из способов сократить размер проверяемой модели $M$ ---
выбрать подходящую группу автоморфизмов $G$ размеченной системы переходов $M$ и построить фактор-модель $M/G$.
Состояниями фактор-модели $M/G$ служат орбиты состояний модели $M$ относительно группы $G$; также известно,
что модели $M/G$ и $M$ находятся ...
Добавлено: 30 сентября 2015 г.
Zakharov V.A., Volkanov D. Y., Zorin D. A. и др., Programming and Computer Software 2015 Vol. 41 No. 6 P. 325-335
Checking the correctness of distributed systems is one of the most difficult and urgent problems in software engineering. A combined toolset for the verification of real-time distributed systems (RTDS) is described. RTDSs are specified as statecharts in the Universal Modeling Language (UML). The semantics of statecharts is defined by means of hierarchical timed automata. The ...
Добавлено: 13 октября 2015 г.
И. В. Ефименко, Форсайт 2013
В работе обсуждаются вопросы создания формальной модели предметной области дорожного картирования на основе анализа лучших практик в данной области. Предполагается, что создание такой модели позволит обобщить опыт построения дорожных карт и обеспечит основу для разработки средств автоматизации формирования и использования дорожных карт. ...
Добавлено: 12 августа 2013 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2-8
В работе рассматривается генератор тестовых программ, предназначенный для верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из формальных спецификаций архитектуры RISC-V и архитектурно независимого ядра. Спецификации задают синтаксис и семантику команд. Ядро реализует техники построения последовательностей команд и генерации данных. Генерация осуществляется на основе шаблонов, описывающих структурные и поведенческие свойства программ. Инструмент позволяет расширять ...
Добавлено: 30 октября 2018 г.
Захаров В. А., Подымов В. В., Алтухов В. С. и др., , in : Proceedings of 2014 International Science and Technology Conference "Modern Networking Technologies (MoNeTec): SDN&NFV Next Generation of Computational Infrastructure", Moscow, Russia, October 27-29, 2014. : M. : Max press, 2014. P. 7-12.
Добавлено: 13 октября 2015 г.
Захаров В. А., Волканов Д. Ю., Зорин Д. А. и др., Программирование 2015 № 6 С. 72-86
Проверка правильности функционирования распределенных программ --- это одна из наиболее трудных и актуальных задач современного программирования. В статье описано комбинированное программно-инструментальное средство верификации распределенных вычислительных систем реального времени (РВС РВ). Для описания РВС РВ используется универсальный язык моделирования UML. Семантика диаграмм состояний UML определяется на основе модели вычислений иерархических временных автоматов. Средство верификации диаграмм UML ...
Добавлено: 13 октября 2015 г.
Cham : Springer, 2017
This book constitutes the refereed proceedings of the 13th International Haifa Verification Conference, HVC 2017, held in Haifa, Israel in November 2017. The 13 revised full papers presented together with 4 poster and 5 tool demo papers were carefully reviewed and selected from 45 submissions. They are dedicated to advance the state of the art and state of the ...
Добавлено: 24 января 2018 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2018 Т. 25 № 5 С. 506-524
О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 5. — С. 506–524. Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых ...
Добавлено: 26 октября 2018 г.
Татарников А. Д., Камкин А. С., Проценко А. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87-102
ARM — это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ ...
Добавлено: 24 ноября 2017 г.
Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences, Allerton Press Inc., United States 2019 Vol. 53 No. 7 P. 663-675
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a nite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between ows of control signals ...
Добавлено: 17 октября 2019 г.
Татарников А. Д., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97-100
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промышленных микропроцессоров. ...
Добавлено: 2 февраля 2018 г.
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21-32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 9 ноября 2020 г.
Switzerland : Springer, 2017
This book constitutes the proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017, held in Zaragoza, Spain, in June 2017. Petri Nets 2017 is co-located with the Application of Concurrency to System Design Conference, ACSD 2017.
The 16 papers, 9 theory papers, 4 application papers, and 3 tool papers, ...
Добавлено: 6 мая 2017 г.
Татарников А. Д., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2016 Т. II С. 38-45
Генерация тестовых программ и анализ результатов их симуляции на проектной модели являются основным подходом к функциональной верификации микропроцессоров. Верификация – крайне трудоемкий процесс. По некоторым оценкам затраты на нее составляют около 70% от общих трудозатрат на разработку микропроцессора. Это связано с тем, что логика работы современных микропроцессоров содержит огромное количество состояний, и для того, чтобы ...
Добавлено: 12 декабря 2017 г.
Bialystok : Bialystok University of Technology, 2013
This volume contains the Proceedings of 22nd Concurrency, Specification and Programming (GS&P) Workshop held on September 25-27, 2013 in Warsaw. There were 48 submissions. Each submission was reviewed by two program committee members. The committee decided to accept 40 papers. The Workshop was initiated in the mid 1970s by computer scientists and mathematicians from Warsaw ...
Добавлено: 30 сентября 2013 г.
Татарников А. Д., Камкин А. С., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125-138
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является ...
Добавлено: 10 декабря 2017 г.
Berlin : Springer, 2014
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 ...
Добавлено: 3 июля 2014 г.
Внуков А. А., Тепляков М. В., Программы для ЭВМ. Базы данных. Топологии интегральных микросхем 2010 № 2(71)(Iч.) С. 92-92
Программа предназначена для поддержания заданных климатических условий в жилом или служебном помещении. Программа состоит из нескольких вычислительных блоков, включающих блок съёма данных регулируемого параметра и состояния исполнительного устройства, блок внесения изменений в регулируемый параметр и блок Трёхдиапазонного регулятора. Программа может быть использована при построении систем, состоящих из множества контроллеров КОНТАР, датчиков и исполнительных устройств для ...
Добавлено: 16 мая 2013 г.