Американскому космическому агентству приходится решать весьма непростые задачи создания надежного программного обеспечения. Специалисты NASA, занимающиеся полетами в глубокий космос, преодолевают очевидный кризис в разработке программного обеспечения, опираясь на два дополняющих друг друга подхода. Один уделяет первостепенное внимание программной инженерии, а второй использует потенциал автоматической генерации и проверки корректности кода.

Космические корабли и научное оборудование, которое люди посылают на исследование Солнечной системы, подстерегают разнообразные опасности. Тем не менее, самая серьезная опасность, с которой может столкнуться космический зонд, орбитальный корабль или вездеход, как правило, оказывается и самой предсказуемой: наличие ошибок даже в самом тщательно протестированном программном обеспечении.

Когда эта статья отправлялась в печать, космические аппараты приближались к Марсу, и для ряда сложных программных систем наступало время их окончательной проверки. В дни, когда взгляды множества людей прикованы к Красной планете, некоторые аналитики вспомнят ошибки в программах, проявившиеся в 1999 году во время полетов Mars Polar Lander и Mars Climate Orbiter.

В то же самое время далеко за орбитой Марса космический корабль Cassini следует к месту своего свидания с Сатурном. Voyager, запущенный в 70-х годах, передал сигнал из области, где заканчивается влияние Солнца, и в силу вступают законы межзвездного пространства. Орбитальные обсерватории ведут наблюдения за Вселенной, а в Калифорнии в Лаборатории реактивного движения NASA (JPL), уже начат следующий проект стоимостью в миллиарды долларов. Проект Mars Science Laboratory, кульминация которого намечена на 2009 год, ставит своей целью высадку на Марс более крупного космического аппарата, который будет действовать в автономном режиме более года. Многие научные космические станции стоимостью в сотни миллионов долларов сейчас находятся в полете, на этапе разработки или проектирования.

Больше ставки — выше риск

Число космических проектов постоянно растет; расширяется и круг задач, которые они призваны решать. Затерянные в космосе лаборатории передают снимки других миров, измеряют уровень радиации, определяют параметры потоков частиц и полей в межпланетном пространстве, берут химические пробы, определяют характеристики планет и, в конечном итоге, дают ученым возможность проверить свои теории, получить ответы на старые вопросы и поставить новые.

NASA и другие космические агентства используют все более сложные и масштабные программные системы для решения все более серьезных научных задач. В силу своего назначения и из-за огромных расстояний от станций наземного управления (связь необходимо поддерживать на дистанциях, измеряемых десятками световых минут или даже световыми часами), космические аппараты требуют все большей автономности, что неминуемо увеличивает их сложность. Это многократно увеличивает риск обострения проблемы, которая старше, чем само выражение «программная инженерия». Речь идет о проблеме надежности программного обеспечения.

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

От наземного контроля к автономным системам

Традиционно управление полетом и его планирование осуществлялись на Земле, где люди формировали последовательность зависящих от времени команд, определявшую, что и когда должен делать космический аппарат. Этот подход оказался достаточно эффективным, однако с увеличением количества полетов расходы на операции наземного управления стали чрезмерными.

Ранее космические системы включали ограниченное число автономных программ, отвечающих, например, за контроль давления, защиту от сбоев, выход на орбиту, спуск и посадку. Эти программы тестировались в течение десятилетий и теперь реализованы в современных системах на аппаратном уровне. Однако новые требования и увеличение числа полетов заставили создать единую программу автономного управления космическими аппаратами, которую можно было бы использовать для разных полетов.

Традиционные системы управления в космических аппаратах включают в себя подсистему защиты от сбоев, которая ведет мониторинг и «оберегает аппарат, разворачивая его солнечные антенны к Солнцу, сообщая станции наземного управления о возможных отказах, отключая ненужные системы и ожидая команды с Земли. Хотя такие механизмы отказоустойчивости давно и хорошо себя зарекомендовали, управление кораблем в критические моменты (например, вывод на орбиту), безусловно, является одним из источников непоправимых ошибок.

Защита космического аппарата от небольших сбоев, не подвергающих его риску, и многочасовое ожидание инструкций значительно сокращают количество научных данных, которые можно было бы получить и отослать на Землю. В самом деле, при таком подходе исследовательский аппарат может пропустить незапланированные события, например, не зафиксирует пролет кометы.

Глубокий космос — весьма враждебная среда для физического оборудования, но для управления полетами условия здесь вполне благоприятны: на планирование некритических маневров отводится больше времени. В то же время, марсоходу требуется большая автономность для выполнения своей сложной миссии: иногда есть всего несколько секунд на то, чтобы предотвратить падение в трещину.

Именно задача автономного управления поставила перед NASA наиболее сложные вопросы в его текущих исследованиях. Впрочем, агентству приходится решать и более земные проблемы.

За качество программ

