Монитор-Э готов

[ДмитрийК]

типа формальные спецификации быстро становятся больше по объему чем сама программа и встает вопрос а как доказать корректность спецификаций итд. рекурсивно Пока особого прогресса не видно.

А что вы подразумеваете под доказательством корректности спецификации? Верификацию (доказательство что она завершима, не переполняет буфера, не конкурирует за ячейки памяти и т.д.) или валидацию - т.е. доказательство того, что спецификация соответствует т.з?

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

[Not]

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

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

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

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

[Старый]

А я вот думаю: неужели нельзя всё это проверить на земле создав космическому аппарату условия которые он будет испытывать в полёте?

[Not]

А я вот думаю: неужели нельзя всё это проверить на земле создав космическому аппарату условия которые он будет испытывать в полёте?

К сожалению, всё проверить невозможно - количество тестовых комбинаций экспоненциально от количества "элементарных" компонентов системы.

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

А я вот думаю: неужели нельзя всё это проверить на земле создав космическому аппарату условия которые он будет испытывать в полёте?

На 100% соответствие не получишь. Часть аппаратуры приходится заменять имитаторами и математическими моделями. В которых тоже могут быть ошибки. Пример из личной практики: когда включили MDM на ФГБ на 5-е сутки его полета, провели выставку бортовой шкалы времени в MDM. И сразу "улетели" на два месяца вперед. Все массивы КПИ были тщательно проверены и перепроверены на стенде. Все, казалось, было в порядке. А потом выяснили, что в составе стенда использовалась модель бортовой аппаратуры КИС "Компарус", которая использовалась для задания БШВ. И в модели была ошибка (сдвиг счетчика на три разряда). А по этой модели отлаживалось бортовое ПО. Ошибку можно было бы обнаружить только при использовании реальной бортовой аппаратуры. У разработчиков ПО такой аппаратуры не было, естественно. Пришлось разрабатывать и вводить первую программу-вставку в MDM ФГБ.

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

[Старый]

Ошибку можно было бы обнаружить только при использовании реальной бортовой аппаратуры. У разработчиков ПО такой аппаратуры не было, естественно.

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

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

Так вот я и спрашиваю: почему же не делают полностью эквивалентные испытания чтобы все не замеченые ошибки вылезли ещё до запуска? Хорошо если ошибка не приведёт к фатальным последствиям, а если приведёт? Всем памятна история м Полар Лэндером. И у нас Монитр чуть не грохнули.

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

Да, блин, быстрее всего это главное. Как в фильме "А зори здесь тихие": - "Спешила я!".

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

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

[Старый]

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

[Старый]

Это суровая реальность, а она имеет мало общего с прекраснодушными мечтаниями Маниловых.

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

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

Это суровая реальность, а она имеет мало общего с прекраснодушными мечтаниями Маниловых.

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

А кто говорит, что испытания не проводятся? Еще как проводятся. Но еще раз повторяю для тех, кто едет на бронепоезде: любой проект, в том числе, и создания спутника имеет бюджет. Выходить за который не всегда удается. И решение по объему испытаний принимает заказчик, выделяя деньги на постройку аппарата. В том числе и то, сколько он готов заплатить за отработку и испытания. Чудес не бывает, за все приходится платить. Еще раз говорю, это реалии жизни.
Или ты думаешь, что изготовителю наплевать на результат своей работы? И он не заинтересован в том, чтобы сделать ее лучше? Тогда мы имеем очередной всплеск конспирологии: все разработчики и изготовители либо идиоты, либо вредители.

[ДмитрийК]

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

Ну так расскажите скорее пока Старый опять всю тему не за@$%л Впрочем можно и новую тему открыть.

[TAU]

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

Это каких? Можно поподробнее?
Я читал об опыте применения формальной верификации к софту - идея заманчивая но это палка о двух концах, типа формальные спецификации быстро становятся больше по объему чем сама программа и встает вопрос а как доказать корректность спецификаций итд. рекурсивно Пока особого прогресса не видно.

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

Так что прогресс есть  :wink:

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

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

Это каких? Можно поподробнее?
Я читал об опыте применения формальной верификации к софту - идея заманчивая но это палка о двух концах, типа формальные спецификации быстро становятся больше по объему чем сама программа и встает вопрос а как доказать корректность спецификаций итд. рекурсивно Пока особого прогресса не видно.

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

Так что прогресс есть  :wink:

А эта технология применима только к бортовому ПО или к любому? И можно ли где-нибудь почитать подробнее?

[TAU]

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

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

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

[TAU]

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

Это каких? Можно поподробнее?
Я читал об опыте применения формальной верификации к софту - идея заманчивая но это палка о двух концах, типа формальные спецификации быстро становятся больше по объему чем сама программа и встает вопрос а как доказать корректность спецификаций итд. рекурсивно Пока особого прогресса не видно.

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

Так что прогресс есть  :wink:

А эта технология применима только к бортовому ПО или к любому?

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

И можно ли где-нибудь почитать подробнее?

Пишите в личку.

[Старый]

В России начат прием данных с американского спутника-долгожителя LandSat-5, запущенного еще в далеком 1984 году, передает CNews.ru. Сделанные им снимки чрезвычайно важны для страны из-за отсутствия сегодня аналогичных отечественных данных такого рода.

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

 Хотя может Снюсь опять чтото перепутал?

[пежмарь]

Ну и как там?

Анекдот (в тему?):
- Это реанимация?
- Да.
- А больной Иванов жив?
- Пока нет ....

[ssv]

Кто вкурсе Монитор совсем готов или есть шансы. Есть информация что неделю в связь не могут войти и ориентации нет.

[Сафронов Иван]

Похоже скорее мертв, чем жив. Впрочем инфу об этом по-любому раньше конца октября, скорее всего, не получить: ведь на 27 октября намечены торжества по случаю 90-летия ЦиХ.

[ssv]

В чем проблема? Слышал потеря ориентации. ГИВУС чудит? Кто знает у Монитора есть резервный контур управления ориентации?