SpaceX Falcon 9

[Not]

Kap пишет:

Not пишет:
Вы ничего не поняли из вышенаписанного. Речь шла о формальном доказательстве корректности, что с тестирование имеет мало общего.

Тестирование и формальное доказательство корректности нужны для одного и того же - правильной работы ПО.

Верно.

Kap пишет:
Причем в случае с современными коммерческими программами которые без ООП писать практически нереально применяется именно первое - предикаты и логические схемы получались бы неохватными. Да, для встроенных систем, которыми является СУ РН, все еще подходят методы до-объектной эры, но если писать с использованием ТДД и юниттестов - результат будет как минимум приближаться к ПО с формально-доказанной надежностью при том что сильно дешевле. Или все-таки использовать Яву - у организаций, заинтересованных в надежности явамашин денег на ее обеспечение больше весь бюджет НАСА даже по-отдельности, а разница в скорости с Си нынче менее чем двукратная что более чем достаточно если не увлекаться "быстрыми" процессами (ракеты успешно летали еще в 60е).

Полный бред. Давайте наведем порядок в вашем сумбуре. Мы говорим ТОЛЬКО о высоконадежных СУ РВ. Все остальные коммерческие системы за скобками. Ява в ее стандартном виде категорически не подходит вследствии недетерминированности времени исполнения (сборка мусора, латентность при переключении контекстов, доступе к железу, и т.д.). Существует Ява для систем реального времени, но ее мало используют, поскольку ООП для которого она предназначена мало применимо в высоконадежных системах управления. Почему - тема отдельная. Если интересно - заведите ветку, расскажу там.

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

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

Kap пишет:

Not пишет:
Нельзя. В качестве примера вам один из последних дефектов в OpenSSH когда всем (ВСЕМ!) пришлось обновить ПО.

Какая связь между БСДшной программой для шифрования связи и ядром линукса? Правильно - никакой. Ну и новые версии оси СУ РН требуются несколько реже.

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

Kap пишет:

Not пишет:
Методы создания высоконадежного ПО не имеют ничего общего с методами созднания открытыхпрограммных систем.

По все той же вике Фалькон летает на линуксе. То что виноват софт пока что только предположение.

Как "летает" Фалькон на линуксе мы вчера видели. Попробуйте рассмотреть ПО которое пишут Энергия, Боинг, Локхид и поищите там Линукс.

[silentpom]

Кто нить в состоянии припомнить проблемы с наддувом баков у других РН?

[Not]

Элон Маск
Cause still unknown after several thousand engineering-hours of review. Now parsing data with a hex editor to recover final milliseconds.

Во как! В ход пошла тяжелая техника - шестнадцатеричный редактор  

[Veganin]

salto пишет:

Kap пишет:
Давление в баке окислителя верхней ступени привысило норму. Походе учудила система наддува.

Кто может описать систему наддува бака окислителя верхней ступени?

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

[НИИзнайка]

Я так понял, это летел уже прототип пилотируемого Драгона. Система спасения (нижняя!) уже была ? если да - то почему не сработала, не увела корабль?

[silentpom]

откуда вы это поняли???

[Искандер]

Not пишет:

Искандер пишет:
Неприятно, но впечатление что опять какая-то мелкая фигня типа клапана или в алгоритмах управления/контроля что-то забыли прописать, не предусмотрели. Короче детские болезни...
Лучше уж сейчас чем с экипажем.

Проблема однако в том, что этой "мелкой фигни" в РКН достаточно много и выявлять по одной за пуск выглядит нежизнеспособно.

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

Нежизнеспособно? А что делать? На то ЛКИ и существуют чтобы выявить баги, набраться опыта. Подчистят, подправят.
Я не думаю, что там причина в выходе за границы множества ограничений РН - это же не первый полёт. Скорее телеметрия не рассматривала в качестве аварийных все критичные параметры второй ступени пока первая работает или ещё какая нибудь тупость. Иначе выключили бы двигатели раньше взрыва и могли попытаться вернуть Дракон, а может даже каким-то образом и первую ступень.