В течение всей своей карьеры, которая началась с разработки полупроводниковой начинки для миссии Mariner на Марс и Венеру в 60-х годах, Том Гевин, один из руководителей группы полетов JPL, сталкивается с ситуациями, когда программное обеспечение становится не только инструментом реализации программы полета, но и важным фактором риска и причиной серьезных потерь. Сегодня Гевин считает своей основной задачей совершенствование программных систем в JPL, дальнейшую интеграцию производства программного обеспечения с конструированием других систем, а также проведение исследований, приоритетом для которых является увеличение числа космических проектов.

В нынешней экспедиции на Марс вывод на орбиту, спуск и посадка управляются программным обеспечением.

Mars Exploration Rover — рисунок художника. (Собственность NASA)

«Люди наблюдают, как работает механическая система, как выпускаются парашюты, выстреливаются подушки безопасности, а сам аппарат подпрыгивает на поверхности. Но это система, управляемая программно, и большая часть риска проекта связана с тем, насколько надежным окажется данное программное обеспечение», — подчеркнул Гевин. На программное обеспечение расходуется большая часть бюджета проекта; огромные средства уходят на кодирование, независимую проверку и тестирование, которое продолжается по 24 часа в сутки, при том что сроки окончания этих тестов диктуются движением планет.

Если пропустить срок, определенный небесной механикой, то полеты придется отложить надолго, например, путешествие к Марсу — на 22 месяца, на Венеру — на 19 месяцев, а к Юпитеру — на 13. Однако за точное выполнение намеченного плана иногда приходится расплачиваться чем-то иным. Гевин, к примеру, отметил, что программное обеспечение для PathFinder, который успешно опустился на поверхность Марса в 1997 году, в массе своей осталось без документации.

Гевин, по его словам, только начинает предпринимать попытки внедрить среди разработчиков лаборатории дисциплину создания программного обеспечения. Программисты описали 40-летний опыт в трех книгах, куда вошли практические решения, найденные в процессе подготовки полетов, принципы проектирования и обеспечения безопасности космических аппаратов.

Сейчас лаборатория инвестирует 4 млн. долл. в год в реализацию инициативы, направленной на обеспечение качества программного обеспечения, призванную дать разработчикам возможность систематизировать и использовать набор «лучших» практических решений. Впрочем, Гевин считает, что данная инициатива будет успешной лишь в том случае, если разработчиков удастся убедить документировать свои практические решения.

Вперед, только вперед

Исследования, проводимые в лабораториях NASA, в том числе в JPL, направлены на обеспечение надежности программного обеспечения, которое будет использовано в последующих полетах. Уникальные проблемы глубокого космоса заставили руководство агентства увеличить объем средств, выделяемых на исследования, посвященные вопросу надежности программного обеспечения. Разработчики используют передовые технологии синтеза кода и проверки корректности программного обеспечения, которое служит для самых разных целей — от автономных программ на базе методов искусственного интеллекта до крупных программных систем с более традиционной функциональностью.

В 2003 году в NASA была образована Лаборатория надежного программного обеспечения, основателем которой стал известный специалист по проверке программ на базе моделей Джерард Хольцман. Ту же цель создания качественного программного обеспечения преследует и еще один проект, Mission Data System (MDS).

Mars Exploration Rover на сборочной линии космических аппаратов JPL. (Собственность NASA)

В 1998 году, после того, как за полгода было завершено шесть независимых проектов запусков космических аппаратов, руководство JPL осознало необходимость увеличения отдачи от программной инженерии и потребность в повторном использовании общего для всех программного обеспечения полетов. Тогда Роберт Расмуссен и предложил MDS как многоцелевую архитектурную платформу, способную унифицировать программную и системную инженерию на всех этапах — от разработки концепции полета, до подготовки и запуска космического аппарата [1].

Когда в NASA говорят о MDS, то могут иметь в виду архитектуру, концепцию, миллионы строк кода, составляющие сейчас эту систему, создание программного обеспечения для марсианской экспедиции, набор процессов разработки или соответствующие исследования. В любом случае, MDS предлагает общую для разных полетов платформу создания, тестирования и повторного использования программного обеспечения, которое будет работать на космических кораблях, спускаться на поверхность в исследовательских аппаратах и действовать здесь, на Земле. Это кардинальный отказ от установившейся практики, при которой в результате независимых, разноплановых процессов разработки создавались «одноразовые» программные системы индивидуально для каждого космического полета.

Конечно, далеко не все ресурсы NASA, выделенные на обеспечение надежной работы программ, задействованы в исследованиях Хольцмана и в проекте MDS. Тем не менее, эти два проекта демонстрируют диапазон подходов, принятых в NASA, с одной стороны, подчеркивая различия между предлагаемыми решениями, а с другой — способствуя более эффективному решению задачи обеспечения надежности в целом.

Человеческие ошибки

Главная идея, положенная в основу работы Хольцмана, состоит в том, что программирование — это вид человеческой деятельности, а людям свойственно ошибаться. Хольцман напомнил, что на каждые 1000 строк, вновь написанного и не снабженного комментариями кода, приходится около 50 ошибок; после тщательного тестирования их число сокращается до 10. Дополнительные меры позволяют довести число дефектов до одного (а для некоторых продуктов не удается добиться даже этого) на каждые 1000 строк кода, но при этом общее количество оставшихся ошибок в крупной системе по-прежнему велико.

