Методы и средства разработки БПО

[TAU]

Вот, по просьбам трудящихся открываю новую тему.

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

[А.Коваленко]

Вот, по просьбам трудящихся открываю новую тему.

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

Два вопроса:
1) Мы, это кто?
2) Где можно узнать подробности?

[eng. Alex]

Затрагивается ли серая область программируемой аппаратуры (FPGA)? Или само-перепрограммируемой в реальном масштабе времени?

[ДалекийГость]

Нами разработана комплексная методология...

На каких КА она использовалсь/используется/планируется использоваться?

[TAU]

1) Мы, это кто?

Научно-исследовательская группа СГАУ

2) Где можно узнать подробности?

Пишите в личку, подумаем, как организовать.

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

[TAU]

Нами разработана комплексная методология...

На каких КА она использовалсь/используется/планируется использоваться?

Изделия ЦСКБ-Прогресс

[TAU]

Затрагивается ли серая область программируемой аппаратуры (FPGA)? Или само-перепрограммируемой в реальном масштабе времени?

Нет

[Not]

C предыдущей ветки:

Если речь о верификации, то там много чего сделано, тов. Хольцманн в JPL не зря свой хлеб ест. Есть также ряд интересных направлений в CSAIL. MIT. В частности, достаточно давно научились генерировать спецификации автоматически из кода программы и верифицировать их. Естественно, с ограничениями (предполагая что P != NP), но работает

Ой, а можно поподробнее? В новой теме:
http://www.novosti-kosmonavtiki.ru/phpBB2/viewtopic.php?p=156094#156094

А ссылки на указанные Вами работы в Интернете есть?

Gerard Holzmann - достаточно известный в мире товарищ, занимающийся верификацией ПО. Известен тем, что написал SPIN - верификатор программ, использующий темпоральную логику для аннотации программ и находящий в них логические казусы с параллелизмом (тупики, конкурентный доступ к памяти, неотловленные исключения и т.д.) Все это хозяйство им было написано в бытность сотрудника Bell Labs, сейчас работает в NASA (JPL), в лаборатории надежного ПО , прославился и там, в частности тем, что с помощью своего метода нашел несколько критических ошибок в отлаженном и готовом к старту БПО Deep Space 1 (кажется пять), связанных с конкурентным доступом к памяти. . Они же в JPL разработали Java PathFinder, инструмент, автоматически аннотирующий ПО спецификациями подходящими для SPIN. [/url]

[Not]

И кстати, специально для Старого, у БПО Deep Space 1, до того как за него взялся Хольцман, было 800 часов предполетного тестирования, тем не менее, как видите, были допущены и не обнаружены критические ошибки в коде.

[Not]

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

Можно конкретнее о спецификации и верификации? Это дедуктивный анализ с доказательством теорем и т.д. или модельный подход?

[eng. Alex]

Не могли бы ли вы дать ссылочку на статью или краткое описание методологии? Может быть издана какая-нибудь литература? Можно и по почте.

[Feol]

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

[ДалекийГость]

Изделия ЦСКБ-Прогресс

Значит есть опыт практического применения на реальных КА.
Тогда такой вопрос, если можно.

Относится ли эта методология ко всем или только к некоторым видам испытаний: автономной отладке программ, автономным испытаниям программ и приборов, частным проверкам, регламентым работам, компексным испытаниям на стендах с математичской моделью, в КИСе, на полигоне, в полете?

[TAU]

Можно конкретнее о спецификации и верификации? Это дедуктивный анализ с доказательством теорем и т.д. или модельный подход?

И то, и другое. Есть, с одной стороны, семейство формальных теорий для описания УА РВ, позволяющих проводить логический вывод.  У нас используется не классическая темпоральная логика, но достаточно похожие методы.
С другой - построена модель семантики, которая позволяет проверять ряд вещей прямо на ней.

[TAU]

Не могли бы ли вы дать ссылочку на статью или краткое описание методологии? Может быть издана какая-нибудь литература? Можно и по почте

