Современная электроника №1/2021

ПРОЕКТИРОВАНИЕ И МОДЕЛИРОВАНИЕ 46 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 1 2021 дит из состояния А2 в состояние А4. При этом включённым остаётся ком- прессор К2. Переход автомата А в состо- яние А4 приводит к переходу автомата B из состояния B7 в состояние B3, кото- рому соответствует продувка реторт R1/R2 воздухом. При этом открыты клапаны V4, V6, V9, V10. Снятие сигнала Run приводит к пере- ходу автомата А в начальное состоя- ние А1. При этом автомат B, находясь в любом состоянии, также переходит в начальное состояние B1. В начальных состояниях всё оборудование отклю- чено. Математическое и программное обеспечение Рассмотренный алгоритм в виде СВА представляет математическое обе- спечение. Программное обеспечение является формальной и изоморфной [10] трансляцией математическо- го обеспечения (графов переходов). Трансляция может быть ручной или автоматической при наличии транс- лятора на целевой язык программиро- вания. Также платформа Rodin поддер- живает автоматическую трансляцию Рис. 4. Граф переходов автомата В моделей Event-B на языки C, C++, C # , Java [17]. Для создания сверхнадёжного про- граммного обеспечения написа- ние кода вручную противопоказано. Во избежание ошибок нужно исполь- зовать автоматическую кодогенерацию по исходной модели. Это даёт гарантию эквивалентности поведения програм- мы и её модели. Заключение В статье рассмотрены автоматный алгоритм управления и платформа Rodin. Алгоритм управления был создан в виде СВА и поэтому является строгим математическим объектом, удобным для формального анализа. Для вери- фикации алгоритма требуется предста- вить СВА с помощью аксиом и доказать ряд теорем, соответствующих предъяв- ляемым требованиям надёжности и без- опасности. Для этого будет использо- ваться платформа Rodin. Литература 1. Нейзов М. Формальный дедуктивный ана- лиз автоматного алгоритма управления генератором эндогаза с помощью плат- формы Rodin. Часть 1. Определение тре- бований надёжности и безопасности работы генератора эндогаза. Современ- ная электроника. 2020. № 9. 2. Кузнецов О. П., Адельсон-Вельский Г. М. Дискретная математика для инженера. 2-е изд., перераб. и доп. Энергоатомиз- дат. М. 1988. С. 480. 3. URL: www3.hhu.de/stups/handbook/rodin. 4. URL: wiki.event-b.org. 5. Abrial J. R. Modelling in Event-B: System and Software Engineering. Cambridge Univ. Press. 2010. 6. Robinson K. System Modelling & Design. Using Event-B. Draft book. 2012. P. 142. 7. Поликарпова Н. И., Шалыто А. А. Авто- матное программирование. 2008. С. 167. 8. Шалыто А. А. Switch-технология. Алго- ритмизация и программирование задач логического управления. Наука. СПб. 1998. С. 628. 9. КарповЮ. Г. Теория автоматов: учебник для вузов. – 1-е изд. Издат. дом ПИТЕР. СПб. 2003. С. 208. 10. Шалыто А. А. Автоматное проекти- рование программ. Алгоритмизация и программирование задач логиче- ского управления. Известия РАН. Тео- рия и системы управления. 2000. № 6. С. 63–81. 11. Зюбин В. Е. Процесс-ориентирован- ное программирование: учеб. посо- бие. Новосибирск. Новосиб. гос. ун-т. 2011. С. 194. 12. Шелехов В. И. Разработка автоматных программ на базе определения требова- ний. ИСИ СО РАН. Новосибирск. Систем- ная информатика. 2014. № 4. C. 1–29. 13. Любченко В. С. К проблеме создания модели параллельных вычислений. Параллельные вычисления и задачи управления: труды третьей междуна- родной конференции. Москва. 2006. С. 1359–1374. 14. Harel D. et al. STATEMATE: A working environment for the development of complex reactive systems. IEEE Trans. Eng. 1990. № 4. P. 403–414. 15. Wagner F., Schmuki R., Wagner T., Wolstenholme P. Modeling software with finite state machines: a practical approach. Auerbach Publications. 2006. P. 390. 16. Samek M. Practical UML Statecharts in C/C++. Second Edition: Event-Driven Programming for Embedded Systems. Newnes. 2008. 17. Mery D., Singh N. K. Automatic code generation from Event-B models. In Proceedings of the Second Symposium on Information and Communication Technology. SoICT. ACM. 2011.