Статистические показатели качества программ, созданных неопытными и квалифицированными программистами, в целом одинаковы.

«Опытный программист, как правило, делает столько же ошибок, — заметил Хольцман, — но они значительно сложнее, более скрыты и требуют более детального анализа. Если такой специалист делает ошибку, то обнаружить ее намного труднее».

Тестировщики — тоже люди, и потому следует признать, что процессы тестирования, как и программирования, по самой своей природе изобилуют ошибками. С точки зрения Хольцмана, из этого следует, что единственной альтернативой остаются методы автоматического тестирования. Не теряя оптимизма, Хольцман уверен, что ему удастся убедить своих коллег в достоинствах автоматических методов проверки на базе моделей как альтернативы традиционному подходу к тестированию программного обеспечения.

Такие методы, как проверка на базе моделей, статистический анализ и анализ времени исполнения, дают возможность тщательнее проверить программы, позволяя протестировать даже маловероятные сценарии развития событий. Традиционное тестирование — отнимающая значительное время операция; как правило, с приближением даты пуска ее начинают сокращать, как только можно. Подобное тестирование может выявить сценарии, при которых возникновение ошибок наиболее вероятно, однако оно никогда не позволит найти все ошибки. Более того, методы тестирования постоянно устаревают.

«Мы создаем системы более сложные, чем способны понять, и более сложные, чем способны проверить, — утверждает Хольцман. — Традиционные процессы тестирования, разработанные для детерминированных, последовательных сред, за последние три десятилетия практически не изменились. Кроме того, современные системы — многопоточные, что делает их недетерминированными: планирование процессов и потоков, которые по-разному перекрываются по времени при каждом выполнении, а события возникают в непредсказуемые моменты, и методы тестирования для этого просто не предназначены».

С другой стороны, по его словам, исследователи благодаря более совершенным алгоритмам и постоянно наращиваемым вычислительным ресурсам начинают решать ранее казавшиеся неразрешимыми проблемы анализа программ. По расчетам Хольцмана, небольшой автоматический тест, разработанный им в 1980 году, выполнялся на компьютере в течение семи дней, если при этом удавалось найти достаточно мощный для его запуска компьютер. В 2000 году, при наличии в тысячи раз большей памяти и мощного процессора, тот же самый тест мог быть выполнен за семь секунд. Сейчас для этого требуется две секунды, а еще через два года хватит одной.

В конце 70-х годов бытовало мнение, что формальные методы можно автоматизировать. К концу 80-х Хольцман разработал Spin, вероятно, самое известное и широко применяемое в мире средство проверки на базе моделей [2]. В конце 90-х он и его коллеги из Bell Labs впервые использовали Spin и соответствующую технологию для разработки реального продукта, когда проверяли программное обеспечение для коммутатора IP-телефонии.

Хотя фрагмент кода, который они проверяли, был относительно небольшим, всего 10 тыс. строк из примерно 25 миллионов, он составлял функциональную основу системы, и возможные ошибки в нем могли оказаться фатальными для взаимодействий между параллельными процессами. Это приложение подтвердило истинность нескольких утверждений, касающихся данного метода, в том числе и то, что можно извлекать модели из исходных текстов автоматически. «Тестовые примеры» для получения моделей из текстов на Си стали тем решением, на которое деньги были потрачены один раз, а теперь оно повторно используется во всем процессе разработки.

В JPL, воспользовавшись Spin для проверки корректности программного обеспечения, разработанного для проекта Cassini, пригласили Хольцмана в NASA. Буквально в течение нескольких недель после своего переезда в Калифорнию, он помог создать тестовые примеры для проверки кода уже запущенных аппаратов Mars Exploration Rover и искал способ сделать то же самое для Mars Science Laboratory. Теперь Хольцман работает над формированием группы теоретиков, разработчиков систем и «активистов», которые будут взаимодействовать с виртуальной группой из нескольких сотен человек, чтобы продемонстрировать работу этих методик.

Космическая проверка Spin

Сотрудники NASA, в том числе Клаус Хевелунд и Томас Прессбургер, стали первыми и весьма успешными экспериментаторами, работавшими со Spin, системой проверки на базе моделей. Они развили свою собственную технологию проверки корректности и тестирования, Java PathFinder 1, которая преобразует высокоуровневые исходные тексты программ в Promela, формальный язык Spin [3]. Впоследствии для Java PathFinder 2, Виллем Виссер вместе с Хевелундом создали новый модуль проверки на базе моделей, в котором виртуальная Java-машина интерпретирует исходные тексты [4]. Сейчас ведется работа по интеграции технологии проверки на базе моделей, реализованной в Java PathFinder 2, с Java PathExplorer, инструментарием мониторинга и анализа времени исполнения [5].

