forum.opennet.ru

Форум Разговоры, обсуждение новостей
Вариант для распечатки		Пред. тема \| След. тема
Режим отображения отдельной подветви беседы		[ Отслеживать ]

Оглавление

Организация Linux Foundation представила платформу для крити..., opennews (??), 05-Апр-16, (0) [смотреть все]

Только кода на сайте пока нет, одни планы , Аноним (-), 11:40 , 05-Апр-16, (1)
На базе ядра Linux Смешные Высоконадёжные системы создаются совсем иначе , Аноним (-), 12:05 , 05-Апр-16, (2) –29 //

Чё не так-то Майкрософт танцует Отдел маркетинга потеет Всё трендово , Andrey Mitrofanov (?), 12:08 , 05-Апр-16, (3) +13
Вы разбираетесь в данной теме Посоветуйте пожалуйста, что можно почитать по теме, Аноним (-), 12:08 , 05-Апр-16, (4) +6 //

Mathematically Verified Software Kernels Raising the Bar for High Assurance Im, Срп (?), 13:42 , 05-Апр-16, (13) //

И какие высоконадежные системы вы знаете, которые это используют , XoRe (ok), 17:30 , 05-Апр-16, (31) +3

а зачем знать - тут разрабатывать собираются, т е можно и с нуля попробовать, н, Очередной аноним (?), 08:30 , 06-Апр-16, (49) –2

золотые слова, XoRe (ok), 19:05 , 07-Апр-16, (59) +1

Всё это красивая болтовня А в реальных высоконадёжных системах полагаются на ду, Crazy Alex (ok), 19:03 , 05-Апр-16, (36) +5

да да, а операционки которые держатся на доказательствах , Аноним (-), 19:31 , 05-Апр-16, (38)

Во-первых, верифицируются микроядра и изолируемые компоненты Т е моноблочная 70, Вареник (?), 00:00 , 06-Апр-16, (43) +2

Ну и повсеместные проверки состояний, исполнений, результатов даже в ущерб произ, bOOster (ok), 06:14 , 13-Апр-16, (62) –1

Треп пустой Кто-то диссертацию защитил Кроме академической - никакой ценности , bOOster (ok), 06:09 , 13-Апр-16, (61)

ммм, да у вас будапешт голубчик, Аноним (-), 12:09 , 05-Апр-16, (5)
Естественно, в них обязательно должен быть крайний, конкретный которого потом ра, Аноним (-), 12:42 , 05-Апр-16, (8)
Угу Слишком сложное для сабжевой задачи В самом ядре все баги отловить нереаль, Анонимизатор (?), 12:43 , 05-Апр-16, (9)
Не надо нас учить своим очистительным клизмам А ядро в любой момент можно будет, Аноним (-), 14:27 , 05-Апр-16, (15) //

На куда, простите , Michael Shigorin (ok), 14:28 , 05-Апр-16, (17) +2 //

QNX 716 kju 720 716 603 n 712 603 ks or B 712 kju 720 n 754, Andrey Mitrofanov (?), 14:31 , 05-Апр-16, (18)

Так это другие буковки PS да и с заменой юзерспейса лёгким взмахом ре рук, Michael Shigorin (ok), 15:04 , 05-Апр-16, (19) +2

Ты Майкл просто старый хрыч Смотри как нынче супер надёжные проекты делаются , _ (??), 16:26 , 05-Апр-16, (25) +2

ЙОШКЕН КОТ 11 Ну как должно будучи на PHP написано, так и работает , RomanCh (ok), 16:53 , 05-Апр-16, (28) +1
В противовес http www theregister co uk 2013 06 19 nuke_plants_to_keep_pdp11_u, Аноним (-), 17:34 , 05-Апр-16, (32)
Ага, точно работает Только ответ, не тот что нужно , невидимка (?), 04:29 , 06-Апр-16, (47)

Всё познаётся в сравнении Помните Code Red , Michael Shigorin (ok), 14:28 , 05-Апр-16, (16) //

