H
напомни завтра, у меня есть еще одна книга, там еще более интересный подход к изложению материалу
👍
Size: a a a
2020 April 26
G
Ещё нашёл "Silberschatz - Operating System Concepts, 10th edition"
G
Белого шума поменьше, чем в Таненбауме, читать интереснее, книжка тоже толстая. Ещё в конце про построение виртуальных машин расскажут
DI
какая конечная цель? просто теории набраться?
G
Да
G
Ну ещё у меня далекоидущая цель нечто системное формально верифицировать, как вариант - игрушечную ОС
DI
туда можно спокойно на пару лет закопаться
G
В ОС/формальную верификацию?
G
Или в написание ОС
DI
в ОС
формальная верификация тоже интересная тема, но я в принципе малоприменимой ее к реальной жизни считаю
формальная верификация тоже интересная тема, но я в принципе малоприменимой ее к реальной жизни считаю
G
в ОС
формальная верификация тоже интересная тема, но я в принципе малоприменимой ее к реальной жизни считаю
формальная верификация тоже интересная тема, но я в принципе малоприменимой ее к реальной жизни считаю
http://annotationsforall.org/resources/links/GT-libc-experience-report.pdf
Может будет интересно почитать
Может будет интересно почитать
DI
у моего прошлого работодателя был целый отдел, который занимался формальной верификацией, ПО было сертифицировано по SIL 4, но внутри был лютый говнокод
при этом софт управлял железнодорожными поездами до скоростей 500 км/ч
так что да, красиво на бумаге
при этом софт управлял железнодорожными поездами до скоростей 500 км/ч
так что да, красиво на бумаге
ED
у моего прошлого работодателя был целый отдел, который занимался формальной верификацией, ПО было сертифицировано по SIL 4, но внутри был лютый говнокод
при этом софт управлял железнодорожными поездами до скоростей 500 км/ч
так что да, красиво на бумаге
при этом софт управлял железнодорожными поездами до скоростей 500 км/ч
так что да, красиво на бумаге
Были проблемы или верификация спасала?
DI
чем спасала? это не более, чем академическая идея
GK
у моего прошлого работодателя был целый отдел, который занимался формальной верификацией, ПО было сертифицировано по SIL 4, но внутри был лютый говнокод
при этом софт управлял железнодорожными поездами до скоростей 500 км/ч
так что да, красиво на бумаге
при этом софт управлял железнодорожными поездами до скоростей 500 км/ч
так что да, красиво на бумаге
Расскажите, а что из себя представляет процесс формальной верификации на SIL4? Какие инструменты используются? Требуются сертифицированные/проприетарные тулзы, одобренные каким-нибудь TUV, или допустимо использование FOSS (пруверы, какой-нибудь FramaC)?
Я не очень представляю, как вообще возможно формально верифицировать ПО для управляющих систем. Наверняка большая часть данных поступает извне (ioctl'и из ядра, по каналам связи из модулей УСО или других компонентов системы, etc.). Как же можно доказать корректность такой программы, если на её данные могут повлиять отказы оборудования или каналов связи?
Я не очень представляю, как вообще возможно формально верифицировать ПО для управляющих систем. Наверняка большая часть данных поступает извне (ioctl'и из ядра, по каналам связи из модулей УСО или других компонентов системы, etc.). Как же можно доказать корректность такой программы, если на её данные могут повлиять отказы оборудования или каналов связи?
DI
1) берем исходники системы
2) мульт баксов
3) подписываем контракт с европейским аудитором
4) ждем 6-12 месяцев
5) получаем сертификат
2) мульт баксов
3) подписываем контракт с европейским аудитором
4) ждем 6-12 месяцев
5) получаем сертификат
GK
А чем же целый отдел занимается? :)
DI
коммуникациями с аудитором
GK
Эх, ну понятно. У нас вот, когда сертифицировались на SIL2, спрашивали по всем пунктам — и использование статических анализаторов, и тесты, и стандарт кодирования, и т.д. Хотя я не в курсе, как реально это всё проверялось (но у нас всё это на самом деле используется).
ED
чем спасала? это не более, чем академическая идея
Так я и спрашиваю. В чём практическая составляющая?