Эта работа началась с проекта Deep Space 1, послужившего своего рода тестовым полигоном для проверки технологии. В рамках полета в течение двух дней все управление космическим аппаратом было передано программному обеспечению Remote Agent. Хевелунд и Джон Пених в качестве эксперимента пропустили Plan Runner, критически важный для Remote Agent компонент кода, через Spin. Автоматическая проверка обнаружила пять ошибок — пять дефектов при работе с параллельными процессами, которые были устранены до полета.

Несмотря на эту проверку и 800 часов предполетного тестирования, Remote Agent попал в тупиковую ситуацию через шесть часов после своей активации. Группа разработчиков, организованная для анализа 12 тыс. строк на Lisp, составлявших текст системы, обнаружила ошибку через пять часов, причем эта ошибка была того же рода, что Хевелунд и Пених нашли ранее, и находилась в модуле, который был переработан уже после эксперимента по проверке корректности кода. Следует отметить, что группа приняла решение не исправлять эту ошибку, поскольку шансы на ее повторное возникновение были крайне малы. Ошибка больше не проявлялась (исправление дефекта могло с большой вероятностью привести к появлению новых проблем), показав, насколько редки такие ошибки, и почему их так трудно найти при традиционном тестировании.

Этот эпизод продемонстрировал, насколько велик потенциал проверки на базе моделей, и каковы ее ограничения.

«В частности, для параллельного программного обеспечения, где существует так много одновременных процессов, — заметил ведущий научный сотрудник Майкл Лоури, — проверка на базе моделей может оказаться лучше тестирования».

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

Есть и еще одна тенденция, которая подчеркивает трудности масштабирования средств проверки на базе моделей при работе с большими программами. Цифры, которые Лоури привел в качестве подтверждения этой тенденции, таковы: 30 тыс. строк кода были созданы в 80-х годах для полета Cassini; в 90-х годах программное обеспечение для проекта Mars PathFinder содержало 120 тыс. строк, а для Mars Exploration Rover оно выросло до 428 тыс. Некоторые считают, что программное обеспечение для Mars Science Laboratory будет содержать несколько миллионов строк.

Поиск других путей

Когда Хевелунд и Пених начали вручную преобразовывать код Deep Space 1 для проверки с помощью Spin, они могли анализировать в день около 30 строк. Автоматическое преобразование Java PathFinder позволило анализировать около 1500 строк кода в день, но увеличить это число не позволял объем доступной памяти. В тот момент, однако исследователи осознали основные ограничения Spin и Promela. Именно тогда Виссер и Хевелунд создали модуль проверки на базе моделей, который использует виртуальную Java-машину. По словам Виссера, этот модуль «мог анализировать все поведение, все пути внутри кода, поскольку мы управляли планированием, а потому могли запланировать все возможные параллельные процессы». На создание первой версии понадобилось всего три месяца, но еще четыре года ушло на совершенствование инструментария.

Самая крупная программа, которая была проанализирована с его помощью, содержит 8 тыс. строк. Это прототип программного обеспечения космического аппарата с шестью сложными потоками управления, преобразованный в Java из С++, на котором он был первоначально написан. Как и Spin, Java PathFinder должен был стать эффективнее просто за счет совершенствования аппаратного обеспечения и улучшений, предпринимаемых при автоматическом преобразовании. Сейчас Пених пишет транслятор из C++ в Java, чтобы Java PathFinder мог бы работать и с текстами на C++.

Исследователи ставят своей задачей повышение эффективности автоматизированного анализа программ и за счет реализации иного подхода. Если Java PathFinder ведет поиск в пространстве путей в коде, чтобы найти тот путь, в котором есть ошибка, то Java PathExplorer целиком предназначен для поиска ошибок в одном пути. Главное, как считает Хевелунд, — использование более мощной временной логики, которая «позволяет одновременно делать заключения в соответствии с логикой будущего и прошлого, делать заключения о настоящем и анализировать возможные значения».

Java PathExplorer один раз выполняет программу, записывая состояние системы во время исполнения. В дальнейшем, работая с этой записью, в которой зарегистрированы все представляющие интерес события, инструментарий использует один набор алгоритмов для точного анализа, позволяющего определить, есть или нет ошибки в данной конкретной последовательности. Другой набор алгоритмов помогает сделать вывод, могут ли другие возможные версии этой последовательности содержать ошибки.

Среди последних усовершенствований инструментария — улучшение временной логики и расширение возможностей с учетом более высоких скоростей передачи данных. Примером может стать ситуация, при которой одна цепочка обновляет координаты x и y за одну операцию, а другая цепочка читает их по очереди. Если первая цепочка может обновить обе координаты между операциями чтения x и y, вполне безобидная операция программы может привести к получению ошибочной пары координат.

Хевелунд и Виссер намерены использовать базовые технологии Java PathFinder и Java PathExplorer для автоматической генерации тестов.

Компоненты в контексте