я даже застал всю это красоту нимду тоже в действии, ИТ пачками выдергивало се, none_first (ok), 17:50 , 05-Апр-16, (34) +1 //

Ну человек наверняка имел-то в виду совсем не винду, а намёкивал на специализиро, Michael Shigorin (ok), 19:40 , 05-Апр-16, (39)

При всём уважении к вашей точке зрения, подавляющая часть IT-культуры - таки про, nbw (ok), 09:46 , 06-Апр-16, (51) +1

Это так а если копнуть чуточку глубже, то недавно пробегал очередной top10 и то, Michael Shigorin (ok), 17:32 , 06-Апр-16, (57) –1

Ага, ставится отстой типа windows nt или qnx Только тперь это Г даже за откаты , Sfinx (ok), 15:58 , 05-Апр-16, (24) +1 //

Я в 10 лет тоже верил, что скоро все хорошие люди соединятся в один большой, пла, _ (??), 16:39 , 05-Апр-16, (27) +1 //

Хорошие таки валили из СССР со страшной силой , Аноним (-), 00:32 , 06-Апр-16, (45) –2

В Израиль, полы подметать , nbw (ok), 09:49 , 06-Апр-16, (52) +1

Какие спецы - такая и работа Это только в СССР-ии и России тебя будут держать, Василий Теркин (?), 10:28 , 06-Апр-16, (54) +1

Поспрашивайте у таких, к чему они пришли, свалив Познавательно , Michael Shigorin (ok), 17:29 , 06-Апр-16, (56)

google, yahoo сейчас конечно не фонтан , а один не сознаётся так как в М , не п, Sarmat (?), 12:41 , 13-Апр-16, (64)

Иксперды по высоконадёжным системам подтянулись, Нанобот (ok), 18:08 , 05-Апр-16, (35) +3 //

Не суди по себе - лучше выскажи своё скромное мнение , Аноним (-), 00:54 , 06-Апр-16, (46)

Например, платформа CIP может быть использована для управления генерацией и пер, Аноним (6), 12:21 , 05-Апр-16, (6) +1 //

А вы не в курсе, под какой ОС современные SCADA в большинстве своем , Аноним (-), 12:58 , 05-Апр-16, (11) +2 //

Лучше выбери незнание и крепкий сон - , _ (??), 16:28 , 05-Апр-16, (26) +5
это те, кот по ч-л желанию могут отправить турбину в космос , none_first (ok), 17:47 , 05-Апр-16, (33) +1

То есть по планам это будет лучшее творение ближайшие 60 лет, Аноним (-), 12:28 , 05-Апр-16, (7) //

Наконец-то сделают хоть что-то цивильное , Анонимизатор (?), 12:44 , 05-Апр-16, (10) //

Анонсировали коммунизм Верифицировать моноядро, даже с минимальным набором дров, Вареник (?), 00:08 , 06-Апр-16, (44) //

А зачем это делать Есть показатели вероятности, есть теория надежности Ловить , Василий Теркин (?), 10:32 , 06-Апр-16, (55)

Действительно, зачем производители авто, самолетов, медоборудования парятся с ве, Вареник (?), 18:13 , 06-Апр-16, (58) +1

Верифицируют компоненты для того чтобы в любом случае компоненты соответствовали, bOOster (ok), 06:26 , 13-Апр-16, (63)

Когда нормальный десктоп представят Это тоже критически важно , Аноним (-), 15:42 , 05-Апр-16, (22) +2
Еще один или просто очередной громкий анонс И вновь никакого кода Может, кон, SpiritOfStallman (ok), 15:52 , 05-Апр-16, (23) +1 //

Трудно сказать Hitachi и Siemens опыт в таких проектах точно имеют, остальные _, _ (??), 17:23 , 05-Апр-16, (30)
Какой-тaкoй кoд-шмoд, шановный - люди cypьeзные лопатами не махають Эта месага н, fail (?), 21:39 , 05-Апр-16, (41) +1

