Projekt ELISA (Enabling Linux In Safety Applications) (diskuse)

[snajpa]

<3

Critical hit. Tak strasne se mi to hodi do kramu, az ukapava slzicka stesti.

[BFU]

Na githubu maji README, co vic si prat ...

[snajpa]

V pohode, to prijde; ja uz jsem jasal, kdyz se objevily prvni zminky o formalni verifikaci task modelu Linuxu, jakykoliv dalsi potvrzeni tim smerem se hodi, vysledky stejne potrebuju realne az tak za rok, ted jde jenom o volbu technologii a Linux evidentne nebude spatny napad postupne i pro critical control loopy...

[pirated_byte]

Me to pripada jako spatny napad. Mozna verifikuji nejaky formalni model, ale jeho spravnou implementaci uz asi tezko. Linux je prilis monstrozni.

[trekker.dk]

Tipnul bych si, že začnou tím, že vysekají tolik kódu, kolik jenom půjde...

[sigma]

Já tedy moc nechápu, na jaký segment aplikací s tím míří. Orientuji se a mám nějaké zkušenosti se safety normami pro průmyslové aplikace (IEC 61508) a energetiku (IEC 61513). Pro jakékoliv bezpečnostně relevantní systémy v těchto segmentech mi přijde použití Linuxu s ohledem na formální požadavky celkem unreal.

To neznamená, že se Linux pro "critical control loopy" nepoužívá. Např. takový Siemens Sinumerik je postaven na RT Linuxu na Intel CPU. Je to software pro řízení obráběcích strojů, kde chyba může způsobit zničení obrobku v hodnotě milionů USD (v případě velkých strojů, které dělá třeba Škoda MT). Ale na tohle není potřeba certifikace podle nějaké normy, to je otázka spolehlivosti. Otázky funkční bezpečnosti - zjednodušeně aby to někoho nezabilo - se musí řešit úplně jinak.

Při uvažování o použití Linuxu mi formální verifikace task modelu přijde jako sice důležitá, ale v celkovém kontextu celkem okrajová věc. Protože těch míst, kde to celé může selhat je tam mnohem více, a vstupuje do toho hodně také HW platforma, to vám ale asi nemusím psát. Takže nějaký takovýhle projekt mi zatím přijde spíš jako podklad pro management, že je možné ten Linux brát vážně. Podobně jako ze supportu Linuxu dokáže žít Wind River, který za vás řeší QA proces, maintenance a hlavně také legal aspekty konkrétní distribuce na konkrétním HW podle nějaké certifikované metodiky. Toje v tomto prostředí ta největší hodnota.

[snajpa]

Jsme v absolutni shode, presne tak - ted tyhle zpravy potrebuju presne, spis pro sales pitch, proc neni potreba se Linuxu bat a ze i ostatni, velci, hraci jdou timhle smerem.

[snajpa]

Jinak tipoval bych, ze ten nejvetsi drive je smerem automotive, vcelku se pocita s virtualizovanymi ridicimi jednotkami bezici na nejakem centralnim cipu s nejakou kombinaci Cortex-A + Cortex-R.

Mne osobne prijde hodne zajimavy dostat Linuxovou kontejnerizaci do stavu, kdy by se dalo control loopy ridit z kontejneru (a centralnimi knoby jim nastavovat resource/realtime management). Akorat teda, jestli je nejaka verifikace task modelu Linuxu behem na delsi trat, dostat kontejnery do industrial ready stavu je temer mission impossible, napr. memory control group je totalni fail...

[Sid1]

Ono v podstate staci si pozriet ako je urobena verifikacia seL4 a ze je z toho vytiahnuty IO. Takze verifikacia linuxu je cisto iba tak odrazka do powerpointu co pekne vyzera a ako sa vravi slubom nic nepokazis

[jiwopene]

s/Clem/Cílem/

[Ladislav Hagara]

Dík. Opraveno.