В дополнение к работам, целью которых является расширение возможностей технологии проверки на базе моделей, Димитра Гьяннакопулу и Корина Пасареану обратились к решению задач модульной и композиционной проверки корректности. Их подход предусматривает декомпозицию анализа программы на анализ ее компонентов, корректность которых, возможно, установить намного проще, чем всей программы в целом, при этом гарантируя свойства реконструированного целого.

Mars Science Laboratory — рисунок художника. (Собственность NASA)

Опираясь на абстрактную модель поведения компонента и требуемые свойства, Гьяннакопулу и Пасареану разработали методики формулирования предположений, которые описывают контекст, в котором компонент будет обеспечивать необходимые свойства. Будучи сформирован, контекст проверяется на соответствие предположению с тем, чтобы гарантировать корректность целого.

«Мы разделяем поведение компонента на то поведение, которое контролируется контекстом, и то, которое им не контролируется, — пояснила Гьяннакопулу, — и, в результате, получаем сведения о том, как контролируемое поведение влияет на выполнение требуемых свойств».

Эти ученые разработали платформу для последовательного формулирования предположений, опираясь на использование алгоритмов обучения и проверку на базе моделей. Когда не ясно, каким должен быть контекст компонента, решение — циклическое повторение анализа времени исполнения — генерация на основе предположения программы мониторинга, оснащение программы датчиками, проверка среды на соответствие предположениям, сделанным во время разработки, и выполнение кода восстановления в том случае, если предположение нарушено.

Mars Science Laboratory — рисунок художника. (Собственность NASA)

Поскольку из-за отсутствия информации об архитектуре этот подход реализовался только на уровне модели, его расширили таким образом, чтобы он работал непосредственно на уровне программного обеспечения. Там, где нет моделей архитектуры системы, те же самые методы предполагается применить к коду — генерация предположений и выполнение «модульных заключений» применительно к исходным текстам. Сейчас это пока лишь теория, но у исследователи полны решимости заставить эту методику работать.

Динамика статического анализа

Исходные тексты — это, фактически, отправная точка для статического анализа, еще один вид инструментария, апробированный в NASA. Формально данный метод существенно отличается от проверки на базе моделей и порождает результат иного рода. По словам Джиллауме Брата, научного сотрудника лаборатории JPL, статический анализ позволяет проанализировать код на основе программной семантики, не создавая модель и не выполняя программу. Брат и его коллега, Эрнауд Венет, работая над совершенствованием методов статического анализа, подтвердили практический потенциал подобного инструментария в задачах создания кода программ, тестирования модулей и их интеграции.

Статический анализ мало помогает в случае параллельности, тупиков и передачи данных. В то же время, он может оказаться весьма эффективным в деле выявления ошибок в стиле программирования, таких как неинициализированные переменные и указатели, попытки обращения за границами массивов и некорректные арифметические операторы, т. е. тех моментов, которые могут привести к искажению данных или даже сбою системы во время ее работы. Подобные ошибки весьма распространены, но статический анализ позволяет их устранить.

По итогам такого анализа создается своего рода математическая голограмма вычисляемое приближение набора значений, возникающих динамически во время выполнения программы, — которую можно рассматривать под разными углами, уточняя детали. В итоге, анализ позволяет получить три вида результатов: ошибки, которые инструментарий однозначно идентифицировал как ошибки, код, который до определенной степени является корректным, и возможные проблемы (это могут быть действительные ошибки или что-либо еще, например, невыполняемый участком программы).

Задача состоит в том, чтобы в каждой точке программы определить некоторый числовой инвариант. Анализ должен помочь сделать предположение, какое значение он может принимать при любом выполнении программы. Каждой отдельной конкретной операции в программе, сопоставляется абстрактная операция, выполняющаяся не над числами, а над интервалами.

Брат и Венет начали реализацию своего проекта с применения инструментария статического анализа PolySpace к реальному программному коду с Deep Space 1 и Mars PathFinder. Этот инструментарий оказался достаточно эффективным для того, чтобы установить базовые параметры для масштабирования и точности, т. е. соотношение точных классификаций ошибок и предупреждений о возможных проблемах в коде. Затем они создали специализированный инструментарий, адаптированный к программному обеспечению NASA в том виде, как они себе его представляли. Затем началось тестирование их нового инструментария, C Global Surveyor, на программном обеспечении запуска, вывода на орбиту, спуска и посадки для Mars Exploration Rover. Они начали искать способы, с помощью которых разработчики MDS могли бы получить эффект от автоматической проверки, согласившись на определенные ограничения в методах программирования на C++.

Рожденный инженером

Кирк Рейхольц, один из основных партнеров Хольцмана и других апологетов автоматизированных подходов, является страстным пропагандистом совершенно иной точки зрения. Рейнхольц занимает пост главного программиста в проекте Mars Science Laboratory.

Рассказывая о том, как его группа создает код для Mission Data System, содержащий более миллиона строк, Рейнхольц продемонстрировал твердую веру в мастерство людей, здравый смысл и процессы: «Цель этой работы, по существу, заключается в том, чтобы превратить все, что мы изучили за несколько десятилетий создания встроенного, чрезвычайно надежного программного обеспечения, в большей степени в инженерную дисциплину, нежели в искусство».

