Особенности программирования БВК АМС

[Вадим Семенов]

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

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

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

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

[bs]

Да уже обсудили пару страниц назад. Но интересно было бы узнать, что именно из разработок лабаратории надежности ПО применялось в работе над MSL.

[Not]

Да уже обсудили пару страниц назад. Но интересно было бы узнать, что именно из разработок лабаратории надежности ПО применялось в работе над MSL.

http://books.google.com/books?id=A_IBWF69WjMC&pg=PA16&lpg=PA16#v=onepage&q&f=false

[bs]

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

Я имел в виду более серьезные продукты лаборатории надежности.

[Not]

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

Я имел в виду более серьезные продукты лаборатории надежности.

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

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

На скептическое же отношение вы безусловно имеет право, благо это ничего не меняет в реальности  

[TAU]

Дело не безопасности...

ну-ну. спор можно с вами на этом заканчивать

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

почитайте литературу

Ада помоему сейчас не особо актуальна

Ада успешно используется в настоящее время. Насколько я понимаю, кроме прочего - при написании ПО МКС.

для очень высокоуровневых вещей можно создать спец. DSL с кодогенератором в Си

А можно - проблемно-ориентированный язык с прямой генерацией машинного кода   БЦВМ. Без промежуточной стадии.

[TAU]

Я спасаюсь, добиваясь сто процентного покрытия кода при тестировании. Это гарантирует...

1. Это невозможно. Покрытия кстати по какому из критериев? Покрытия операторов? Условий? Путей?
Для космического же аппарата, взаимодействующего в реальном времени с аппаратурой, протестировать все ситуации невозможно абсолютно.
2. Не гарантирует покрытие кода ничего...

[bs]

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

Спасибо за высокую оценку моих познавательных способностей

specification learning
- writing specs is time consuming
- often hard to come up with properties
- one approach is to use already generated log files to "get ideas"
- in the extreme case, specifications can be automatically generated from log files

Источник - Monitoring the Execution of Space Craft Flight Software, JPL

Моя вина лишь в том, что я более глубоко подошел к изучению данного вопроса, перелопатив и другие публикации. В итоге думал, что это тоже было в обсуждаемом документе. Ну тут уж простите меня - в 3:30 по Москве у меня дома тоже 3:30 :shock:

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

Давайте не будем фантазировать. Из документа, от которого плясали:

Testing is complicated by the fact that the programming team has little time for activities not related to development of new software, and hence cannot be disturbed too much by a testing effor. This prevents for example an approach based on new test-specific code instrumentation, be it automated or not.

Выделил, чтобы вам было легче разобраться. Про отсутствие времени на спецификации - это ваши фантазии. Не стоит так обобщать "testing effort", тем более, что следующей фразой дается конкретное пояснение.

На скептическое же отношение вы безусловно имеет право, благо это ничего не меняет в реальности  

Ну и на этом спасибо. Думаю очевидно, что мой скептицизм не безосновательный - обратите внимание на case study в документе, на который я сослался в начале.

[TAU]

В СССР было огромное количество бомжей

Ложь №1. Были возможно - как единичные исключения.

и нищих тоже хватало

Ложь №2. Нищета была редким, исключительным явлением при развитом социализме.

бомжи есть в любой стране, даже в Японии.
И дело тут СОВСЕМ не в уровне доходов

ну-ну. и нищим нравится бедствовать

Зачем вообще становиться миллионером нормальному человеку? Есть достойное качество жизни, уверенность в будущем своем и своих детей - зачем стремиться к миллиардам?

А зачем жить? Зачем работать? - Можно ведь бомжевать :?

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

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

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

[bs]

1. Это невозможно. Покрытия кстати по какому из критериев? Покрытия операторов? Условий? Путей?

Возможно. По всем указанным критериям.

Для космического же аппарата, взаимодействующего в реальном времени с аппаратурой, протестировать все ситуации невозможно абсолютно.

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

2. Не гарантирует покрытие кода ничего...

Гарантирует, что весь код работает именно так, как было задумано при его написании. Без сюрпризов и глупостей.

