Max Home IndustryВас могут использовать для частой перезагрузки сервера, чтобы убедиться, что он не выйдет из строя из-за проблем с ресурсами, но как насчет современного реактивного авиалайнера, такого как Boeing 787?
Неизбежное проникновение программного обеспечения в инженерное дело несет с собой проблему ошибок. Инженеры по встраиваемым компьютерным системам имеют долгую историю попыток найти способы сделать программное обеспечение доказуемо правильным. Языки, используемые для управления процессами, как правило, однозадачны, как и их операционные системы, и обычно проводится множество проверок оборудования, чтобы убедиться, что ничего серьезного не может пойти не так.
Это делает недавнее распоряжение Федерального управления гражданской авиации США еще более шокирующим.
В основном это говорит о том, что все Boeing 787 Dreamliners необходимо отключать каждые 248 дней. Если они не будут сброшены, блоки GCU блоков управления генератором перейдут в отказоустойчивый режим, и самолет потеряет всю электрическую мощность.
Почему именно?
Процитируем директиву FAA:
Это состояние вызвано внутренним программным счетчиком GCU, который переполняется через 248 дней непрерывного питания. Мы выпускаем это объявление, чтобы предотвратить потерю всей электроэнергии переменного тока, которая может привести к потере управления самолетом.
Простое предположение предполагает, что проблема заключается в 32-битном переполнении со знаком, поскольку 231 — это количество секунд в 248 днях, умноженное на 100, то есть счетчик в сотых долях секунды.
Итак, проблема заключается в простом классическом переполнении. Вы могли бы подумать, что это то, что можно было бы обнаружить формальными методами, но подумайте на мгновение, как вы собираетесь реализовать такой счетчик?
Вы можете увеличить количество используемых битов, что откладывает переполнение, или вы можете работать с арифметикой с бесконечной точностью, которая будет медленно использовать доступную память и, наконец, вывести систему из строя.
Возможно, новая система обнаружения переполнения от MIT, см. MIT обнаруживает ошибки переполнения, указала бы на это, и тогда программисты могли бы реализовать тест и процедуру безопасного сброса часов, что является лучшим, на что можно надеяться.
Пока не будет исправления проблемы, все Dreamliners необходимо перезагрузить до истечения 248-дневного периода. По-видимому, если произойдет худшее, и ГПА переполнятся и отключат питание, тогда у самолета должно быть достаточно резервного питания от литий-ионной батареи примерно на 6 секунд, пока набирающая воздушная турбина развертывается для аварийной выработки электроэнергии. Так что, если повезет, это не ошибка, из-за которой самолеты могут падать с неба.
Один интересный факт заключается в том, что FAA утверждает, что перезагрузка GCU займет около часа, поэтому кнопки сброса явно нет.
Невозможно исправить Dreamliner.
Больше мультяшных забав на xkcd, веб-комиксе о романтике, сарказме, математике и языке
Подсчитано, что Airbus A380, сравнимый по сложности с Dreamliner, имеет более 100 миллионов строк кода.