Preview

Моделирование и анализ информационных систем

Расширенный поиск

Формальная модель и задачи верификации программно-конфигурируемых сетей

https://doi.org/10.18255/1818-1015-2013-6-36-51

Аннотация

Программно-коммутируемые сети (ПКС) — это класс компьютерных телекоммуникационных сетей, появившийся несколько лет назад в стремлении упростить проектирование и повысить гибкость управления сетями за счет разделения потоков данных (пакетов) и потоков управления (сообщений и команд), циркулирующих в сетях. ПКС представляет собой распределенную систему, в которой один или несколько контроллеров управляют множеством сетевых коммутаторов, обеспечивающих продвижение пакетов по каналам сети. Функциональные возможности и порядок взаимодействия коммутаторов и контроллеров ПКС определяются протоколом OpenFlow. На основе аппарата булевых функций и дискретных преобразователей нами предложена формальная модель ПКС, введен прототип формального языка спецификаций, поставлены задачи верификации моделей ПКС и получены оценки их сложности. Для одной из задач верификации моделей ПКС описан метод ее решения, на основе которого разработано программно-инструментальное средство верификации ПКС.

Об авторах

Владимир Анатольевич Захаров
Московский государственный университет им. М.В. Ломоносова
Россия

Центр прикладных исследований компьютерных сетей, доцент,

119991, Москва, ГСП-1, Ленинские горы, д. 1, стр. 52



Руслан Леонидович Смелянский
Московский государственный университет им. М.В. Ломоносова
Россия

Центр прикладных исследований компьютерных сетей, профессор,

119991, Москва, ГСП-1, Ленинские горы, д. 1, стр. 52



Евгений Викторович Чемерицкий
Московский государственный университет им. М.В. Ломоносова
Россия

Центр прикладных исследований компьютерных сетей, аспирант,

119991, Москва, ГСП-1, Ленинские горы, д. 1, стр. 52



Список литературы

1. OpenFlow Switch Specification. Version 1.4.0, August 5, 2013. www.opennetworking.org.

2. Kim H., Feamster N. Improving network management with software defined networking // Communications Magazine. IEEE, 2013. P. 114—119.

3. Al-Shaer E., Marrero W., El-Atawy A., El Badawi K. Network Configuration in a Box: Toward End-to-End Verification of Network Reachability and Security // 17th IEEE International Conference on Network Protocols (ICNP’09). Princeton, New Jersey, USA, 2009. P. 123—132.

4. Mai H., Khurshid A., Agarwal R., Caesar M., Godfrey R.B., King S.T. Debugging of the Data Plane with Anteater // Proceedings of the ACM SIGCOMM conference. 2011. P. 290—301.

5. Kazemian P., Varghese G., McKeown N. Header space analysis: Static checking for networks // Proceedings of 9-th USENIX Symposium on Networked Systems Design and Implementation. 2012.

6. Khurshid A., Zhou W., Caesar M., Godfrey P.B. VeriFlow: Verifying Network-Wide Invariants in Real Time // Proceedings of International Conference "Hot Topics in Software Defined Networking"(HotSDN). 2012. P. 49—54.

7. Gutz S., Story A., Schlesinger C., Foster N. Splendid isolation: A Slice Abstraction for Software Defined Networks // Proceedings of International Conference "Hot Topics in Software Defined Networking"(HotSDN). 2012. P. 79—84.

8. Reitblatt M., Foster N., Rexford J.,Walker D. Consistent updates for software-defined networks: change you can believe in! // HotNets. 2011. V. 7.

9. Reitblatt M., Foster N., Rexford J., Schlesinger C., Walker D. Abstractions for Network Update // Proceedings of ACM SIGCOMM conference. 2012. P. 323—334.

10. Canini M., Venzano D., Peresini P., Kostic D., Rexford J. A NICE way to Test OpenFlow Applications // Proceedings of Networked Systems Design and Implementation, April 2012.

11. Immerman N. Languages that capture complexity classes // SIAM Journal of Computing. 1987. V. 16, No 4. P. 760—778.

12. Immerman N., Vardi M. Model checking and transitive closure logic // Lecture Notes in Computer Science. 1997. P. 291—302.

13. Alechina N., Immerman N. Reachability logic: efficient fragment of transitive closure logic // Logic Journal of IGPL. 2000. V. 8, No 3. P. 325—337.

14. Galil Z., Hierarchies of Complete Problems // Acta Informatica. 1976. No 6. P. 77—88.


Рецензия

Для цитирования:


Захаров В.А., Смелянский Р.Л., Чемерицкий Е.В. Формальная модель и задачи верификации программно-конфигурируемых сетей. Моделирование и анализ информационных систем. 2013;20(6):36-51. https://doi.org/10.18255/1818-1015-2013-6-36-51

For citation:


Zakharov V.A., Smelyansky R.L., Chemeritsky E.V. A Formal Model and Verification Problems for Software Defined Networks. Modeling and Analysis of Information Systems. 2013;20(6):36-51. (In Russ.) https://doi.org/10.18255/1818-1015-2013-6-36-51

Просмотров: 1041


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)