Даже если Вы правы, то это не первый раз, когда F9 допиливают/доделывают - то гидравлическую жидкость доливают, то решетчатые рули устанавливают, то вместо гидразиновых газовые рули ставят - и т.д. В итоге потребительские свойства и надежность F9 растут. Тут другая проблема - Маск не может остановится, РН всё время меняют.

[Андрей Иванов]

Эксперт: стоимость пуска ракеты Falcon 9 может вырасти из-за аварии

Вряд ли единичная авария скажется на стратегических перспективах SpaceX и частной космонавтики в целом. Илона Маска (главу SpaceX - прим. ТАСС) как поддерживало, так и продолжит поддерживать американское космическое агентство. Но после этой аварии повысится стоимость страховки, соответственно, вырастет стоимость пуска. Скорее всего, не больше чем на 20%. 
компании SpaceX, возможно, придется пересмотреть программу подготовки к пилотируемым запускам и заново набрать статистику успешных пусков Falcon 9, чтобы ее можно было использовать при запуске пилотируемых кораблей.
Теперь программа повторного использования ступеней ракеты-носителя откладывается. Практика показывает, что отработка займет еще не один год"

http://tass.ru/kosmos/2079163

[Salo]

Вы почто Сашу Ильина aka Lin заанонимили?

[Kap]

vlad7308 пишет:
а разве софт, подобный СУ РН, делается не под системы реального времени?

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

silentpom пишет:
как человек, 10 лет страдавший дедлоками - бесплатный и надежный линукс тут скорее создает проблемы, чем решает.

Прогресс тут на месте совсем не стоял.

Not пишет:
Давайте наведем порядок в вашем сумбуре. Мы говорим ТОЛЬКО о высоконадежных СУ РВ

Что за зверь такой "высоконадежная"? Маск тратить деньги на формальную проверку мог очень врядли, а проблемы с софтом у него до сих пор только гипотетические. Так что надежность софта у него вполне высокая.

Not пишет:
Все остальные коммерческие системы за скобками.

Современные коммерческие системы имеют статистику работы которая ни одной РН не снилась. Довольно часто имеет околонулевой процент отказов.

Not пишет:
Ява в ее стандартном виде категорически не подходит вследствии недетерминированности времени исполнения (сборка мусора, латентность при переключении контекстов, доступе к железу, и т.д.).

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

Not пишет:
Теперь о тестировании и формальном доказательстве корректности. Тестирование - это частный случай динамического анализа, когда вы показываете, что на всех ваших тестовых наборах система работает корректно. Формальное доказательство - статический анализ, который по сути полная противоположность анализа динамического - он гарантирует, что на всех допустимых диапазонах входных данных система работает корректно.

Любую программу можно рассматривать как математическую функцию - даже целая парадигма на этом основана. Правильность работы алгоритма при наборе аргументов А означает соответствие значения этой функции при А ожидаемому. Так вот, "все допустимые" диапазоны для РН избыточны: мы знаем что атмосферное давление ни когда не может существенно превышать 1 атмосферу, а если превышает - надежность софта уже не поможет. И таких примеров куча ибо запуск ракеты очень хорошо изучен. Т.е. для марсохода находить область значения нашей программы на всей области определения - нужно и оправдано, для РН - атавизм времен "когда компьютеры были большими"(с).

Not пишет:
- это всего лишь пример когда ошибка в чрезвычайно важном участке кода не была замечена в течении многих лет миллионами глаз.

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

Not пишет:
Как "летает" Фалькон на линуксе мы вчера видели.

Уже доказано что виновато ПО или как?

[Not]

Kap пишет:
Уже доказано что виновато ПО или как?

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

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

[Дмитрий В.]

Искандер пишет:

Тут другая проблема - Маск не может остановится, РН всё время меняют.

Что с него взять? Он, похоже, перфекционист: "всегда есть лучшее решение", "хорошее - враг лучшего" etc.

