<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.3 20210610//EN" "JATS-journalpublishing1-3.dtd">
<article article-type="research-article" dtd-version="1.3" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xml:lang="ru"><front><journal-meta><journal-id journal-id-type="publisher-id">mais</journal-id><journal-title-group><journal-title xml:lang="ru">Моделирование и анализ информационных систем</journal-title><trans-title-group xml:lang="en"><trans-title>Modeling and Analysis of Information Systems</trans-title></trans-title-group></journal-title-group><issn pub-type="ppub">1818-1015</issn><issn pub-type="epub">2313-5417</issn><publisher><publisher-name>Yaroslavl State University</publisher-name></publisher></journal-meta><article-meta><article-id pub-id-type="doi">10.18255/1818-1015-2014-6-31-43</article-id><article-id custom-type="elpub" pub-id-type="custom">mais-69</article-id><article-categories><subj-group subj-group-type="heading"><subject>Research Article</subject></subj-group><subj-group subj-group-type="section-heading" xml:lang="ru"><subject>Оригинальные статьи</subject></subj-group><subj-group subj-group-type="section-heading" xml:lang="en"><subject>Articles</subject></subj-group></article-categories><title-group><article-title>Верификация алгоритмов мультиагентного анализа данных с помощью системы проверки моделей SPIN</article-title><trans-title-group xml:lang="en"><trans-title>Using SPIN for Verification of Multi-agent Data Analysis</trans-title></trans-title-group></title-group><contrib-group><contrib contrib-type="author" corresp="yes"><name-alternatives><name name-style="eastern" xml:lang="ru"><surname>Гаранина</surname><given-names>Наталья Олеговна</given-names></name><name name-style="western" xml:lang="en"><surname>Garanina</surname><given-names>N. O.</given-names></name></name-alternatives><bio xml:lang="ru"><p>старший научный сотрудник, 630090 Россия, г. Новосибирск, проспект Академика Лаврентьева, 6</p></bio><bio xml:lang="en"><p>старший научный сотрудник,</p><p>A.P. Ershov Institute of Informatics Systems, Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia</p></bio><email xlink:type="simple">garanina@iis.nsk.su</email><xref ref-type="aff" rid="aff-1"/></contrib><contrib contrib-type="author" corresp="yes"><name-alternatives><name name-style="eastern" xml:lang="ru"><surname>Бодин</surname><given-names>Евгений Викторович</given-names></name><name name-style="western" xml:lang="en"><surname>Bodin</surname><given-names>E. V.</given-names></name></name-alternatives><bio xml:lang="ru"><p>научный сотрудник, 630090 Россия, г. Новосибирск, проспект Академика Лаврентьева, 6</p></bio><bio xml:lang="en"><p>научный сотрудник,</p><p>A.P. Ershov Institute of Informatics Systems, Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia</p></bio><email xlink:type="simple">bodin@iis.nsk.su</email><xref ref-type="aff" rid="aff-1"/></contrib><contrib contrib-type="author" corresp="yes"><name-alternatives><name name-style="eastern" xml:lang="ru"><surname>Сидорова</surname><given-names>Елена Анатольевна</given-names></name><name name-style="western" xml:lang="en"><surname>Sidorova</surname><given-names>E. A.</given-names></name></name-alternatives><bio xml:lang="ru"><p>старший научный сотрудник, 630090 Россия, г. Новосибирск, проспект Академика Лаврентьева, 6</p></bio><bio xml:lang="en"><p>старший научный сотрудник,</p><p>A.P. Ershov Institute of Informatics Systems, Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia</p></bio><email xlink:type="simple">lena@iis.nsk.su</email><xref ref-type="aff" rid="aff-1"/></contrib></contrib-group><aff-alternatives id="aff-1"><aff xml:lang="ru"><institution>Институт систем информатики им. А.П. Ершова СО РАН</institution><country>Россия</country></aff><aff xml:lang="en"><institution>Russian Academy of Sciences Siberian Branch</institution><country>Russian Federation</country></aff></aff-alternatives><pub-date pub-type="collection"><year>2014</year></pub-date><pub-date pub-type="epub"><day>20</day><month>12</month><year>2014</year></pub-date><volume>21</volume><issue>6</issue><fpage>31</fpage><lpage>43</lpage><permissions><copyright-statement>Copyright &amp;#x00A9; Гаранина Н.О., Бодин Е.В., Сидорова Е.А., 2014</copyright-statement><copyright-year>2014</copyright-year><copyright-holder xml:lang="ru">Гаранина Н.О., Бодин Е.В., Сидорова Е.А.</copyright-holder><copyright-holder xml:lang="en">Garanina N.O., Bodin E.V., Sidorova E.A.</copyright-holder><license xml:lang="ru" license-type="creative-commons-attribution" xlink:href="https://creativecommons.org/licenses/by/4.0/" xlink:type="simple"><license-p>Данная работа распространяется под лицензией Creative Commons Attribution 4.0.</license-p></license><license xml:lang="en" license-type="creative-commons-attribution" xlink:href="https://creativecommons.org/licenses/by/4.0/" xlink:type="simple"><license-p>This work is licensed under a Creative Commons Attribution 4.0 License.</license-p></license></permissions><self-uri xlink:href="https://www.mais-journal.ru/jour/article/view/69">https://www.mais-journal.ru/jour/article/view/69</self-uri><abstract><p>В статье представлен подход к формальной верификации алгоритмов мультиагентного анализа данных для пополнения онтологий. Агенты системы на основе входных данных устанавливают значения элементов объектов, полученных на предварительной стадии анализа. Агенты параллельно осуществляют проверку семантической и синтаксической согласованности, используя правила пополнения онтологий и обработки данных. Поскольку агенты действуют параллельно, необходимо верифицировать некоторые важные свойства системы, связанные с этим, например, свойство корректности определения завершения работы системы. В нашем подходе используется инструмент проверки моделей SPIN. Протоколы агентов записаны на языке Promela, а свойства мультиагентной системы анализа данных выражены в логике LTL. Мы провели ряд экспериментов по проверке данной модели.</p></abstract><trans-abstract xml:lang="en"><p>The paper presents an approach to formal verification of multi-agent data analysis algorithms for ontology population. The system agents correspond to information items of the input data and the rule of ontology population and data processing. They determine values of information objects obtained at the preliminary phase of the analysis. The agents working in parallel check the syntactic and semantic consistency of tuples of information items. Since the agents operate in parallel, it is necessary to verify some important properties of the system related to it, such as the property that the controller agent correctly determines the system termination. In our approach, the model checking tool SPIN is used. The protocols of agents are written in Promela language (the input language of the tool) and the properties of the multi-agent data analysis system are expressed in the liner time logic LTL. We carried out several experiments to check this model in various modes of the tool and various numbers of agents.</p></trans-abstract><kwd-group xml:lang="ru"><kwd>пополнение онтологий</kwd><kwd>мультиагентные системы</kwd><kwd>проверка моделей</kwd><kwd>система верификации SPIN</kwd></kwd-group><kwd-group xml:lang="en"><kwd>ontology population</kwd><kwd>multi-agent system</kwd><kwd>model checking</kwd><kwd>SPIN</kwd></kwd-group><funding-group><funding-statement xml:lang="ru">РФФИ, Президиум РАН</funding-statement></funding-group></article-meta></front><back><ref-list><title>References</title><ref id="cit1"><label>1</label><citation-alternatives><mixed-citation xml:lang="ru">Aref M.M. A Multi-Agent System for Natural Language Understanding // International Conference on Integration of Knowledge Intensive Multi-Agent Systems. 2003. 36.</mixed-citation><mixed-citation xml:lang="en">Aref M.M. A Multi-Agent System for Natural Language Understanding // International Conference on Integration of Knowledge Intensive Multi-Agent Systems. 2003. 36.</mixed-citation></citation-alternatives></ref><ref id="cit2"><label>2</label><citation-alternatives><mixed-citation xml:lang="ru">A.M.B.R. Carvalho, D.S. de Paiva, J.S. Sichman, J.L.T. da Silva, R.S. Wazlawick &amp; V.L.S. de Lima Multi-Agent Systems for Natural Language Processing // Multi Agent Systems Models Architecture and Appications: Proceedings of the II Iberoamerican Workshop on D.A.I. and M.A.S / Francisco J. Garijo &amp; Cristian Lemaitre (eds.) Toledo, Spain, October 1–2 1998. P. 61–69.</mixed-citation><mixed-citation xml:lang="en">A.M.B.R. Carvalho, D.S. de Paiva, J.S. Sichman, J.L.T. da Silva, R.S. Wazlawick &amp; V.L.S. de Lima Multi-Agent Systems for Natural Language Processing // Multi Agent Systems Models Architecture and Appications: Proceedings of the II Iberoamerican Workshop on D.A.I. and M.A.S / Francisco J. Garijo &amp; Cristian Lemaitre (eds.) Toledo, Spain, October 1–2 1998. P. 61–69.</mixed-citation></citation-alternatives></ref><ref id="cit3"><label>3</label><citation-alternatives><mixed-citation xml:lang="ru">Banares-Alcantara R., Jimenez R., Aldea L. Multi-agent systems for ontology-based information retrieval // European Symposium on Computer-Aided Chemical Engineering-15 (ESCAPE-15). Barcelona, Espana, 2005.</mixed-citation><mixed-citation xml:lang="en">Banares-Alcantara R., Jimenez R., Aldea L. Multi-agent systems for ontology-based information retrieval // European Symposium on Computer-Aided Chemical Engineering-15 (ESCAPE-15). Barcelona, Espana, 2005.</mixed-citation></citation-alternatives></ref><ref id="cit4"><label>4</label><citation-alternatives><mixed-citation xml:lang="ru">Cheng X., Xie Y., Yang T. Study of Multi-Agent Information Retrieval Model in Semantic Web // Proc. of the 2008 International Workshop on Education Technology and Training and 2008 International Workshop on Geoscience and Remote Sensing (ETTANDGRS’08). 2008. Vol. 02. P. 636–639.</mixed-citation><mixed-citation xml:lang="en">Cheng X., Xie Y., Yang T. Study of Multi-Agent Information Retrieval Model in Semantic Web // Proc. of the 2008 International Workshop on Education Technology and Training and 2008 International Workshop on Geoscience and Remote Sensing (ETTANDGRS’08). 2008. Vol. 02. P. 636–639.</mixed-citation></citation-alternatives></ref><ref id="cit5"><label>5</label><citation-alternatives><mixed-citation xml:lang="ru">Clark K.L., Lazarou V.S. A Multi-Agent System for Distributed Information Retrieval on the World Wide Web // Proc. of the 6th Workshop on Enabling Technologies on Infrastructure for Collaborative Enterprises. 1997. P. 87–93.</mixed-citation><mixed-citation xml:lang="en">Clark K.L., Lazarou V.S. A Multi-Agent System for Distributed Information Retrieval on the World Wide Web // Proc. of the 6th Workshop on Enabling Technologies on Infrastructure for Collaborative Enterprises. 1997. P. 87–93.</mixed-citation></citation-alternatives></ref><ref id="cit6"><label>6</label><citation-alternatives><mixed-citation xml:lang="ru">D. Fum, G. Guida, C. Tasso A Distributed Multi-Agent Architecture for Natural Language Processing // Proc. of the 12th conference on Computational linguistics (COLING ’88). 1988. Vol. 2. P. 812–814.</mixed-citation><mixed-citation xml:lang="en">D. Fum, G. Guida, C. Tasso A Distributed Multi-Agent Architecture for Natural Language Processing // Proc. of the 12th conference on Computational linguistics (COLING ’88). 1988. Vol. 2. P. 812–814.</mixed-citation></citation-alternatives></ref><ref id="cit7"><label>7</label><citation-alternatives><mixed-citation xml:lang="ru">Garanina N., Sidorova E., Bodin E. A Multi-agent Approach to Unstructured Data Analysis Based on Domain-specific Onthology // Proc. of the 22nd International Workshop on Concurrency, Specification and Programming. Warsaw, Poland, Sept. 25–27, 2013. CEUR Workshop Proceedings, Vol. 1032. P. 122–132.</mixed-citation><mixed-citation xml:lang="en">Garanina N., Sidorova E., Bodin E. A Multi-agent Approach to Unstructured Data Analysis Based on Domain-specific Onthology // Proc. of the 22nd International Workshop on Concurrency, Specification and Programming. Warsaw, Poland, Sept. 25–27, 2013. CEUR Workshop Proceedings, Vol. 1032. P. 122–132.</mixed-citation></citation-alternatives></ref><ref id="cit8"><label>8</label><citation-alternatives><mixed-citation xml:lang="ru">Garanina N., Bodin E. Distributed Termination Detection by Counting Agent // Proc. of the 23nd International Workshop on Concurrency, Specification and Programming. Chemnitz, Germany, 29 September – 01 Oktober 2014. Humboldt-Universit¨at zu Berlin, 2014. P. 69–79.</mixed-citation><mixed-citation xml:lang="en">Garanina N., Bodin E. Distributed Termination Detection by Counting Agent // Proc. of the 23nd International Workshop on Concurrency, Specification and Programming. Chemnitz, Germany, 29 September – 01 Oktober 2014. Humboldt-Universit¨at zu Berlin, 2014. P. 69–79.</mixed-citation></citation-alternatives></ref><ref id="cit9"><label>9</label><citation-alternatives><mixed-citation xml:lang="ru">Holzmann G.J. The Spin Model Checker: Primer and Reference Manual // Addison Wesley Pub, 2003. P. 608.</mixed-citation><mixed-citation xml:lang="en">Holzmann G.J. The Spin Model Checker: Primer and Reference Manual // Addison Wesley Pub, 2003. P. 608.</mixed-citation></citation-alternatives></ref><ref id="cit10"><label>10</label><citation-alternatives><mixed-citation xml:lang="ru">Minakov I., Rzevski G., Skobelev P., Volman S. Creating Contract Templates for Car Insurance Using Multi-agent Based Text Understanding and Clustering// Proc. Holonic and Multi-Agent Systems for Manufacturing, Third International Conference on Industrial Applications of Holonic and Multi-Agent Systems, HoloMAS 2007. Regensburg, Germany, September 3–5, 2007. Springer, Lecture Notes in Computer Science, 2007. Vol. 4659. P. 361–370.</mixed-citation><mixed-citation xml:lang="en">Minakov I., Rzevski G., Skobelev P., Volman S. Creating Contract Templates for Car Insurance Using Multi-agent Based Text Understanding and Clustering// Proc. Holonic and Multi-Agent Systems for Manufacturing, Third International Conference on Industrial Applications of Holonic and Multi-Agent Systems, HoloMAS 2007. Regensburg, Germany, September 3–5, 2007. Springer, Lecture Notes in Computer Science, 2007. Vol. 4659. P. 361–370.</mixed-citation></citation-alternatives></ref><ref id="cit11"><label>11</label><citation-alternatives><mixed-citation xml:lang="ru">C.T. dos Santos, P. Quaresma, I. Rodrigues, R. Vieira A Multi-Agent Approach to Question Answering // Computational Processing of the Portuguese Language: 7th International Workshop, PROPOR 2006. Itatiaia, Brazil, May 2006 (PROPOR’2006). LNAI 3960, 13–17 de Maio de 2006. Berlin/Heidelberg: Springer Verlag. P. 131–139.</mixed-citation><mixed-citation xml:lang="en">C.T. dos Santos, P. Quaresma, I. Rodrigues, R. Vieira A Multi-Agent Approach to Question Answering // Computational Processing of the Portuguese Language: 7th International Workshop, PROPOR 2006. Itatiaia, Brazil, May 2006 (PROPOR’2006). LNAI 3960, 13–17 de Maio de 2006. Berlin/Heidelberg: Springer Verlag. P. 131–139.</mixed-citation></citation-alternatives></ref></ref-list><fn-group><fn fn-type="conflict"><p>The authors declare that there are no conflicts of interest present.</p></fn></fn-group></back></article>
