?
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., Zakharov V.
Translator: Zakharov V.
Software-dened networking (SDN) is an approach to building computer net- works that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and ow-table updating was dened in the form of a protocol known as OpenFlow. In this paper we describe an abstract formal model of SDN, introduce a tentative language for specication of SDN forwarding policies, and set up formally model-checking problems for SDNs.
Zakharov 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 ...
Added: October 13, 2015
Zakharov V., Чемерицкий Е. В., Моделирование и анализ информационных систем 2014 Т. 21 № 6 С. 57-69
Designing of network update algorithms is urgent for development of SDN control software. A particular case of Network Update Problem is that of restoring seamlessly a given network configuration after some packet forwarding rules have been disabled (say, at the expiry of their time-outs). We study this problem in the framework of a formal model ...
Added: September 30, 2015
Zakharov V., Чемерицкий Е. В., , 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.
Designing of network update algorithms is urgent for development of SDN control software. A particular case of Network Update Problem is that of adding a set of forwarding rules into flow-tables of SDN switches (say, to install new paths in the network) or restoring seamlessly a given network configuration after some packet forwarding rules have ...
Added: October 13, 2015
Zakharov V., Смелянский Р. Л., Чемерицкий Е. В., Моделирование и анализ информационных систем 2013 Т. 20 № 6 С. 33-48
Software-defined networking (SDN) is an approach to building computer networks that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and flow-table updating was defined in the form of a protocol known ...
Added: September 30, 2015
Kamkin A., М. : МАКС Пресс, 2018
This textbook is devoted to formal methods for program verification and is based on the lectures given by the author at CMC MSU, DCAM MIPT, and FCS HSE. It describes the basics of such approaches as deductive analysis and model checking. The list of topics includes formal semantics of programming languages (operational and axiomatic semantics), ...
Added: November 2, 2018
Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the ninth workshop dedicated to formalisms for program semantics, formal models and verification, programming and specification languages, algebraic and logical aspects of programming. ...
Added: October 26, 2018
Zakharov V., Коннов И. В., Моделирование и анализ информационных систем 2010 Т. 17 № 4 С. 78-87
Наиболее значительную трудность для всех инструментальных средств верификации моделей программ
создает эффект комбинаторного взрыва. Один из способов сократить размер проверяемой модели $M$ ---
выбрать подходящую группу автоморфизмов $G$ размеченной системы переходов $M$ и построить фактор-модель $M/G$.
Состояниями фактор-модели $M/G$ служат орбиты состояний модели $M$ относительно группы $G$; также известно,
что модели $M/G$ и $M$ находятся ...
Added: September 30, 2015
Zakharov V.A., Volkanov D. Y., Zorin D. A. et al., 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 ...
Added: October 13, 2015
И. В. Ефименко, Форсайт 2013
This paper represents an approach to development and implementation of the formal model of technological roadmapping (TRM). The research was carried out based on the analysis of the best practices in the domain. It integrates the experience of a wide range of TRM projects. The proposed model provides basis for developing tools for TRM automation, ...
Added: August 12, 2013
Tatarnikov A., Kamkin A., Проценко А. С. et al., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2-8
In this paper, a specification-based test program generator for functional verification of RISC-V microprocessors is presented. The tool is based on the MicroTESK framework and consists of two main parts: (1) the formal specifications of the RISC-V ISA and (2) the ISA-independent generation core. Test programs are generated on the basis of the ISA specifications and test templates ...
Added: October 30, 2018
Zakharov V., Подымов В. В., Алтухов В. С. et al., , 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.
In this paper we present a VERifying MONiTor (VERMONT) which is a software toolset for checking the consistency of network configurations with formally specified invariants of Packet Forwarding Policies (PFP). Correct and safe management of networks is a very hard task. Every time the current load of flow tables should satisfy certain requirements. Some packets ...
Added: October 13, 2015
Zakharov V., Волканов Д. Ю., Зорин Д. А. et al., Программирование 2015 № 6 С. 72-86
Проверка правильности функционирования распределенных программ --- это одна из наиболее трудных и актуальных задач современного программирования. В статье описано комбинированное программно-инструментальное средство верификации распределенных вычислительных систем реального времени (РВС РВ). Для описания РВС РВ используется универсальный язык моделирования UML. Семантика диаграмм состояний UML определяется на основе модели вычислений иерархических временных автоматов. Средство верификации диаграмм UML ...
Added: October 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 ...
Added: January 24, 2018
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2018 Т. 25 № 5 С. 506-524
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. The behaviour of such a reactive system displays itself in the correspondence between flows of control signals ...
Added: October 26, 2018
Tatarnikov A., Kamkin A., Проценко А. С. et al., Труды Института системного программирования РАН 2016 Т. 28 № 6 С. 87-102
ARM is a family of microprocessor instruction set architectures developed in a company with the same name. The newest architecture of this family, ARMv8, contains a large number of instructions of various types and is notable for its complex organization of virtual memory, which includes hardware support for multilevel address translation and virtualization. All of ...
Added: November 24, 2017
Gnatenko A., Zakharov V., 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 ...
Added: October 17, 2019
Tatarnikov A., Известия высших учебных заведений. Физика 2016 Т. 59 № 8-2 С. 97-100
The paper proposes a method of automated construction of behavior models of microprocessors, which are used in the process of test program generation to predict the results. The proposed method is based on using formal specifications of instruction set architecture. The method is implemented in MicroTESK, a test program generation tool being developed at ISP ...
Added: February 2, 2018
Gnatenko A., Zakharov V., Системная информатика 2020 Vol. 17 P. 21-32
Sequential reactive systems such as controllers, device drivers, computer interpreters operate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems of this kind. Since runs of transducers develop ...
Added: November 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, ...
Added: May 6, 2017
Tatarnikov A., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2016 Т. II С. 38-45
Test program generation and simulation is the most widely used approach to functional verification of microprocessors. Functional verification is a quite time consuming process. According to various estimates, it accounts for more than 70% of overall resources spent on designing a new microprocessor. This can be explained by the fact that modern hardware designs have ...
Added: December 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 ...
Added: September 30, 2013
Tatarnikov A., Kamkin A., Проценко А. С., Proceedings of the Institute for System Programming of the RAS 2015 Vol. 27 No. 3 P. 125-138
A memory subsystem is one of the key components of a microprocessors. It consists of a number of storage devices (instruction buffers, address translation buffers, multilevel cache memory, main memory, and others) organized into a complex hierarchical structure. Huge state space of a memory subsystem makes its functional verification extremely labor consuming. Nowadays, the main ...
Added: December 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 ...
Added: July 3, 2014
Vnukov A., Тепляков М. В., Программы для ЭВМ. Базы данных. Топологии интегральных микросхем 2010 № 2(71)(Iч.) С. 92-92
Программа предназначена для поддержания заданных климатических условий в жилом или служебном помещении. Программа состоит из нескольких вычислительных блоков, включающих блок съёма данных регулируемого параметра и состояния исполнительного устройства, блок внесения изменений в регулируемый параметр и блок Трёхдиапазонного регулятора. Программа может быть использована при построении систем, состоящих из множества контроллеров КОНТАР, датчиков и исполнительных устройств для ...
Added: May 16, 2013