DRAKON.SU

В 2015г. начался новый этап реформы в космической отрасли. Образована государственная корпорация "РОСКОСМОС". Руководителем назначен Игорь Комаров. Началась рутинная работа по реорганизации отрасли, включающей около 200 различных предприятий: http://www.federalspace.ru/275/. Генеральной стратегией объявлена интеграция предприятий: неэффективно реализуемые функции, дублированные на разных предприятиях, передаются в ведение вновь образуемым предприятиям. Например, принято решении о едином предприятии по разработке двигателей космических аппаратов (КА) в интересах каждого из шести центров разработки КА.

Следует надеяться, что реформа Роскосмоса затронет также область разработки управляющих программ для КА -- то, что принято называть бортовым программированием. Увы, эта часть работ финансируется у нас по остаточному принципу. Для большинства руководителей космической отрасли бортовая программа -- это специальная железка, которая вставляется в КА; они не делают различия программ с другим оборудованием в КА. Да, они знают, что есть специальные люди с большим гонором -- программисты, которые эти программы делают. Но не более того. Возможно, кому-то такая картина покажется чересчур утрированной. Но есть еще факты в которые трудно поверить: до сих пор применяется ассемблерное программирование. И похоже, лишь АО "Информационные спутниковые системы" избежали такой участи. Для справки: ассемблерное программирование применялось в 1960-1970-ых гг. и почти всюду исчезло в 1980-ых.

Между тем, в космическом агентстве NASA очень значительная (если не большая) часть функциональности КА реализуется программно, а не аппаратно. А что у нас?

На начальном этапе обсуждения будет правильным уточнить и дополнить исходную картину бортового программирования в нашей космической отрасли.
Большая просьба ко всем, кто обладает такой информацией, поделиться ею на нашем Форуме.
После этого можно будет переходить к обсуждению различных вариантов решения проблем бортового программирования.
Некоторые предварительные идеи были озвучены в сообщении: http://forum.oberoncore.ru/viewtopic.php?f=62&t=5503&start=20#p93732.

Так понимаю, что генеральной стратегией объявлено "хранить яйца в одной корзине", ради углубления эффективности, конечно.

Ну, не все столь ужасно.

По моим сведениям, весьма продвинутая технология программирования (им даже удалось сократить численность отдела "бортовых" программистов с 30 до четырех человек) применяется в МОКБ "Марс".
Как и в случае ГРАФИТ/ФЛОКС Паронджанова в НПЦ АП имени Пилюгина, она ориентирована на визуальное представление алгоритмов.
Кстати, в НПЦ АП помимо ГРАФИТ/ФЛОКС, применяются и другие проблемно-ориентированные языки. Например, язык "У" для баллистических расчетов.

В НПОА, г. Екатеринбург, по слухам, использовали даже язык Ада, в основном - Си, причем есть собственная среда разработки RocketSite.

В РКК "Энергия" имени С.П. Королева неплохая развитая технология, они выпустили по ней уже не одну книгу.

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

Была кстати тема на форуме НК На чем пишется софт для КА?

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

Наверное, это лучшее учебное пособие по технологии бортового программирования, в котором архитектура бортовых комплексов управления и методы их конструирования тщательно проработаны и в доступном виде изложены для студентов. Технология бортового программирования базируется на общей технологии программирования, представленной в оглавлении учебного пособия следующими двумя подразделами:
2.2. Методология модульного проектирования архитектуры программного обеспечения бортовых комплексов управления ... 123
2.3. Методология структурного проектирования компонентов программного обеспечения бортовых комплексов управления ... 133
Отметим, что эта часть учебного пособия не претерпела существенных изменений по сравнению с более ранними версиями начиная с 2003г.

Методы модульной и структурной декомпозиции программ -- это уровень технологии начала 1980-ых годов. Тогда на смену модульной пришла объектно-ориентированная технология, позволяющая спрятать внутри классов часть структур данных и связей между ними, тем самым существенно упрощая основную программу. Отметим, что объектно-ориентированная методология применима и для разработки программ на языках типа Модула-2 или Си.

