> Ну это можно дописать, Да? Ну покажите это. Может еще за разумные сроки и деньги? А то еще и с адекватными условиями лицензии? Странно, а чего вон тем не нравится что они из линуха это хотят.
> а вот что с верифицируемостью,
Типовой девайс с QNX, чего доброго еще и на стремном x86 гробе, с его SMM, ME, и прочим, а также довольно навороченым софтом - вот прямо так уж верифицирован? Позволю себе усомниться в этом. Формальную верификацию проходят только относительно тривиальные штуки. А чему ломаться в тупом тасксвичере? Проблема в том что это довольно бесполезно само по себе - а если это софтом обвесить, до нужной фичности, большой вопрос что там верифицировано в результате. Вон тот MCAS приложивший 2 самолета - номинально сертифицирован был, не мешало ему стремать пилотов прилично времени а парочку угробить совсем.
> надежностью, модульностью и всем прочим в линуксе?
С практической точки зрения у меня есть выводки систем где аптаймом год+ без сбоев вполне обычное дело. Вырубаются по powerloss либо для апдейтов, а не потому что сбой. Откуда я делаю вывод что в принципе наруленый со знанием дела линух в приемлимую надежность может, особенно если с резервированием. Но да, назвать это приключение гарантированным и безопасным? Ни в коем разе. Это здоровая сложная штука, активно развиваемая, где в новой версии могут повесить баг. В этом смысле имплементерам системы придется потр@хаться. Но они привычные.
Модульность? Линух это МОДУЛЬНЫЙ монолит. С вполне оформившимися подсистемами и прочим. И ядро в его минимальном и максимальном обвесе - это две довольно большие разницы. И разумеется для ответственных систем лучше быть ближе к первому чем второму из соображений надежности, стабильности, безопасности и attack surface если есть доступ по сети. Юзермод вообще не навязан, это лишь ядро и может быть любой который удобно в задаче. Некоторые фирмвари сделаны так что ядро пускает лишь 1 процесс, основную тушку фирмвары.
А "всего такого" в линуксе как раз хоть отбавляй, вот его довольно много кто и пытается до умений RTOS заодно еще догнать.
> За сколько можно дописать?
См. выше. ИМХО многие из топиков в принципе решаемы до адекватных на практике уровней. Ну вон Маск и ко не сыкуют в космос летать, комплексные гибридные мероприятия позволяют получить довольно надежные системы даже из неидеальных компонентов. А чрезмерное упование на идеальность компонентов обычно приводит к тому что ситуация когда это оказалось не так - не обрабатывается, или обрабатывается криво, а итог может быть достаточно печален.