Сименс и стандарты Не смешите мои тапочки, они для каждого стандарта умудряются, anonymous (??), 21:34 , 05-Апр-16, (40) +2
Надежное моноядро для критических компонентов Кого они хотят этим купить, ког, Вареник (?), 23:45 , 05-Апр-16, (42)
Зашёл я на сайт этой CIPы Там же одни лозунги Ни кода, ни скриншотов, ни даже, robux (ok), 08:14 , 06-Апр-16, (48)
Лет 10 я слышу одни и теже лозунги от Линуксоидов, в разных проектах, а в высоко, bOOster (ok), 06:06 , 13-Апр-16, (60) –1

Сообщения [Сортировка по времени | RSS]

13. "Например:" +/–

Сообщение от Срп (?), 05-Апр-16, 13:42

"Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations"
https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf

Ответить | Правка | Наверх | Cообщить модератору

31. "Например:" +3 +/–

Сообщение от XoRe (ok), 05-Апр-16, 17:30

> "Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations"
> https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf
И какие высоконадежные системы вы знаете, которые это используют?

Ответить | Правка | Наверх | Cообщить модератору

49. "Например:" –2 +/–

Сообщение от Очередной аноним (?), 06-Апр-16, 08:30

а зачем знать - тут разрабатывать собираются, т.е. можно и с нуля попробовать, нахватавшись лучших идей из имеющегося. Еще про микроядра и всякие QNX'ы можно холивар развести. Особенно в свете того что раньше в мире (не знаю как сейчас) QNX крепко использовался в управлении систем нефте/химической промышленности и др. сложных и опасных производствах (у нас на металлургическом заводе когда-то использовалось, еще QNX4)

Ответить | Правка | Наверх | Cообщить модератору

59. "Например:" +1 +/–

Сообщение от XoRe (ok), 07-Апр-16, 19:05

> а зачем знать
золотые слова

Ответить | Правка | Наверх | Cообщить модератору

36. "Например:" +5 +/–

Сообщение от Crazy Alex (ok), 05-Апр-16, 19:03

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

Ответить | Правка | К родителю #13 | Наверх | Cообщить модератору

38. "Например:" +/–

Сообщение от Аноним (-), 05-Апр-16, 19:31

да да, а операционки которые держатся на доказательствах ?

Ответить | Правка | Наверх | Cообщить модератору

43. "Например:" +2 +/–

Сообщение от Вареник (?), 06-Апр-16, 00:00

Во-первых, верифицируются микроядра и изолируемые компоненты.
Т.е. моноблочная 70-мегабайтная простыня имени Линуса пролетает автоматом. В ней даже обычный статистический анализатор кучу всего находит.
Во-вторых, ОС - это вещь в себе, не реализующая критически важной прикладухи. ОС может быть математически верифицирована, а в прикладной части вы имеете деградирующие компоненты, горячие частицы (даже fault tolerant архитектуры имеют пределы, может "удачно" завалиться), глюки и погрешности сенсоров, абстрактность и упрощение мобели регулируемой системы.
Если у вас в руках надежный безотказный (математически верифицированный) нож - это не значит что он вас гарантированно спасет в джунглях (открытая система - реальный мир).

Ответить | Правка | Наверх | Cообщить модератору

62. "Например:" –1 +/–

Сообщение от bOOster (ok), 13-Апр-16, 06:14

> Всё это красивая болтовня. А в реальных высоконадёжных системах полагаются на дублирование
> компонент, работающих на разных принципах, и на проектирование, при октором в
> случае отказа чего-либо остальныевы элементы выходят в более-менее безопасное состояние.
Ну и повсеместные проверки состояний, исполнений, результатов даже в ущерб производительности. Линуксовый же подход и их "гордость" в 99% случаев выпиливание данных проверок в угоду производительности со словами - да нах они нужны? Все равно в 99%!!! случаев не работают.
facepalm

Ответить | Правка | К родителю #36 | Наверх | Cообщить модератору

61. "Например:" +/–

Сообщение от bOOster (ok), 13-Апр-16, 06:09

Треп пустой. Кто-то диссертацию защитил. Кроме академической - никакой ценности не имеет.

Ответить | Правка | К родителю #13 | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема

Партнёры:

Хостинг:

