Real-time и не-real-time - в одном флаконе или раздельно? Опции

[Kabdim]

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

[AlexandrY]

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

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

[Kabdim]

Саму спецификацию ребята не показали.

Вы не смогли зайти на гитхаб?

[syoma]

Можно было бы попытаться дать гарантию безошибочности (100 %, или хотябы 9.999 ), если бы весь "продукт" был свой, доморощенный.
до последнего бита и проводка.
1. Читаем errata на ВСЕ что используется из комплекующих, и пытаемся ЭТО предусмотреть в коде.
2. Читаем errata, и "мечтаем", что там моежт появиться в следующей ревизии (но глючек уже в этой).
3. Неоткрытая элементарная частица из Вселенной влетает в ГЛАВНЫЙ РЕГИСТР системы и все рушится.
(одна надежда, что по вероятности ОНО не затронет WD).

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

[AlexandrY]

Вы не смогли зайти на гитхаб?

Имеете какое-то отношение к этому проекту или просто купились на фразу - "все формально проверено"?
Только взглянул на спецификацию и чуть крыша не съехала.
Вы напрмер можете человеческим языком объяснить что такое higher-order logic?
Чем эти сектанты там вообще занимаются?

[Kabdim]

Если осилите HoL, то скорее всего вам не потребуются объяснения. Эти "сектанты" называются прикладными математиками.

[AlexandrY]

Если осилите HoL, то скорее всего вам не потребуются объяснения.

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

А реальному программису надо хотя бы узнать как в действительности работает API.
Само изучение API превращается в исследование. Так же с аппаратными ресурсами.
"Прикладные математики" здесь отдыхают.

[Kabdim]

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

[mantech]

Можно было бы попытаться дать гарантию безошибочности (100 %, или хотябы 9.999 ), если бы весь "продукт" был свой, доморощенный.
до последнего бита и проводка.

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

Люди даже в "hellо world" умудряются ошибки вывода в терминал делать...

[Студент заборстр...]

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

Потому что "Задача покрытия" относится к задачам NP-класса. Поэтому в общем виде не решается за обозримое время

[AlexandrY]

Потому что "Задача покрытия" относится к задачам NP-класса. Поэтому в общем виде не решается за обозримое время

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

[Kabdim]

Ну хватит уже фантазировать о том что не осилили. Это уже какое-то болезненное себялюбие - высасывание контраргументов из фантазий.

Потому что "Задача покрытия" относится к задачам NP-класса. Поэтому в общем виде не решается за обозримое время

Ну и вы я так понимаю статьи не читали, но мнение имеете?

[AlexandrY]

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

Вы сами-то докажите что что-то поняли?
От вас только ссылки. Такие мы и сами вам можем тонну отгрузить.

[Kabdim]

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

[AlexandrY]

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

Не то чтобы авторы дураки, но скорее не ориентируются в теме те кто дает ссылки на такие работы.
Скажем можете ли вы объяснить зачем нам вот такое доказательство - confidentiality and intransitive non-interference proofs?
Т.е. как его применить программисту embedded шлюза между Ethernet и SPI ?