PROBABILISTIC TIMED AUTOMATA ANALYSIS OF AIR TRAFFIC CONTROL SYSTEMS

Аннотация

В исследовательском проекте объединяются разработка интеллектуальной системы управления воздушным движением и строгая математическая оценка интерфейсов координации управляющих действий между пилотами и диспетчерами. Интерфейс «диспетчер–пилот» должен иметь формальные спецификации так же, как и программное обеспечение систем управления полётом, поскольку он представляет собой единый реактивный комплекс. Каждое взаимодействие в системе моделируется с помощью вероятностного автоматa с временными ограничениями, что отражает как реальные эксплуатационные ограничения, так и случайное возникновение ошибок оператора и сбоев оборудования. Язык формальных спецификаций Z позволяет формировать контракты, связывающие наблюдаемые внешние действия с их необходимыми предусловиями и постусловиями, которые могут проверяться как человеком, так и машиной. Модули интерфейса, представляющие операторов, графические дисплеи, внутреннюю авионику и надзорных агентов безопасности, соединяются для выполнения слабой ветвящейся бисимуляции, которая доказывает поведенческую эквивалентность при наличии временной неопределённости.

Модель показывает, что команды диспетчера, обратная связь от машины, надзорные вето и подтверждения пилота могут быть представлены двадцатью глобальными состояниями в модели, охватывающей все значимые временные и отказные сценарии. Автоматизированная система верификации фиксирует низкую вероятность успешного завершения миссии, а также ошибки оператора, повышающие общий риск, и выявляет критические временные дивергентные пути выполнения, обнаруживающие скрытые уязвимости проектирования. Инженеры интерфейсов могут изменять временные условия, пересматривать визуальные подсказки и внедрять адаптации к когнитивной нагрузке без нарушения существующих формальных доказательств, поскольку графический дисплей и скрытая логика были доказаны эквивалентными. Данное исследование трансформирует интерфейс «диспетчер–пилот» в компонент экосистемы управления воздушным движением, получающий математическую сертификацию и закладывающий основу для будущих интерфейсов, адаптирующихся к данным о рабочей нагрузке при сохранении гарантий безопасности, проверяемых машинами.