Закладки на сайте
Проследить за страницей

Created 1996-2024 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру


	13. "Например:"	+/–
	Сообщение от Срп (?), 05-Апр-16, 13:42
	"Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations" https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf
	Ответить \| Правка \| Наверх \| Cообщить модератору


	31. "Например:"	+3 +/–
	Сообщение от XoRe (ok), 05-Апр-16, 17:30
	> "Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations" > https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf И какие высоконадежные системы вы знаете, которые это используют?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	49. "Например:"	–2 +/–
	Сообщение от Очередной аноним (?), 06-Апр-16, 08:30
	а зачем знать - тут разрабатывать собираются, т.е. можно и с нуля попробовать, нахватавшись лучших идей из имеющегося. Еще про микроядра и всякие QNX'ы можно холивар развести. Особенно в свете того что раньше в мире (не знаю как сейчас) QNX крепко использовался в управлении систем нефте/химической промышленности и др. сложных и опасных производствах (у нас на металлургическом заводе когда-то использовалось, еще QNX4)
	Ответить \| Правка \| Наверх \| Cообщить модератору


	59. "Например:"	+1 +/–
	Сообщение от XoRe (ok), 07-Апр-16, 19:05
	> а зачем знать золотые слова
	Ответить \| Правка \| Наверх \| Cообщить модератору


	36. "Например:"	+5 +/–
	Сообщение от Crazy Alex (ok), 05-Апр-16, 19:03
	Всё это красивая болтовня. А в реальных высоконадёжных системах полагаются на дублирование компонент, работающих на разных принципах, и на проектирование, при октором в случае отказа чего-либо остальныевы элементы выходят в более-менее безопасное состояние. А математические доказательства корректности, во-первых, проходят только для крайне простого кода, а во-вторых держатся на предположении о корректности специфиакации.
	Ответить \| Правка \| К родителю #13 \| Наверх \| Cообщить модератору


	38. "Например:"	+/–
	Сообщение от Аноним (-), 05-Апр-16, 19:31
	да да, а операционки которые держатся на доказательствах ?
	Ответить \| Правка \| Наверх \| Cообщить модератору


	43. "Например:"	+2 +/–
	Сообщение от Вареник (?), 06-Апр-16, 00:00
	Во-первых, верифицируются микроядра и изолируемые компоненты. Т.е. моноблочная 70-мегабайтная простыня имени Линуса пролетает автоматом. В ней даже обычный статистический анализатор кучу всего находит. Во-вторых, ОС - это вещь в себе, не реализующая критически важной прикладухи. ОС может быть математически верифицирована, а в прикладной части вы имеете деградирующие компоненты, горячие частицы (даже fault tolerant архитектуры имеют пределы, может "удачно" завалиться), глюки и погрешности сенсоров, абстрактность и упрощение мобели регулируемой системы. Если у вас в руках надежный безотказный (математически верифицированный) нож - это не значит что он вас гарантированно спасет в джунглях (открытая система - реальный мир).
	Ответить \| Правка \| Наверх \| Cообщить модератору


	62. "Например:"	–1 +/–
	Сообщение от bOOster (ok), 13-Апр-16, 06:14
	> Всё это красивая болтовня. А в реальных высоконадёжных системах полагаются на дублирование > компонент, работающих на разных принципах, и на проектирование, при октором в > случае отказа чего-либо остальныевы элементы выходят в более-менее безопасное состояние. Ну и повсеместные проверки состояний, исполнений, результатов даже в ущерб производительности. Линуксовый же подход и их "гордость" в 99% случаев выпиливание данных проверок в угоду производительности со словами - да нах они нужны? Все равно в 99%!!! случаев не работают. facepalm
	Ответить \| Правка \| К родителю #36 \| Наверх \| Cообщить модератору


	61. "Например:"	+/–
	Сообщение от bOOster (ok), 13-Апр-16, 06:09
	Треп пустой. Кто-то диссертацию защитил. Кроме академической - никакой ценности не имеет.
	Ответить \| Правка \| К родителю #13 \| Наверх \| Cообщить модератору