<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.3 20210610//EN" "https://jats.nlm.nih.gov/publishing/1.3/JATS-journalpublishing1-3.dtd">
<article article-type="research-article" dtd-version="1.3" xml:lang="en">
  <front>
    <journal-meta>
      <journal-title-group>
        <journal-title>Computing, Telecommunication and Control</journal-title>
        <trans-title-group xml:lang="ru">
          <trans-title>Информатика, телекоммуникации и управление</trans-title>
        </trans-title-group>
      </journal-title-group>
      <issn pub-type="epub">2687-0517</issn>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="publisher-id">17</article-id>
      <title-group>
        <article-title>UPPAAL-based verification of software-defined networks</article-title>
        <trans-title-group xml:lang="ru">
          <trans-title>Верификация программно-конфигурируемых сетей при помощи системы UPPAAL</trans-title>
        </trans-title-group>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <name>
            <surname>Podymov</surname>
            <given-names>Vladislav</given-names>
          </name>
          <email>valdus@yandex.ru</email>
        </contrib>
        <contrib contrib-type="author">
          <name>
            <surname>Popesko</surname>
            <given-names>Uliana</given-names>
          </name>
          <email>ulya_kiber@mail.ru</email>
        </contrib>
      </contrib-group>
      <pub-date publication-format="electronic" date-type="pub" iso-8601-date="2014-04-10">
        <day>10</day>
        <month>04</month>
        <year>2014</year>
      </pub-date>
      <issue>2</issue>
      <issue-id pub-id-type="publisher-id">193</issue-id>
      <fpage>169</fpage>
      <lpage>179</lpage>
      <abstract xml:lang="en">
        <p>special kind of computer networks in which the switching device control is fully centralized. This paper investigates the problems of formal description and verification of SDN as a real-time system. We provide a UML-based description of SDN, using the UML diagram editor Dia. To verify real-time properties of SDN, we use a well-known model-checking tool UPPAAL. The main result of the research is an approach for SDN verification, based on translation of SDN description into network of timed automata. Translation correctness is formalized and proved. A number of experiments were done to show that the approach can be used to verify real-time properties of SDN specified as TCTL formulae.</p>
      </abstract>
      <kwd-group xml:lang="en">
        <kwd>software-defined networks</kwd>
        <kwd>verification</kwd>
        <kwd>timed automata</kwd>
        <kwd>temporal logic</kwd>
        <kwd>UPPAAL</kwd>
      </kwd-group>
    </article-meta>
  </front>
</article>
