Ответ на »сообщение 1164« (Снегурочка)
___________________________

Я практически не занимался построением корректных программ в том смысле, который имели в виду Давид Грис и Алагич с Арбибом, но слышал такое утверждение, что доказательство корректности программы на порядок сложнее самой программы. Если ПО Ариана имело объём в 80 тыс. строк, то доказательство его корректности имело бы объём около миллиона строк!

Допустим, что в подобных задачах деньгам особого счёта не ведут, но ведь всё равно, что бы построить такое доказательство, а затем ещё и верифицировать само доказательство - это же сколько времени нужно.
А тут ещё могут и спецификации вдруг измениться... Вапще ужассс!!

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

Хотя, тестирование программы для ПК и программы для ракеты - очень разные вещи. Не будешь же перезапускать ракету после патча вновь обнаруженной ошибки. :-)) А модель оборудования ракеты точно также может содержать ошибки...

Понятное дело, что верифицированный софт - самый лучший софт, но насколько такой достаточно сложный софт реален?
И поможет ли тут Оберон-технология? :о))

Ответ на »сообщение 1159« (Как слышно? Приём!)
___________________________

В отчёте по Ариан 5 (1996г, не путать с другим кряком - 2002 года) в числе
прочих выводов были даны рекомендации о необходимости "перекрывающих
и избыточных" тестов. Отнюдь не о простоте стуктуры программы или ясности
документации люди ведут речь.

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

Ответ на »сообщение 1159« (Как слышно? Приём!)
___________________________


В отчёте по Ариан 5 (1996г, не путать с другим кряком - 2002 года) в числе
прочих выводов были даны рекомендации о необходимости "перекрывающих
и избыточных" тестов. Отнюдь не о простоте стуктуры программы или ясности
документации люди ведут речь.


Неясно, как можно хорошо протестировать плохо структурированную программу.


>>> что в принципе можно сделать в таких обстоятельствах?

Я бы говорил о сетевой логике и топологии связей в проектировании систем.
Здесь появившаяся ошибка затухает, а не размножается или приводит к аварии.
Аварийный блок замещается соседями. Функциональность, конечно, падает,
но не катастрофически.

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


Проблема в том, что в Ариане для надежности (защиты от аппаратных сбоев?) использовалось дублирование.
Одна и та же ошибка "вырубила" сразу оба процессора.

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

Хотя нельзя сказать, что это панацея - всё равно ведь было признано, что ПО удовлетворяло всем спецификациям.

Интересно сравнить объём ПО в mission-critical системах вроде Ariane 5 и в современном ПО для персональных компьютеров.

Начну с последнего.

http://blogs.msdn.com/macmojo/archive/2006/11/03/it-s-all-in-the-numbers.aspx

About 30,000,000 lines of code make up the current version of Office that we are developing...

http://www.upgrade-cepis.org/issues/2005/3/up6-3Amor.pdf

the total source lines of code count for Debian 3.1 is 229,496,000 SLOC (Source Lines Of Code).
Largest package ... OpenOffice.org (1.1.3): 5,181,000 SLOC.
... Comparisons with other systems:
Microsoft Windows 3.1 (April 1992) 3,000,000
Microsoft Windows 95 (August 1995) 15,000,000
Microsoft Windows XP (2002) 40,000,000
Red Hat Linux 8.0 (September 2002) 50,000,000

А вот что я нашёл про Ariane:

http://www.inria.fr/actualites/inedit/inedit14_evea.en.html

between Ariane 4 and Ariane 5, the volume of software increased more than tenfold, now reaching some 80,000 lines of code.

Ну и напоследок - для тех, кто интересуется:
http://en.wikipedia.org/wiki/Source_lines_of_code

Ответ на »сообщение 1158« (Александр Смирнов)
___________________________
Верно. Датчик - лазерный гороскоп, который нужен был
только до и в момент старта.
Дык, и я о том - ошибка модели.
Не тому учат компетентных программистов.
Зацикливание на частностях приводит к повисанию.
"Тут и лежит главный резерв надежности".

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

"Если задача всё же не решается - решайте другую задачу".

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

Недостатки модели никакой язык программирования не компенсирует.

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

В отчёте по Ариан 5 (1996г, не путать с другим кряком - 2002 года) в числе
прочих выводов были даны рекомендации о необходимости "перекрывающих
и избыточных" тестов. Отнюдь не о простоте стуктуры программы или ясности
документации люди ведут речь.

>>> что в принципе можно сделать в таких обстоятельствах?

Я бы говорил о сетевой логике и топологии связей в проектировании систем.
Здесь появившаяся ошибка затухает, а не размножается или приводит к аварии.
Аварийный блок замещается соседями. Функциональность, конечно, падает,
но не катастрофически.

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

Извините, что вмешиваюсь.
На самом деле в случае с Ariane было все с точностью до наоборот (см. напр. http://www.osp.ru/text/302/179592/). Виновником аварии был как раз включенный контроль переполнения. По ошибке выполнялся опрос датчика, который в данный момент не мог давать правильные показания. Из-за этого произошло исключение в программе. Обработчик исключения переключил управление на резервный компьютер, который, естественно поднял тоже самое исключение. Парадокс, но если бы в данном случае не использовалась проверка переполнения ("небезопасный" язык) никакой аварии бы не было, так как программный модуль, опрашивавший датчик в данный момент не использовался.

Ответ на »сообщение 1147« (Geniepro)
___________________________
>>>Хотя интересно, если бы не отключили бы программный контроль переполнения - что дальше-то?
Ошибка не в отключении контроля переполнения.
Выбран не тот тип данных.
Контроль переполнения отключили для повышения быстродействия - в системах реального времени это может быть оправдано.
Тип данных выбрали с целью экономии памяти, создав возможность переполнения - вот этому оправдания нет.

Не надо выдавать ошибки проектирования за ошибки программирования.