[TAU]

Java мало что дает для надежных систем

По крайней мере по сравнению с Си меньше возможностей залезть по произвольному адресу в память и что-нибудь испортить.

[TAU]

1. Это невозможно. Покрытия кстати по какому из критериев? Покрытия операторов? Условий? Путей?

Возможно. По всем указанным критериям

По всем ПУТЯМ вы покрываете программы? Настоящие? Из многих сотен тыщ строк? Простите, не верю.

2. Не гарантирует покрытие кода ничего...

Гарантирует, что весь код работает именно так, как было задумано при его написании. Без сюрпризов и глупостей

Не гарантирует.

[Not]

1. Это невозможно. Покрытия кстати по какому из критериев? Покрытия операторов? Условий? Путей?

Возможно. По всем указанным критериям

По всем ПУТЯМ вы покрываете программы? Настоящие? Из многих сотен тыщ строк? Простите, не верю.

2. Не гарантирует покрытие кода ничего...

Гарантирует, что весь код работает именно так, как было задумано при его написании. Без сюрпризов и глупостей

Не гарантирует.

Это вероятно наш Юниспейс с его "аккуратным" программированием.

bs, помните историю про ходжу Насреддина, падишаха, шахматную доску и зернышки риса?  

[bs]

По всем ПУТЯМ вы покрываете программы? Настоящие? Из многих сотен тыщ строк? Простите, не верю.

Да, вот такой я кудесник. Впрочем не я один.

Гарантирует, что весь код работает именно так, как было задумано при его написании. Без сюрпризов и глупостей

Не гарантирует.

Вы сейчас рассуждаете в срезе некоего асбтрактного "покрытия"? Я же его использовал в сочетании с тестированием. Представьте себе такой план тестирования, который заставляет отработать каждый линейный (детерминированный) участок кода минимум один раз и зафиксировать ожидаемый результат.

[TAU]

на них работает лаборатория надежности ПО (NASA) Почитать можно например в докладе сделанном по системе LogScope, в Гренобле, на конфе по методам runtime верификации, в 2009 году:
http://books.google.com/books?id=A_IBWF69WjMC&pg=PA16&lpg=PA16#v=onepage&q&f=false

Спасибо, Not!

[bs]

Это вероятно наш Юниспейс с его "аккуратным" программированием.

Ага, "обидеть художника может каждый"

bs, помните историю про ходжу Насреддина, падишаха, шахматную доску и зернышки риса?  

Увы не могу - тяжелое детство, знаете ли. Вместо сказок штудировал мануалы по БЭСМ.

P.S. Пардон, кажется из уроков математики про геометрическую прогрессию припоминаю. Тонко  :lol:

[Not]

Это вероятно наш Юниспейс с его "аккуратным" программированием.

Ага, "обидеть художника может каждый"

bs, помните историю про ходжу Насреддина, падишаха, шахматную доску и зернышки риса?  

Увы не могу - тяжелое детство, знаете ли. Вместо сказок штудировал мануалы по БЭСМ.

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

[TAU]

По всем ПУТЯМ вы покрываете программы? Настоящие? Из многих сотен тыщ строк? Простите, не верю.

Да, вот такой я кудесник. Впрочем не я один...
 Представьте себе такой план тестирования, который заставляет отработать каждый линейный (детерминированный) участок кода минимум один раз и зафиксировать ожидаемый результат.

Если каждый линейный участок - это первый критерий, покрытие операторов. Ничего особенного он не гарантирует.

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

К сожалению   (попробую найти литературу) и это не гарантирует отсутствия ошибок.

[bs]

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

Выходит проблема тех, кто не прогуливал дискретку в том, что теперь за ее деревьями они не видят леса?  :twisted:

[bs]

Если каждый линейный участок - это первый критерий, покрытие операторов. Ничего особенного он не гарантирует.

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

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

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

К сожалению   (попробую найти литературу) и это не гарантирует отсутствия ошибок.

Не тратьте времени - отсутствие ошибок не гарантирует ни что. Я уже объяснял, о какой гарантии разговор.