Технологический базис космической отрасли -- это набор технологий, используемых в отрасли и являющихся внешними по отношению к ней в отличии от технологий, разрабатываемых внутри отрасли. Технологический базис -- это основа, на которой строится технологическая платформа отрасли, например, такая как НИСС. Общая технология программирования входит в технологический базис, но не только она. Далее рассмотрим часть технологического базиса, связанного с бортовым программированием.

Имеются три индустрии:
1. Software engineering -- Программная инженерия
2. Requirements engineering -- Инженерия требований
3. Systems engineering -- Системная инженерия -- Системотехника в СССР

Технология программирования часто используется как эквивалент программной инженерии, хотя содержание этих понятий не совпадает. Частью программной инженерии являются формальные методы (Formal methods). Они базируются на формальной спецификации программ. Формальные методы включают:

- тестирование на базе формальной спецификации;
- статическую верификацию (software model checking);
- проверку на моделях (model checking);
- дедуктивную верификацию;
- программный синтез.

Требования — совокупность утверждений относительно свойств разрабатываемой системы. В качестве системы может быть КА или бортовая программа. Инженерия требований применяется как в программной, так и в системной инженерии. Языки и методы инженерии требований, применяемые в космической отрасли, должны быть едиными для КА и бортовых программ. Существуют разные виды требований. В первую очередь, это функциональные требования, определяющие поведение системы. Другой пример -- требования безопасности.

Формальные методы и инженерия требований появились около 40 лет назад. Поскольку они важны для космической отрасли, я собираюсь дать их краткое популярное изложение в рамках рубрики "Космическое программирование" в отдельных темах, чтобы не загромождать основную линию ведения дискуссии. Очень желательно, чтобы кто-нибудь дал популярное изложение системной инженерии.

Вопрос: чем технологический базис нашей космической отрасли отличается от уровня 1980 года?
Отличается. Появились графические языки программирования: Дракон в НПЦ АП и язык блок-схем в МОКБ «Марс». В 1980 году еще не было графических интерфейсов пользователя.

А чем еще ???

То, что у нас в этом плане не все хорошо, проливает свет сообщение форума: http://forum.oberoncore.ru/viewtopic.php?f=140&t=5351#p90975.

Чтобы оценить состояние нашей космической отрасли в части бортового программирования, полезно познакомиться с опытом NASA и стран Европы.

Бортовое программирование у них

Одним из знаковых достижений NASA за последние годы является доставка на поверхность Марса в 2012г. и эксплуатация марсохода третьего поколения (научной лаборатории) Curiosity. Размер бортовой программы марсохода -- 3.8 млн. строк кода на языке C. Программа разрабатывалась в течении пяти лет командой из 40 высококлассных программистов.

Высокая надежность программы марсохода достигнута применением трех классов методов:

методов безопасного программирования на базе JPL Institutional Coding Standard for the C Programming Language. Version 1.0, 2009;

современных методов экспертизы кода;

формальных методов, в особенности, методов проверки на моделях (model checking).

Данные методы поддерживались набором разнообразных эффективных инструментов. Методы представлены в докладе Джерарда Хольцмана на семинаре HotDep'12, а также описаны в его статье: Gerard J. Holtzman. Mars code. 2012.

Чтобы получить представление о современных методах и инструментах верификации программ, полезно прослушать 9-ю Ершовскую лекцию, прочитанную 19 апреля Александром Петренко, синхронно с просмотром слайдов лекции.

Формальные методы -- это область, в которой наше отставание катастрофическое: NASA уже 20 лет применяет формальные методы, а у нас мало специалистов по формальным методам и некому учить.

Написаны сотни статей по применению формальных методов в аэрокосмической отрасли. Авторы из разных стран, даже из Китая; из России -- никого. Вот несколько статей:

1. Formal modelling and quantitative analysis of satellite navigation systems
2. SPACE SOFTWARE VALIDATION USING ABSTRACT INTERPRETATION
3. A Symbolic Model Checking Approach to Verifying Satellite Onboard Software
4. Spacecraft early design validation using formal methods
5. The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions
6. Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems
7. Formal Analysis of a Space Craft Controller using SPIN
8. FORMAL VALIDATION OF AEROSPACE SOFTWARE
9. Formal Specification and Quantitative Analysis of a Constellation of Navigation Satellites

Уже лет 10 существует серия Европейских стандартов на построение космических аппаратов,
и в частности, на разработку бортовых программ (ECSS‐E‐ST‐40C) и требований к ним.
Блок стандартов можно выкачать по ссылке

http://escies.org/ftp/ecss.nl/ISO

Там прописаны формальные методы, инженерия требований и системная инженерия.
Стандарты NASA в космической отрасли обновляются каждые пять лет.
А где наши стандарты?

Стандарт MISRA уже несколько раз упоминался на форуме:
http://forum.oberoncore.ru/viewtopic.php?f=70&t=5172&hilit=MISRA
http://forum.oberoncore.ru/viewtopic.php?f=115&t=615&p=65550&hilit=MISRA#p65550

Сейчас снова просмотрел правила MISRA и действительно большинство правил исправляют дефекты языка Си, а к Оберону не применимы.

Поэтому первый шаг - это не использовать язык Си. А второй шаг - использовать формальные методы.

Бортовое программирование у нас

В Роскосмосе нет бортового программирования. Слово "программирование" не встречается в многочисленных материалах Роскосмоса.
Никто из руководства Роскосмоса не имеет соответствующего образования, чтобы понимать, что такое бортовое программирование. В плане образования ключевыми здесь являются две дисциплины: системное программирование и операционные системы реального времени.

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

Для руководителей космической отрасли бортовая программа -- это специальная железка, которая вставляется в КА. Такой у них уровень компетенции. Возможно единственное исключение -- академик Евгений Микрин, автор серии учебников по технологии бортового программирования.

Данная ситуация с бортовым программированием в космической отрасли сложилась еще со времен СССР.

На каждом предприятии по разработке КА есть подразделение бортового программирования для КА. Технология программирования базируется на предыдущем опыте и регламентируется лишь ГОСТами. Развитие технологии в компетенции руководителя подразделения и существенно зависит от его квалификации. Оказывается, по крайней мере на двух предприятиях, технология застряла на уровне ассемблерного программирования. Разумеется, есть и позитивный опыт разработки добротной технологии бортового программирования.

Технологическое отставание от США, а теперь уже и от Китая, -- громадное. Сопоставьте нашу практику бортового программирования с опытом разработки программы Марсохода и китайским опытом применения формальных методов в космической отрасли.

Почему так случилось

Можно говорить о советском наследии, о трудных 90-ых, о том, что космическая отрасль должна была реформироваться гораздо раньше.

Главная причина в другом. Обсуждение этого будет дальше.

Что надо сделать

Бортовое программирование должно быть унифицировано для разрабатываемых КА на разных предприятиях и проводиться в одном центре по примеру того, как это делается в NASA.

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

Кончено, это не все.

Здравствуйте, Владимир.

Что можете сказать про перспективы использования формальных методов при разработке бортового программного обеспечения?

Какие подход вы считаете наиболее перспективными?
- использование ручного доказательства при содействии proof checker-а.
- использование полностью автоматического доказательства

И какие методы Вы считаете наиболее перспективными?
- метод Хоара
- метод индуктивных утверждений
- Model Checking
- итд.

Владимир Шелехов ответил Рифату здесь:
viewtopic.php?p=99879#p99879

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

На самом деле в космической отрасли США ситуация с бортовым программированием в космической отрасли весьма далека от идеала.

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

В настоящее время космический аппарат, будь то американский марсоход, или спутник АО "ИСС" - это программно-аппаратный комплекс, и успех космических миссий напрямую зависит не только от надежности бортовой аппаратуры, но и от качества бортового программного обеспечения. Я даже встречал термин "software defined spacecraft".