Вот, по просьбам трудящихся открываю новую тему.
Для затравки:
Нами разработана комплексная методология информационной поддержки этапов жизненного цикла БПО и вообще программ управления реального времени, включая методы спецификации, верификации, автоматического синтеза управляющих программ, определения характеристик и генерации тестов для них.
ЦитироватьВот, по просьбам трудящихся открываю новую тему.
Для затравки:
Нами разработана комплексная методология информационной поддержки этапов жизненного цикла БПО и вообще программ управления реального времени, включая методы спецификации, верификации, автоматического синтеза управляющих программ, определения характеристик и генерации тестов для них.
Два вопроса:
1) Мы, это кто?
2) Где можно узнать подробности?
Затрагивается ли серая область программируемой аппаратуры (FPGA)? Или само-перепрограммируемой в реальном масштабе времени?
ЦитироватьНами разработана комплексная методология...
На каких КА она использовалсь/используется/планируется использоваться?
Цитировать1) Мы, это кто?
Научно-исследовательская группа СГАУ
Цитировать2) Где можно узнать подробности?
Пишите в личку, подумаем, как организовать.
Объектом моделирования и разработки являются управляющие алгоритмы реального времени и программы комплексного функционирования, в которых важны временные соотношения между выдачей управляющих воздействий на БА и другие программы БПО (насколько я знаю, они на разных фирмах называются по-разному), то есть речь не идет о вычислительных алгоритмах и проблематике обработки сложных структур данных.
Разработана на протяжении ряда лет комплексная методология, позволяющая пройти цепочку от спецификации до готовой программы, набора тестов для нее и автоматически определенных некоторых характеристик.
ЦитироватьЦитироватьНами разработана комплексная методология...
На каких КА она использовалсь/используется/планируется использоваться?
Изделия ЦСКБ-Прогресс
ЦитироватьЗатрагивается ли серая область программируемой аппаратуры (FPGA)? Или само-перепрограммируемой в реальном масштабе времени?
Нет
C предыдущей ветки:
ЦитироватьЦитироватьЕсли речь о верификации, то там много чего сделано, тов. Хольцманн в JPL не зря свой хлеб ест. Есть также ряд интересных направлений в CSAIL. MIT. В частности, достаточно давно научились генерировать спецификации автоматически из кода программы и верифицировать их. Естественно, с ограничениями (предполагая что P != NP), но работает
Ой, а можно поподробнее? В новой теме:
http://www.novosti-kosmonavtiki.ru/phpBB2/viewtopic.php?p=156094#156094
А ссылки на указанные Вами работы в Интернете есть?
Gerard Holzmann - достаточно известный в мире товарищ, занимающийся верификацией ПО. Известен тем, что написал SPIN (http://spinroot.com) - верификатор программ, использующий темпоральную логику для аннотации программ и находящий в них логические казусы с параллелизмом (тупики, конкурентный доступ к памяти, неотловленные исключения и т.д.) Все это хозяйство им было написано в бытность сотрудника Bell Labs, сейчас работает в NASA (JPL), в лаборатории надежного ПО (http://eis.jpl.nasa.gov/lars), прославился и там, в частности тем, что с помощью своего метода нашел несколько критических ошибок в
отлаженном и готовом к старту БПО Deep Space 1 (кажется пять), связанных с конкурентным доступом к памяти.
. Они же в JPL разработали Java PathFinder, инструмент, автоматически аннотирующий ПО спецификациями подходящими для SPIN. [/url]
И кстати, специально для Старого, у БПО Deep Space 1, до того как за него взялся Хольцман, было 800 часов предполетного тестирования, тем не менее, как видите, были допущены и не обнаружены критические ошибки в коде.
ЦитироватьНами разработана комплексная методология информационной поддержки этапов жизненного цикла БПО и вообще программ управления реального времени, включая методы спецификации, верификации, автоматического синтеза управляющих программ, определения характеристик и генерации тестов для них.
Можно конкретнее о спецификации и верификации? Это дедуктивный анализ с доказательством теорем и т.д. или модельный подход?
Не могли бы ли вы дать ссылочку на статью или краткое описание методологии? Может быть издана какая-нибудь литература? Можно и по почте.
Вопрос, конечно, сам по себе более, чем актуальный. Попыток решения его была предпринята масса, но пока революционных переворотов не произошло. Так или иначе, любые мысли по этой теме интересны и могут быть полезны.
ЦитироватьИзделия ЦСКБ-Прогресс
Значит есть опыт практического применения на реальных КА.
Тогда такой вопрос, если можно.
Относится ли эта методология ко всем или только к некоторым видам испытаний: автономной отладке программ, автономным испытаниям программ и приборов, частным проверкам, регламентым работам, компексным испытаниям на стендах с математичской моделью, в КИСе, на полигоне, в полете?
ЦитироватьМожно конкретнее о спецификации и верификации? Это дедуктивный анализ с доказательством теорем и т.д. или модельный подход?
И то, и другое. Есть, с одной стороны, семейство формальных теорий для описания УА РВ, позволяющих проводить логический вывод. У нас используется не классическая темпоральная логика, но достаточно похожие методы.
С другой - построена модель семантики, которая позволяет проверять ряд вещей прямо на ней.
ЦитироватьНе могли бы ли вы дать ссылочку на статью или краткое описание методологии? Может быть издана какая-нибудь литература? Можно и по почте
Да, публикации есть. В журнале "Полет", например, №12 за 2005 год,
"Известия РАН. Теория и системы управления" - №2, 2006.
Вообще-то с качественными описаниями есть определенный напряг.
Но со всеми, кто заинтересовался, буду рад установить контакт - пишите личное сообщение с e-mail, что-нибудь вышлю.
ЦитироватьC предыдущей ветки:
Gerard Holzmann - достаточно известный в мире товарищ, занимающийся верификацией ПО. Известен тем, что написал SPIN (http://spinroot.com) - верификатор программ, использующий темпоральную логику для аннотации программ и находящий в них логические казусы с параллелизмом (тупики, конкурентный доступ к памяти, неотловленные исключения и т.д.) Все это хозяйство им было написано в бытность сотрудника Bell Labs, сейчас работает в NASA (JPL), в лаборатории надежного ПО (http://eis.jpl.nasa.gov/lars), прославился и там, в частности тем, что с помощью своего метода нашел несколько критических ошибок в отлаженном и готовом к старту БПО Deep Space 1 (кажется пять), связанных с конкурентным доступом к памяти. . Они же в JPL разработали Java PathFinder, инструмент, автоматически аннотирующий ПО спецификациями подходящими для SPIN. [/url]
Спасибо, начал смотреть.
Кстати, говоря о нашей методологии, могу сказать, что одним из плюсов ее является гибкая настраиваемость на целевой язык программирования, на котором генерируется управляющая программа - хоть Си, хоть ассемблер, хоть еще какой-нибудь.
И еще - у нас активно применяются визуальные методы и представления.
ЦитироватьЦитироватьИзделия ЦСКБ-Прогресс
Значит есть опыт практического применения на реальных КА.
Тогда такой вопрос, если можно.
Относится ли эта методология ко всем или только к некоторым видам испытаний: автономной отладке программ, автономным испытаниям программ и приборов, частным проверкам, регламентым работам, компексным испытаниям на стендах с математичской моделью, в КИСе, на полигоне, в полете?
Значит, так. Мы называем сейчас нашу методологию методологией CALS, поскольку она поддерживает самые разные этапы жизненного цикла управляющих алгоритмов и программ реального времени:
1) спецификацию - с использованием символического или визуального языка (здесь возможная формальная верификация на непротиворечивость и проверка важных свойств, плюс проверка выполнимости спецификации на заданном базисе функциональных задач);
2) построение множества возможных вариантов исполнения (таблица значимых комбинаций значений встречающихся в алгоритме условий);
3) автоматическую генерацию технической документации на алгоритм, включая графические документы - временную диаграмму и блок-схему;
4) автоматический синтез программы, удовлетворяющей спецификации, на целевом языке программирования (еще раз подчеркну, что речь не идет о сложных вычислительных алгоритмах, а именно о координирующих согласованную работы элементов БА и БПО);
5) генерация отладочных заданий для каждого из возможных вариантов исполнения алгоритма - с необходимыми точками останова, проверочными печатями значений переменных, и т.д. Опять же - не вычислительные алгоритмы;
6) определение характеристик программы по характеристикам ее базовых составляющих.
Методология позволяет и затем, в процессе эксплуатации, в случае необходимости вностить изменения в визуальном редакторе, и автоматически получать весь пакет документов + перегенерировать программу, что открывает простор для доработок и коррекций ПО.
По Вашим вопросам - автономная отладка поддерживается, совместная на уровне генерации таблиц входных и выходных информационных и управляющих связей, комплексная пока нет.
Хотя примечательно то, что наша методология может быть применена не только к алгоритмам БПО, но и к алгоритмам моделей бортовых систем, использумемы при испытаниях - то есть все перечисленные этапы можно проходить для программ моделей. Опять же, вся сложная вычислительная часть выносится при этом в функциональные программы.
Не могу сказать, что мы предлагаем какой-то готовый рыночный продукт, но заинтересованы в продвижении и развитии нашей методологии, включая применение в других космических КБ, да и вообще в предметных областях, где используется управление в реальном времени с использованием ЦВМ.
Большое спасибо за подробный ответ. Стало более понятно о чем идет речь. Дело сложное, но по-видимому нужное, потому что "кое-где у нас порой" в этой области практикуется абсолютно ненаучная самодеятельность. Ваша методология выглядит серьезной и продуманной.
Цитироватьнаша методология может быть применена не только к алгоритмам БПО, но и к алгоритмам моделей бортовых систем, использумемы при испытаниях
Конечно.
Цитироватьавтономная отладка поддерживается, совместная на уровне генерации таблиц входных и выходных информационных и управляющих связей, комплексная пока нет
Понятно, комплексные испытания самые сложные. Но, надо надеятся, что это "пока нет" - кратковременное, освоите и их.
ЦитироватьНе могу сказать, что мы предлагаем какой-то готовый рыночный продукт, но заинтересованы в продвижении и развитии нашей методологии, включая применение в других космических КБ
А с Энергией не пробовали взаимодействовать? Там тоже что-то развивали в этом направлении, ну и кроме того у них есть некоторый международный опыт.
С НПО ПМ попробуйте поработать. Там нач. отдела систем ориентации и стабилизации восприимчив в принципе к разного рода визуальным методикам разработки БПО. И не только. То же есть значительный опыт взаимодействия с французами, начиная с Сесата и далее до сих пор. Знакомство хорошее у них с тем, как это дело поставлено в Аэроспасьале. Кстати, с Самарской наукой они уже давно работают, по динамике упругого КА. Если нужно, могу скинуть e-mail контакты, какие есть, в личные сообщения.
Кому интересно - вот тут
http://grafkont.boom.ru
есть старое и отнюдь не идеальное описание технологии.
Вызывает положительные эмоции мнение нынешнего Генконструктора НПО им. Лавочкина В. Хартова, высказанное им в связи с анализом причин аварии "Фобос-Грунта": http://lenta.ru/articles/2013/01/29/laspace/ (http://www.avanturist.org/redirect?url=http%3A%2F%2Flenta.ru%2Farticles%2F2013%2F01%2F29%2Flaspace%2F) "Стала ясна необходимость срочного внедрения строго промышленного подхода к программированию".
Нужна систематизация лучшего опыта - имеющегося у отдельных предприятий в отрасли и внутри страны, и передового зарубежного. И его применение в нашей космической промышленности.
Вообще, аналогичные мысли записаны и в решении конференции по системам управления КА, прошедшей осенью 2012 в МОКБ "Марс" http://mars-mokb.ru/Reshenie.pdf
И в статье http://ubs.mtas.ru/upload/library/UBS3914.pdf
Не знаю как внедрять промышленный подход программирования для уникальных аппаратов, а не серийных, как это было в ИСС. Хартову виднее, конечно. Пока трудно судить о результатах проводимой им политики на НПОЛ, ибо ни одного аппарата заложенных при нем и по его подходам еще не полетело. Да и что-то подсказывает, что ждать этого еще лет 10...
ЦитироватьEchidna пишет:
Да и что-то подсказывает, что ждать этого еще лет 10...
Ужас...
А "Луны-Глоб" в ближайшие 2-4 года? Они ведь существенно переработаны с учетом опыта ФГ - во всяком случае об этом писали весь прошлый год. Да и десантный модуль Экзомарса будет отечественным.
Цитироватьphobos24 пишет:
ЦитироватьEchidna пишет:
Да и что-то подсказывает, что ждать этого еще лет 10...
Ужас...
Денис, мы с тобой точно поседеть успеем :) И БИБ вместе с нами поседеет. :)
ЦитироватьEchidna пишет:
Пока трудно судить о результатах проводимой им политики на НПОЛ, ...
Возможно и не придётся судить, ввиду недолгости проведения...
ЦитироватьVeganin пишет:
Да и десантный модуль Экзомарса будет отечественным.
Что именно? БЦВМ (она там называется CTPU) делает Талес-Аления, я недавно как раз Design Report ее изучал.
ЦитироватьEchidna пишет:
Не знаю как внедрять промышленный подход программирования для уникальных аппаратов, а не серийных, как это было в ИСС. Хартову виднее, конечно. Пока трудно судить о результатах проводимой им политики на НПОЛ, ибо ни одного аппарата заложенных при нем и по его подходам еще не полетело. Да и что-то подсказывает, что ждать этого еще лет 10...
А что, в ИСС был внедрён промышленный подход к программированию ;) ?? Ну, правда, комплексный программный НОК хорош, безусловно.
ЦитироватьSOE пишет:
ЦитироватьVeganin пишет:
Да и десантный модуль Экзомарса будет отечественным.
Что именно? БЦВМ (она там называется CTPU) делает Талес-Аления, я недавно как раз Design Report ее изучал.
А по-моему этот вопрос еще не решен. ;) По крайней мере в Соглашении про это НИЧЕГО нет.
ЦитироватьEchidna пишет:
По крайней мере в Соглашении про это НИЧЕГО нет.
А что там должно быть? EDM TAS как делала, так и делает. Идея пристроить RTG российский и/или нагреватель изотопный умерла в июне после отказа Роскосмоса, научная ПН из РФ, насколько помню, оттуда сгинула ранней осенью.
Мы про десантный модуль 2016 или 2018 говорим?))
Я про EDM в 2016. По Сarrier Module для 2018 не все еще решено. По нему работы находятся в начале "Phase B", то есть, дверь еще открыта. Но если подряжаться быть головными по бортовому ПО, то надо понимать, что делать все надо будет по требованиям и стандартам ЕКА (и CCSDS с точки зрения радиоинтерфейса, и телеметрии/телекоманд). Это серьезное и обдуманное решение должно быть, сразу предупреждаю :)
ЦитироватьFrontm пишет:
ЦитироватьEchidna пишет:
Пока трудно судить о результатах проводимой им политики на НПОЛ, ...
Возможно и не придётся судить, ввиду недолгости проведения...
А поподробнее в этом месте можно? А то публика в задних рядах интересуется. И чем дальше, тем больше. Некоторые даже делают ставки.
Да мне-то куда подробнее? Я чисто так... из сопереживания. А вам виднее и без меня. И результаты видны лучше чем мне. Привет публике в задних рядах.
хотя похоже вопрос не ко мне)) извиняюсь)
Echidna, угу, это в мой огород. :D
ЦитироватьVladimir пишет:
ЦитироватьFrontm пишет:
Возможно и не придётся судить, ввиду недолгости проведения...
А поподробнее в этом месте можно? А то публика в задних рядах интересуется. И чем дальше, тем больше. Некоторые даже делают ставки.
Сомневаюсь, что слышали или знаете меньше меня. :D Ключевое слово - возможно, ибо слухи всякие, кои не берусь озвучивать.
Давно не новость о разделении ГД и ГК. Каков выбор и устроит ли одна из двух должностей - не интересовался.
П. теперь первый зам только единожды, а не дважды. А ставки делают, случаем, не на ГД или ГК некоего В. ?
Если что-то знаете точно и озвучите, было бы хорошо.
Ну, то, что я слышал, тоже относится к категории слухов. Хотя, сдается мне, кое-какие из них воплотятся в жизнь, и довольно скоро. Уж больно поведение и поступки интересующих нас персонажей к этому располагают.
Я никогда не играл в "Угадай мелодию", а потому затрудняюсь расшифровать фамилию по одной букве В. Не подбросите еще пару букв?
ЦитироватьFrontm пишет:
А ставки делают, случаем, не на ГД или ГК некоего В.?
Говорят про В., но, наверное, надо дождаться марта, когда для Х. может освободиться место в Ц.
ЦитироватьVladimir пишет:
Я никогда не играл в "Угадай мелодию", а потому затрудняюсь расшифровать фамилию по одной букве В. Не подбросите еще пару букв?
Последняя такая же.
Цитироватьanik пишет:
ЦитироватьFrontm пишет:
А ставки делают, случаем, не на ГД или ГК некоего В.?
Говорят про В., но, наверное, надо дождаться марта, когда для Х. может освободиться место в Ц.
"Я буду в «
М» ходить до самой смерти, Хотя меня и посылают в «Ж»" А. Иванов
SOE пишет:
Цитироватьнадо понимать, что делать все надо будет по требованиям и стандартам ЕКА (и CCSDS с точки зрения радиоинтерфейса, и телеметрии/телекоманд). Это серьезное и обдуманное решение должно быть, сразу предупреждаю :)
Какое отношение радиоинтерфейс имеет к разработке БПО?
Цитироватьleha13 пишет:
Какое отношение радиоинтерфейс имеет к разработке БПО?
Я упомянул, потому что "задел" CCSDS. Вы правы, прямого отношения не имеет.