По словам Рейнхольца, гениальность MDS заключается в том, что этот подход переносит вопросы (которые, как показывает опыт, в условиях реальных проектов могут обернуться серьезными проблемами) на архитектурный уровень, где есть достаточно совершенные процессы, за которыми можно наблюдать, причем, изучая их с разной степенью детализации, выполнять проверку корректности и так далее: «То, что современный программный инженер может стремиться скрыть, MDS делает явным».

Задача MDS — сделать так, чтобы программистам было проще выбирать правильные решения и сложнее совершать ошибки.

Подходы, которые олицетворяют MDS и проверка на базе моделей (одни — в большей степени полагающиеся на опыт и изобретательность, другие — в большей степени опасающиеся склонности людей к ошибкам), предлагают решения, способные стать залогом успеха Mars Science Laboratory и других проектов.

Проектирование систем следующего поколения

Традиционные методы проектирования, в том числе и те, которые использовались в JPL ранее, предусматривают декомпозицию системы на подсистемы, для каждой из которых группа разработчиков предлагает свои собственные адаптированные решения и итеративно интегрирует их на системном уровне.

Хотя декомпозиция подсистем прекрасно работает в случае хорошо известных предметных областей, таких как корпоративные системы, она не всегда себя оправдывает в такой среде, как глубокий космос, где системные ресурсы, например, энергия или память, ограничены, и система должна взаимодействовать с непредсказуемой физической средой [1, 5]. Эти разнообразные подсистемы должны совместно использовать ограниченные ресурсы, но предположение, из которого исходила группа проектировщиков одной подсистемы, может оказаться неверным для всех подсистем в целом. В итоге, как отметил ассистент архитектора MDS Дэниэл Дворак, использование объектно-ориентированных методологий в такой среде приводит к иерархической декомпозиции подсистем, которые трудно проверить, протестировать или повторно использовать.

Опираясь на свой богатый опыт работы с предыдущими проектами JPL, Роберт Расмуссен отказался в MDS от абстрактной архитектуры при проектировании следующего поколения систем для полетов в глубокий космос. Такие системы взаимодействуют с физическим миром, реагируют на него и пытаются контролировать физическое состояние, а те, кто управляет полетом с Земли, мыслят в аналогичных терминах. В итоге, Расмуссен предложил архитектуру управления на базе состояний, которая моделирует взаимодействия между физическими состояниями и пытается управлять состоянием с учетом целей и ограничений, а не используя зависящую от времени последовательность команд, т. е. такой подход позволяет варьировать степень автономности полета.

В отличие от традиционной объектно-ориентированной декомпозиции подсистем, которые скрывают или инкапсулируют системные взаимодействия в локальных переменных программы, флагах, счетчиках, указателях или условных выражениях, MDS поднимает переменные состояния на вершину архитектурной иерархии, т. е. туда, где их можно увидеть, понять и формировать [1, 6]. В итоге, системный инжиниринг становится анализом состояний с точным и ограниченным словарем для описания всех взаимодействий между элементами, из которых состоит проект. Этот словарь включает в себя такие термины, как переменные состояния, оценочные функции, контроллеры, журналы регистрации значений состояния, модели результатов действия состояний, параметры, ограничения на время и состояние, ресурсы, команды, фрагменты сценариев и цели.

Не менее важно и то, что такой ограниченный словарь отображается на предметную область программной инженерии, устанавливая строго определенные значения входных и выходных величин, тем самым, либо ограничивая возможности системного разработчика, либо помогая ему при реализации данной части системы, либо программист вносит ненужную сложность или потенциальную ошибку, либо первоначальный анализ системы был ошибочен. Более того, все аппаратные компоненты, их атрибуты и смоделированные преобразования между ними могут быть помещены в базу данных состояний и к ним обращаются с запросами специалисты по планированию полета и системные инженеры, разработчики программ и их автоматизированные инструментальные средства, симуляторы, тестирующие программное обеспечение на соответствие отсутствующему аппаратному обеспечению, и, возможно, еще важнее, бортовые программы в случае непредвиденного поведения системы.

Охватывая всю дисциплину инжиниринга и обеспечивая ее соблюдение сверху вниз, MDS использует общий словарь на основе анализа состояний с учетом имеющихся требований. Он применяет этот словарь к циклу разработки программного обеспечения, сверху вниз, вплоть до уровня управления конфигурацией, в то же время оставляя возможности для реализации новых технических подходов.

MDS объединяет системную архитектуру на базе состояний и компонентную программную архитектуру для того, чтобы предоставить специфическую для предметной области платформу для семейства приложений, будь то несколько поколений спутников, спускаемых модулей или космических аппаратов, или платформ, сопровождающих их полет, спуск, посадку и тестирование [1]. Архитектура на базе состояний предлагает структурированный процесс для строгого анализа, в котором особое значение придается проектированию на базе моделей для оценки и управления, делает взаимодействия ясными и предупреждает ненужные сложности. Компонентная архитектура предлагает платформы и руководства по настройке, повторно используемые строительные блоки в объектно-ориентированном проектировании, руководство по адаптации его для конкретных задач и примеры использования платформ.

