Verification of Synchronous-automaton Programs
Abstract
This article presents a synchronous model of the automaton program. A technique of verification of synchronous-automaton programs has been developed. Some properties of the model are checked automatically. There is an ability of verifying user-defined properties. This technique helps to discover errors often made during the design process.
References
1. Кубасов, С.В. Синхронная модель автоматной программы / С.В. Кубасов, В.А. Соколов // Моделирование и анализ информационных систем. - 2007. - T.14, №1. - С. 11-18.
2. 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.
3. 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.
4. Bouali, A. Xeve: an Esterel Verification Environment : Version v1_3 : Rapport technique №0214 / Amar Bouali ; Inria, Institut National de Recherche en Informatique et en Automatique. - France, 1997. - 23 pages. - ISSN 0249-0803.
Review
For citations:
Kubasov S.V. Verification of Synchronous-automaton Programs. Modeling and Analysis of Information Systems. 2007;14(4):20-27. (In Russ.)
Views:
470
Email this article 