maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1109Research ArticleОригинальные статьиArticlesСинхронная модель автоматной программыSynchronous model of automaton programКубасовС. В.KubasovS. V.noemail@neicon.ruСоколовВ. А.SokolovV. A.noemail@neicon.ruЯрославский государственный университетRussian Federation2007200320071411118Copyright © Кубасов С.В., Соколов В.А., 20072007Кубасов С.В., Соколов В.А.Kubasov S.V., Sokolov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1109

Предлагается модель автоматной программы, удовлетворяющая требованиям синхронной модели. Создание формальной модели автоматной программы предоставляет возможность применения технологий и инструментов верификации синхронных программ для проверки автоматных программ. В частности предполагается использование языка esterel с пакетом программ компании Esterel Technologies Inc. для построения верификатора.

This article presents a model of automaton program that satisfies synchronous model requirements. A formal automaton program model lets to use an existing technologies and tools of synchronous programs verification for checking automaton programs. An Esterel language and an Esterel Technologies Inc. toolbox will be used to build a program verifier.

ReferencesШопырин, Д. Г. Синхронное программирование / Д. Г. Шопырин, А. А. Шалыто // Информационно-управляющие системы. - 2004. - №3. - С. 35-42.Шопырин, Д. Г. Синхронное программирование / Д. Г. Шопырин, А. А. Шалыто // Информационно-управляющие системы. - 2004. - №3. - С. 35-42.Benveniste, A. The Synchronous Languages 12 Years Later: Invited Paper / A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. le Gurnic, R. de Simone // Proceedings of the IEEE. - 2003, January. - vol. 91, no. 1. - pp. 64-83.Benveniste, A. The Synchronous Languages 12 Years Later: Invited Paper / A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. le Gurnic, R. de Simone // Proceedings of the IEEE. - 2003, January. - vol. 91, no. 1. - pp. 64-83.Andre, C. Representation and Analysis of Reactive Behaviors: A Synchronous Approach / C. Andre // Computational Engineering in Systems Applications (CESA), IMACS Multiconference. - Lille, France. -1996, July. - pp. 19-29. - ISBN 2-9502908-7-6.Andre, C. Representation and Analysis of Reactive Behaviors: A Synchronous Approach / C. Andre // Computational Engineering in Systems Applications (CESA), IMACS Multiconference. - Lille, France. -1996, July. - pp. 19-29. - ISBN 2-9502908-7-6.Barros, T. Formal specification and verification of distributed component systems: PhD thesis: defence date: 25.11.2005 / T. Barros; Universite de Nice; INRIA Sophia Antipolis. - France, 2005. - 158 p.Barros, T. Formal specification and verification of distributed component systems: PhD thesis: defence date: 25.11.2005 / T. Barros; Universite de Nice; INRIA Sophia Antipolis. - France, 2005. - 158 p.Halbwachs, N. Synchronous programming of reactive systems, a tutorial and commented bibliography / N. Halbwachs // Tenth International Conference on Computer-Aided Verification, CAV'98, Vancouver (B.C.), Canada: LNCS 1427, Springer Verlag, 1998, June. - vol. 1427. - pp. 1-16. - ISBN 3-540-64608-6.Halbwachs, N. Synchronous programming of reactive systems, a tutorial and commented bibliography / N. Halbwachs // Tenth International Conference on Computer-Aided Verification, CAV'98, Vancouver (B.C.), Canada: LNCS 1427, Springer Verlag, 1998, June. - vol. 1427. - pp. 1-16. - ISBN 3-540-64608-6.Berry, G. The Esterel v5 Language Primer, version v5_91: Документация к программному обеспечению Esterel Compiler, version 5.91. Ecole des Mines de Paris (EMP), ARMINES, and INRIA / G. Berry and the Esterel Team. - 2000, 5 June.Berry, G. The Esterel v5 Language Primer, version v5_91: Документация к программному обеспечению Esterel Compiler, version 5.91. Ecole des Mines de Paris (EMP), ARMINES, and INRIA / G. Berry and the Esterel Team. - 2000, 5 June.Berry, G. The Esterel v5_91 System Manual: Документация к программному обеспечению Esterel Compiler, version 5.91. Ecole des Mines de Paris (EMP), ARMINES, and INRIA / G. Berry. - 2000, 5 June.Berry, G. The Esterel v5_91 System Manual: Документация к программному обеспечению Esterel Compiler, version 5.91. Ecole des Mines de Paris (EMP), ARMINES, and INRIA / G. Berry. - 2000, 5 June.Кузнецов, Б. П. Психология автоматного программирования / Б. П. Кузнецов // BYTE / Россия. -2000. - №11. - С. 22-29.Кузнецов, Б. П. Психология автоматного программирования / Б. П. Кузнецов // BYTE / Россия. -2000. - №11. - С. 22-29.Гуров, В. С. UML. SWITCH-Технология. Eclipse / В. С. Гуров, М. А. Мазин, А. С. Нарвский, А. А. Ша-лыто // Информационно-управляющие системы. - 2005. - №6(13). - С. 12-17.Гуров, В. С. UML. SWITCH-Технология. Eclipse / В. С. Гуров, М. А. Мазин, А. С. Нарвский, А. А. Ша-лыто // Информационно-управляющие системы. - 2005. - №6(13). - С. 12-17.Гуров, В. С. Исполняемый UML из России / В. С. Гуров, А. С. Нарвский, А. А. Шалыто. // PC Week/RE. - 2005. - №26. - С. 18-19.Гуров, В. С. Исполняемый UML из России / В. С. Гуров, А. С. Нарвский, А. А. Шалыто. // PC Week/RE. - 2005. - №26. - С. 18-19.Шалыто, А. А. SWITCH-Технология - автоматный подход к созданию программного обеспечения «реактивных» систем / А. А. Шалыто, Н. И. Туккуль // Программирование. - 2001. - №5. - С. 45-62.Шалыто, А. А. SWITCH-Технология - автоматный подход к созданию программного обеспечения «реактивных» систем / А. А. Шалыто, Н. И. Туккуль // Программирование. - 2001. - №5. - С. 45-62.Наумов, А. С. Объектно-ориентированное программирование с явным выделением состояний: Бака¬лаврская работа / А. С. Наумов; СПбГУ ИТМО. - СПб., 2004. - 209 с.Наумов, А. С. Объектно-ориентированное программирование с явным выделением состояний: Бака¬лаврская работа / А. С. Наумов; СПбГУ ИТМО. - СПб., 2004. - 209 с.Шалыто, А. А. Программирование с явным выделением состояний / А. А. Шалыто, Н. И. Туккель // Мир ПК. - 2001. - №8. - С. 116-121; №9. - С. 132-138.Шалыто, А. А. Программирование с явным выделением состояний / А. А. Шалыто, Н. И. Туккель // Мир ПК. - 2001. - №8. - С. 116-121; №9. - С. 132-138.

The authors declare that there are no conflicts of interest present.