Да, публикации есть. В журнале "Полет", например, №12 за 2005 год,
"Известия РАН. Теория и системы управления" - №2, 2006.
Вообще-то с качественными описаниями есть определенный напряг.

Но со всеми, кто заинтересовался, буду рад установить контакт - пишите личное сообщение с e-mail, что-нибудь вышлю.

[TAU]

C предыдущей ветки:
Gerard Holzmann - достаточно известный в мире товарищ, занимающийся верификацией ПО. Известен тем, что написал SPIN - верификатор программ, использующий темпоральную логику для аннотации программ и находящий в них логические казусы с параллелизмом (тупики, конкурентный доступ к памяти, неотловленные исключения и т.д.) Все это хозяйство им было написано в бытность сотрудника Bell Labs, сейчас работает в NASA (JPL), в лаборатории надежного ПО , прославился и там, в частности тем, что с помощью своего метода нашел несколько критических ошибок в отлаженном и готовом к старту БПО Deep Space 1 (кажется пять), связанных с конкурентным доступом к памяти. . Они же в JPL разработали Java PathFinder, инструмент, автоматически аннотирующий ПО спецификациями подходящими для SPIN. [/url]

Спасибо, начал смотреть.

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

И еще - у нас активно применяются визуальные методы и представления.

[TAU]

Изделия ЦСКБ-Прогресс

Значит есть опыт практического применения на реальных КА.
Тогда такой вопрос, если можно.
Относится ли эта методология ко всем или только к некоторым видам испытаний: автономной отладке программ, автономным испытаниям программ и приборов, частным проверкам, регламентым работам, компексным испытаниям на стендах с математичской моделью, в КИСе, на полигоне, в полете?

Значит, так. Мы называем сейчас нашу методологию методологией CALS, поскольку она поддерживает самые разные этапы жизненного цикла управляющих алгоритмов и программ реального времени:
1) спецификацию - с использованием символического или визуального языка (здесь возможная формальная верификация на непротиворечивость и проверка важных свойств, плюс проверка выполнимости спецификации на заданном базисе функциональных задач);
2) построение множества возможных вариантов исполнения (таблица значимых комбинаций значений встречающихся в алгоритме условий);
3) автоматическую генерацию технической документации на алгоритм, включая графические документы - временную диаграмму и блок-схему;
4) автоматический синтез программы, удовлетворяющей спецификации, на целевом языке программирования (еще раз подчеркну, что речь не идет о сложных вычислительных алгоритмах, а именно о координирующих согласованную работы элементов БА и БПО);
5) генерация отладочных заданий для каждого из возможных вариантов исполнения алгоритма - с необходимыми точками останова, проверочными печатями значений переменных, и т.д. Опять же - не вычислительные алгоритмы;
6) определение характеристик программы по характеристикам ее базовых составляющих.

Методология позволяет и затем, в процессе эксплуатации, в случае необходимости вностить изменения в визуальном редакторе, и автоматически получать весь пакет документов + перегенерировать программу, что открывает простор для доработок и коррекций ПО.

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

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

[ДалекийГость]

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

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

Конечно.

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

Понятно, комплексные испытания самые сложные. Но, надо надеятся, что это "пока нет" - кратковременное, освоите и их.

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

А с Энергией не пробовали взаимодействовать? Там тоже что-то развивали в этом направлении, ну и кроме того у них есть некоторый международный опыт.

[Feol]

С НПО ПМ попробуйте поработать. Там нач. отдела систем ориентации и стабилизации восприимчив в принципе к разного рода визуальным методикам разработки БПО. И не только. То же есть значительный опыт взаимодействия с французами, начиная с Сесата и далее до сих пор. Знакомство хорошее у них с тем, как это дело поставлено в Аэроспасьале. Кстати, с Самарской наукой они уже давно работают, по динамике упругого КА. Если нужно, могу скинуть e-mail контакты, какие есть, в личные сообщения.

[TAU]

Кому интересно - вот тут

http://grafkont.boom.ru

есть старое и отнюдь не идеальное описание технологии.