[Искандер]

Дмитрий В. пишет:

Искандер пишет:

Тут другая проблема - Маск не может остановится, РН всё время меняют.

Что с него взять? Он, похоже, перфекционист: "всегда есть лучшее решение", "хорошее - враг лучшего" etc.

Для пилотируемых полётов нужно остановиться.
Надеюсь F9 v1.2 это всё.
Ему бы лучше переключится на метан и на новый носитель, только с газ-газ это на годы.

[salto]

silentpom пишет:
Кто нить в состоянии припомнить проблемы с наддувом баков у других РН?

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

[Вован]

salto пишет:

silentpom пишет:
Кто нить в состоянии припомнить проблемы с наддувом баков у других РН?

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

Оригинально!

[OlegN]

salto пишет:

silentpom пишет:
Кто нить в состоянии припомнить проблемы с наддувом баков у других РН?

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

Я цепочку не понял  .Можно прояснить?

[Александр Ч.]

http://spaceflightnow.com/2015/06/29/satellite-owners-bystanders-in-falcon-9-accident/

...
SpaceX had replaced the Proton rocket, which is marketed by U.S.-based International Launch Services, as a leader in the worldwide launch services sector before Sunday's failure. The California-headquartered rocket firm, founded in 2002 by technology billionaire Elon Musk, could retain its position in the commercial launch market barring more setbacks or lengthy delays, industry officials said.
...

SpaceX's Falcon 9 also won commercial launch competitions by amassing 18 straight successes in the rocket's first 18 missions.
The withdrawal of Sea Launch, a Russian-led consortium with an operations base in Long Beach, California, from the launch services market also opened a window for SpaceX. Chinese Long March rockets are off limits for satellites with U.S.-made components — a restriction that covers nearly all commercial communications platforms — and Russia's Proton rocket has reliability woes.
ULA's Atlas 5 rocket is a marginal player in the commercial marketplace due to high prices and a manifest crammed with U.S. government missions.

А так заметка про то что:

Моя мама варит классно, может быть
Подождем мою маму,
Подождем твою мать

[Александр Ч.]

OlegN пишет:

salto   пишет:

silentpom пишет:
Кто нить в состоянии припомнить проблемы с наддувом баков у других РН?

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

Я цепочку не понял  .Можно прояснить?

Цепочка простая: бак окислителя наддувают газом из газогенератора - продуктами сгорания керосина в кислороде. А продукты сгорания у нас что? Вода и углекислый газ. Температура плавления сухого льда  -55,6°C, плотность 1560 кг/куб.м, а у жидкого кислорода температура не выше −182,96°C и плотность 1141 кг/куб.м. Значит газ наддува остынет, углекислый газ и вода замерзнут, при этом сухо лед выпадет в осадок и забьет топливный фильтр.

PS Обращаю внимание на смайлик.

[salto]

Александр Ч. пишет:

OlegN пишет:

salto пишет:

silentpom пишет:
Кто нить в состоянии припомнить проблемы с наддувом баков у других РН?

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

Я цепочку не понял.Можно прояснить?

Цепочка простая: бак окислителя наддувают газом из газогенератора - продуктами сгорания керосина в кислороде. А продукты сгорания у нас что? Вода и углекислый газ. Температура плавления сухого льда-55,6°C, плотность 1560 кг/куб.м, а у жидкого кислорода температура не выше −182,96°C и плотность 1141 кг/куб.м. Значит газ наддува остынет, углекислый газ и вода замерзнут, при этом сухо лед выпадет в осадок и забьет топливный фильтр.  

Александр Ч.,спасибо! Мне и комментировать ничего не нужно. Конечно, это была только разновидность проблем в системах наддува.

[vadimr]

Kap пишет:

Not пишет:
Вы ничего не поняли из вышенаписанного. Речь шла о формальном доказательстве корректности, что с тестирование имеет мало общего.

Тестирование и формальное доказательство корректности нужны для одного и того же - правильной работы ПО. 

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

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

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