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

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

В правильном языке компилятору нельзя заткнуть рот приведением типа. Да и приведения типа как такового там не должно быть.

Да вы маньяк   Вы сейчас говорили о каком то реальном языке, или о желаемом?

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

И как вы, например, будете приводить вещественыый тип к целочисленному и наоборот?

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

[Unispace]

У вас проблемы в личной жизни, на работе, в проекте ? Не отчаивайтесь! Отправьте байт-код 01001010 на адрес "Компилятор" (услуга платная, 1.5 млрд руб, с учетом НДС), и ваша проблема будет решена, о чем вы получите смс-уведомление  

[zyxman]

Тут проблема, что нужно будет заранее просчитать все допустимые для ширины типа диапазоны входных значений. И это ОЧЕНЬ рутинный трудоемкий процесс, который тоже может принести ошибок.

Все вполне считается компилятором. Но думать и писать действительно надо больше, нежли программирование "абы как". Это плата за надежное ПО. Альтернатива - ПО с багами.

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

Например, для y=x*x тип X должен быть более узким чем тип y. И если для такого простого случая можно действительно компилятором автоматически посчитать диапазоны, то для автоматизации более сложных случаев нужно либо ИИ либо тестирование.

Тестирование не гарантирует отсутсвие багов.Оно гарантирует их наличие

Не понятно значение данной фразы в этом контексте.

Ну а даже если у вас этот самый IF поймал выход за пределы диапазона, что вы будете делать?

Реагировать в зависимости от задачи. Условный пример. Допустим, гироскоп выдает значение угла поворота от 0 до 360 градусов. Если мы получили значение вне этого диапазона, значит он неисправен. Нужно пометить его как неисправный и работать дальше на оставщихся гироскопах. Если это невозможно, перейти на ориентацию на звездных датчиках. Если опять невозможно то перейти в закрутку на солнце. Ну вобщем идея понятна, надеюсь

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

[avp]

Я знаю, что эрланг нативно поддерживает ASN.1
Но, увы, в реальных протоколах связи с КА он не применяется. И я не знаю почему. Поэтому разбирать пакеты всё равно придётся ручками.

Насколько я понимаю, ASN.1 это стандарт описания протоколов, по сути то-же что BNF.
Не применяется вероятно потому что КА проектируют люди, которые не хотят далеко уходить от Си, и на Си все привыкли к BNF.

Да, это стандарт формальных описаний структур данных. Позволяет автоматизировать сериализация/десериализация.

Наезд на Си тут несправедлив, т.к. этот стандарт вырос именно из Си, и существует масса компиляторов из  ASN.1  в Си. Причина тут опять скорее всего в специфике КА, когда нужен полный контроль на данными на всех уровнях иерархии.

Не обязательно фарш и не обязательно Си. Может быть и ТОЛЬКО Эрланг,  и Паскаль, и Модула, да хоть Фортран.

Это возможно только на серийной платформе. Если перед вами голая специфическая железка, то трудозатраты на поднятие инфраструктуры для ЯВУ будут слишком велики. Только если размазать эти затраты по многим проектам.

[TAU]

пока известен только один метод верификации - фактически переборный

На сегодня известны следующие подходы к верификации ПО:

1. Группа формальных методов
2. Инспекции кода (взаимный просмотр, экспертный метод)
3. Группа методов, связанных с тестированием (исполнением)

Причем в данных группах имеются различные варианты конкретных методов, например, к формальным относят, кроме методов дедуктивных выводов о корректности программ, метод проверки моделей (model checking), а исполнение может являться, к примеру, символическим.

[dmdimon]

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

[Not]

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

Прижилась. В виде троирования (резервирования).

[dmdimon]

а что-то не столь тривиальное? типа роевых систем/нейросетей/кластерных систем? Организация ECC озу в райд6 хотя-бы с подключением из резерва по необходимости? То-же для процессоров?

[Not]

а что-то не столь тривиальное? типа роевых систем/нейросетей/кластерных систем? Организация ECC озу в райд6 хотя-бы с подключением из резерва по необходимости? То-же для процессоров?

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

Университетские же разработки безусловно есть.

[dmdimon]

понял. А негде глянуть на эти разработки?

[Not]

понял. А негде глянуть на эти разработки?

Почитайте публикации, например, вот этого гражданина

http://www.csail.mit.edu/user/816

Prof. Williams' research concentrates on model-based autonomy -- the creation of long-lived autonomous systems that are able to explore, command, diagnose and repair them selves using fast, commonsense reasoning.

[dmdimon]

Спасибо!