Программное обеспечение обслуживания полетов, как правило, встроенное, в то время как наземное программное обеспечение опирается на огромные ресурсы (серверы, адекватное энергоснабжение и т.д.). Но будь то одна миллисекунда или один день, цикл управления, и с архитектурной, и с пользовательской точек зрения, должен учитывать эту задержка связи. Например, специалисты управления полетом видят космический корабль как точку на двухмерной схеме, в то время как сам корабль — это объект в трехмерном пространстве. В итоге возникает вопрос, на что указывает эта точка?

Обе точки зрения используют одни и те же математические уравнения, но получают разные результаты, поскольку оперируют с разными степенями свободы. С другой стороны, поскольку MDS касается именно сходных черт, а не различий, разработчики могут использовать одну и ту же математическую и архитектурную платформу для создания ПО управления полетом и наземного контроля. В отличие от предыдущих проектов, в JPL решено объединить полетное и наземное программное обеспечение для Mars Science Laboratory.

Анализ состояний

Анализ состояний, в том виде, как он реализован в MDS, — это единый, методический и строгий подход к выявлению, описанию, представлению и документированию состояний системы, а также к моделированию их поведения и взаимосвязей между ними. Знания о системе и ее среде со временем находят отражение в переменных состояния, которые включают в себя:

  • динамику — положение и пространственные координаты летательного аппарата, углы наклона и поворота;
  • среду — уровень освещенности, атмосферные профили, рельеф;
  • статус устройства — конфигурация, температура, режимы работы, режимы сбоев;
  • параметры — свойства массы, масштабные коэффициенты, погрешности, смещения, уровень шума;
  • ресурсы — мощность и энергия, топливо, память, полоса пропускания;
  • наборы данных — научная информация, наборы параметров;
  • управление данными и правила передачи — сжатие, удаление, приоритеты передачи;
  • внешне управляемые факторы — расписание сеансов и конфигурирование каналов космической связи.

MDS сообщает, хранит и передает информацию о системе в виде записей данных о состоянии, параметрах и командах.

Системные инженеры используют анализ состояний для интеграции целей полета в детальные сценарии, слежения за системными ограничениями и правилами работы, описания методов, которые они будут использовать для достижения поставленных целей, и записи информации об аппаратных интерфейсах и работе. В целом, элементы единого словаря объединяют все аспекты процесса проектирования. Например, если цель заключается в том, чтобы исследовательский аппарат взобрался на скалу, переменной состояния, которой необходимо управлять, будет позиция аппарата относительно скалы. Измерения подтверждают данное состояние, например, поворот колес, данные датчика солнца или показания стереокамеры. Что касается стереокамеры, то модели измерений показывают расстояние до элементов рельефа, уровень освещенности, уровень питания камеры («включена/выключена»), состояние камеры и так далее.

На рис. 1 показана ориентированная на цели архитектура MDS на базе состояний. Опираясь на модель, описывающую механизм работы, модули оценки находят «хорошие» объяснения данным измерений (датчик) и команд (активатор) для оценки состояния. Переменные состояния содержат значения состояний, в том числе степень неопределенности. Чтобы описать развитие состояния графики состояний объединяют текущие и прошлые оценки с прогнозами и планами на будущее. Вся вместе, синхронизованная по времени информация о состоянии и модели поведения состояния предоставляет данные, необходимые для работы системы и оценки производительности [1].

Операторы выражают свое намерение в виде целей, декларируя, что именно должно произойти, а не как. Операторы и планировщики могут ставить цели рекурсивно, даже условно, в виде целей более низкого уровня, которые координируются контроллером/планировщиком, использующим приоритет как решающий аргумент при разрешении конфликтов. MDS хранит оценки состояний, а контроль состояния полностью отделен для того, чтобы избежать искушения сфальсифицировать оценки состояния, «подогнав» их к поставленной цели, или риска по-разному интерпретировать одни и те же данные.

Наконец, MDS представляет фактические аппаратные компоненты в программном обеспечении в виде аппаратных адаптеров, которые способствуют описанию модели абстрактной системы (в том числе времени) за счет преобразования необработанных данных ввода/вывода, а также моделей измерений и команд в абстрактные декларации о состоянии. Кроме того, аппаратные адаптеры на базе программного обеспечения могут выявлять системную аппаратуру с дополнительным поведением, таким как отбор образцов, ввод/вывод, программирование и синхронизация, разметка времени и метаданных, буферизация и маршрутизация данных, преобразование форматов данных, проверка ошибок, а также обработка и сжатие данных. И самое важное заключается в том, что MDS изолирует оболочки состояний от специфических для платформ интерфейсов и поддерживает реальное, имитируемое или абстрактное аппаратное обеспечение в реальном или виртуальном времени.

