По ссылке Владимира Ивановича Шелехова
Цитата:
6. ОБЗОР РАБОТ
Современный пассажирский лифт [16] является сложным техническим сооружением.
Программа управления работой лифта нетривиальна. Ее нередко используют для демонстрации технологии программирования.
Примеры программ управления лифтом можно найти в работах [25, 12-15]. В книге Д. Кнута представлена нетривиальная реализация в форме сопрограмм [14]. В книге Х. Гома иллюстрируются различные виды диаграмм UML [25].
Автоматные методы программирования в сочетании с технологией объектно-ориентированного программирования представлены в работах [12, 13].
В руководстве [15] определяется серия из пяти последовательно уточняемых моделей лифта в технологии Event-B. Предложенная авторами программа управления лифтом существенно проще и короче программ в упомянутых выше работах.
Есть три составляющие, обеспечивающие простоту нашей программы Lift: гиперграфовая композиция в сочетании с механизмом гиперфункций, объектная ориентированность и реализация примитивов вне автоматной программы на языке P.
Формальный метод моделирования и анализа реактивных систем Event-B [17] определяет процесс построения серии моделей исходя из содержательного описания требований к реактивной системе.
Каждая очередная модель является детализацией (refinement) предыдущей модели. Корректность моделей и согласованность моделей различных уровней обеспечивается проведением математических доказательств истинности инвариантов.
Следует отметить неадекватность терминологии. Событие (event) в Event-B включает действия, реализующие реакцию на событие, т.е. сопоставимо с требованием в предлагаемом нами подходе.
По нашему мнению нет никаких оснований называть аксиомами ограничения на значения входных переменных модели.
Система управления лифтом рассматривается в руководстве [15] в качестве примера использования технологии Event-B.
Определяется пять уровней:
лифт без дверей и кнопок;
добавление дверей лифта;
добавление дверей на этажах;
добавление кнопок в лифте;
добавление кнопок на этажах, по одной кнопке на этаж.
На пятом уровне используется 17 событий и 8 переменных: номер текущего этажа,
статус лифта (moving, stopped, idle),
направление движения (up, down),
статус дверей лифта (closed, opening, open, closing),
статус дверей на этажах, массив кнопок лифта,
подмножество нажатых кнопок,
массив кнопок на этажах.
В нашей программе используется 10 требований, две переменных (dir и floor) и три массива кнопок.
Определяя более сложную функциональность, наша программа существенно проще.
Переменные, определяющие статусы лифта и дверей, у нас не нужны, поскольку все действия с дверями локализованы в подпрограмме atFloor, работающей при остановленном лифте и
завершающей работу с гарантией закрытия дверей.
Подпрограмма atFloor появилась в результате гиперграфовой декомпозиции программы Lift, что обеспечивает ее простоту.
Уже модель первого уровня (без дверей и кнопок) в [15] оказалась значительно сложнее нашей реализации. Полная коллекция из пяти уровней является громоздкой.
Технология Event-B [17] декларирует возможность экстракции исполняемой программы из коллекции моделей.
Даже если это возможно, польза от такой программы сомнительна.
Отметим, что в нашем подходе автоматная программа может быть оттранслирована в эффективную программу на язык С++.
Язык интервальной темпоральной логики, разработанный Джоном Рушби для верификации систем реального времени, демонстрировался для спецификации системы управления лифтом [27].
Спецификация в виде 31 темпоральной формулы достаточно сложна; она намного сложнее представленной в данной работе.
Работа [27] по интервальной логике не имела продолжений 1, поскольку появились более предпочтительные подходы к спецификации, например, диаграммы use case.
Разрабатываемая технология предикатного программирования до недавнего времени не имела в мире близких аналогов.
Впервые появился язык, похожий на язык предикатного программирования P.
Функциональный язык доказательного программирования Smart разработан французской компанией Prove&Run 2.
Корректность программ, а также отсутствие уязвимостей обеспечиваются дедуктивной верификацией.
Язык Smart содержит конструкции, аналогичные гиперфункциям. Программа может быть оттранслирована на языки C и Java.
Полное описание языка недоступно. Некоторые особенности языка Smart изложены в работах [18, 19].
В событийно-ориентированной парадигме [20, 21] программа представлена в виде цикла, в котором последовательно просматривается определенный набор событий (сообщений).
Для всякого события запускается соответствующий обработчик события.
Таким образом, программа составляется из набора независимых обработчиков.
В частности, графический интерфейс пользователя (GUI), во всех инструментах его реализующих, определяется именно в такой архитектуре.
Авторы данной парадигмы признают, что программирование в ней является сложным. Причина сложности в том, что в обработчике события неестественным образом перемешиваются части программ, которые в автоматной программе принадлежат сегментам кода для разных управляющих состояний.
Событийно-ориентированный стиль программирования иногда применяется во избежание параллелизма в программе, нередко используя при этом сопрограммную схему взаимодействия.
Отметим, что замена параллельного исполнения сопрограммным является преобразованием, существенно усложняющим программу; см. например [22].
Событийно-ориентированное программирование должно быть ограничено первичной обработкой событий (сообщений) для последующей передачи их автоматной программе, исполняемой параллельно.
В частности, графические интерфейсы пользователя должны быть ориентированы лишь для построения разнообразного гибкого внешнего окружения автоматной программы, но не ее самой.
Обзор работ по автоматному программированию представлен также в статьях [1, 11, 23].