Synchronous model of automaton program
Abstract
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.
About the Authors
S. V. Kubasov
Ярославский государственный университет
Russian Federation
Russian Federation
V. A. Sokolov
Ярославский государственный университет
Russian Federation
Russian Federation
References
1. Шопырин, Д. Г. Синхронное программирование / Д. Г. Шопырин, А. А. Шалыто // Информационно-управляющие системы. - 2004. - №3. - С. 35-42.
2. 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.
3. 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.
4. 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.
5. 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.
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.
7. 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.
8. Кузнецов, Б. П. Психология автоматного программирования / Б. П. Кузнецов // BYTE / Россия. -2000. - №11. - С. 22-29.
9. Гуров, В. С. UML. SWITCH-Технология. Eclipse / В. С. Гуров, М. А. Мазин, А. С. Нарвский, А. А. Ша-лыто // Информационно-управляющие системы. - 2005. - №6(13). - С. 12-17.
10. Гуров, В. С. Исполняемый UML из России / В. С. Гуров, А. С. Нарвский, А. А. Шалыто. // PC Week/RE. - 2005. - №26. - С. 18-19.
11. Шалыто, А. А. SWITCH-Технология - автоматный подход к созданию программного обеспечения «реактивных» систем / А. А. Шалыто, Н. И. Туккуль // Программирование. - 2001. - №5. - С. 45-62.
12. Наумов, А. С. Объектно-ориентированное программирование с явным выделением состояний: Бака¬лаврская работа / А. С. Наумов; СПбГУ ИТМО. - СПб., 2004. - 209 с.
13. Шалыто, А. А. Программирование с явным выделением состояний / А. А. Шалыто, Н. И. Туккель // Мир ПК. - 2001. - №8. - С. 116-121; №9. - С. 132-138.
Review
For citations:
Kubasov S.V., Sokolov V.A. Synchronous model of automaton program. Modeling and Analysis of Information Systems. 2007;14(1):11-18. (In Russ.)
Views:
429
Email this article 