Миссия возможна?

Оценка состояния объекта и управление состоянием через цели, которые ограничивают его поведение на протяжении долгого времени, будут гарантировать выполнение миссии, возложенной на MDS. Поскольку MDS создает и состояние, и модели, которые ее точно описывают, цели по своей природе являются самоконтролируемыми, предписывая возможные входные и выходные данные. Цели также обеспечивают «опорные точки» для модулей проверки, датчики в коде и инструментальные средства проверки и контроля, что способствует увеличению надежности.

Более интригующая возможность, предлагаемая Роукье, предполагает использование автоматической генерации кода для самого разного системного программного обеспечения космических кораблей. Роукье рассматривает существующие методы проверки на базе моделей как наиболее подходящие для конкретных проблем, алгоритмов и тщательно отобранных фрагментов кода, где разработчики знают, чего они ищут — не абстрактные разделы кода из крупномасштабных систем, в которых сложность возникает из-за взаимодействий между различными частями. Вместо этого Роукье делает ставку на методики генерации кода и преобразования уже успешно использованные в проекте Deep Space 1.

Роукьет применял инструментарий Stateflow компании MathWorks и некоторые созданные в его лаборатории средства для генерации 90% кода подсистемы защиты от сбоев в проекте Deep Space 1 на основе 60 или около того состояний машин. Поскольку на создание таких моделей может потребоваться несколько месяцев и их можно пересматривать 50 и более раз, автоматическая генерация эффективного и небольшого по размеру кода на языке Си стала огромной победой, позволяющей талантливым инженерам создавать системы на основе модели, как при обычном строительстве, а не ждать, пока программисты напишут код, проверят его и — почти наверняка — еще раз перепишут конкретную систему. Однако этот подход решает только часть проблемы.

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

С помощью своих моделей на основе состояний MDS предлагает более формальное выражение корректных входных и выходных данных. Использование более интеллектуальных языков с более высокими уровнями абстракции будет поддерживать проверку на базе моделей и сделает возможным применение современной технологии и алгоритмов компиляторов, таких как поиск шаблонов, распознавание дерева и алгебраический формализм для операций на деревьях для самих генераторов кода.

Общая цель Роукьетта заключается в том, чтобы сгенерировать 95% кода для Mars Science Laboratory автоматически, оставляя лишь небольшой рабочий цикл, который будет кодироваться вручную и потребует интенсивной проверки на базе моделей и тестирования. Космос — это весьма малоизученная среда, как заметил Роукье, и единственный способ гарантировать успех полета — привлекать как можно больше талантливых людей и использовать их знания, воображение и время для создания систем, а не для написания кода.

«В ходе анализа скал на Марсе наши надежды сделать серьезные открытия тают, и существует множество других прекрасных мест, куда можно отправиться. Но мы должны сделать такого рода вещи максимально дешевыми и надежными», — подчеркнул он.

Используя новые технологии и подходы для разработки максимально надежного программного обеспечения в рамках жестких ограничений, NASA имеет шанс предложить нечто большее, чем результаты работы запускаемых ею научных станций.

Какого бы прогресса космическое агентство не добилось, решая свои собственные программные проблемы, по-видимому, ему удастся существенно изменить общее положение дел в этой области, развивая как саму компьютерную науку, так и программную инжененрию. Кроме того, любой успешный побочный продукт, который позволит увеличить надежность, и при этом сократить время и стоимость разработки, способен, в принципе, обеспечить экономию, сравнимую с национальным бюджетом, выделяемым на исследование космического пространства.

Литература
  1. D. Dvorak et al., «Software Architecture Themes in JPL?s Mission Data System», Proc. AIAA Space Technology Conf. and Exposition, 1999.
  2. G. Holzmann, The Spin Model Checker: Primer and Reference Manual, Addison-Wesley, 2003.
  3. K. Havelund, T. Pressburger, «Model Checking Java Programs Using Java PathFinder», Int?l J. Software Tools for Technology Transfer, vol. 2, no. 4, 2000.
  4. W. Visser et al., «Model Checking Programs», J. Automated Software Engineering, vol. 10, 2002.
  5. K. Havelund, G. Rosu, «Monitoring Java Programs with Java PathExplorer», Proc. Workshop Runtime Verification, Electronic Notes in Theoretical Computer Science, vol. 55, no. 2, 2001.
  6. D. Dvorak, «Challenging Encapsulation in the Design of High-Risk Control Systems», Conf. Object-Oriented Programming, Systems, Languages, and Applications, Seattle, 2002.

Патрик Риган (patrick.regan@ieee.org) — ведущий корреспондент по вопросам науки и технологии сети некоммерческого телевидения и радио NJN News. Скотт Хемилтон (s.hamilton@computer.org) — старший редактор отдела информации журнала Computer.


Patrik Regan, Scott Hamilton, NASA?s Mission Reliable. IEEE Computer, January 2004. IEEE Computer Society, 2004, All rights reserved. Reprinted with permission.