caxapa.ru :: seL4. seL4's implementation is formally (mathematically) proved correct (bug-free) against its specification -> seL4-Based Project -->

Evgeny_CD, Архитектор (12.02.2016 00:19 - 00:39, просмотров: 424) ответил Evgeny_CD на L4 microkernel family -> Кто-нибудь щупал это дело с практической точки зрения?

seL4. seL4's implementation is formally (mathematically) proved correct (bug-free) against its specification -> seL4-Based Project --> http://sel4.systems/Info/GettingStarted/
https://sel4.systems
Что интересно, seL4 owned by General Dynamics C4 Systems - нехилая такая ВПКшная компашка в Штатах. На GitHub под GPL 2.0 лежит. Подборка документов вложена.

4977a415.pdf hotos07-sel4.pdf seL4-brochure.pdf sel4.pdf GD-NICTA-whitepaper.pdf p133-elphinstone.pdf

Ответить

- Кто понимает в теме, вдруг кто быстро разберется - как именно они верифицируют код на соответствие спецификациям? - Evgeny_CD(12.02.2016 01:45)
  - Д.ARMоед - подскажи, плиз.... - Evgeny_CD(12.02.2016 01:46)
    - в режиме прохожего: система подвергается функциональной декомпозиции -> записывается на хаскеле. далее TimeZoneDefault(481 знак., 12.02.2016 13:05, )
      - Спасибо! Да, у них там есть хаскельный код в репозитории, и какой-то кодогенаратор на их собственном DSL. Все это весьма близко к подходам, которые я здесь много лет ковыряю. А именно - программист пишет не "сразу в С", а в некий DSL, который, в Evgeny_CD(147 знак., 12.02.2016 16:28)
        
        последний тезис упирается в понятие "обратимых вычислений", которые существуют не для всех классов алгебр. для алгебры чёрча - формально не существуют :) TimeZoneDefault(801 знак., 12.02.2016 17:18, )
        
        Спасибо! "частный случай полупрямого произведения групп." Да, это надо переварить.... - Evgeny_CD(12.02.2016 17:52)
        
        переварить лучше то, что фичи, представляемые в виде "proved" решений для сегодняшних камней на самом деле таковыми не являются в силу фундаментальных причин. - TimeZoneDefault(12.02.2016 19:46, )
        
        "Не нее-шь, не продаш" :) - Evgeny_CD(12.02.2016 20:58)
        
        пральна. осталось понять, как нае..ть всех так, чтобы им это понравилось :)) - TimeZoneDefault(12.02.2016 21:39, )
- Еще про нее же. В конце страницы шикарная подборка документов и през. - Evgeny_CD(12.02.2016 00:37, ссылка)
- Ой. eChronos project builds and formally verifies, a small, versatile, high-assurance real-time operating system (OS) for embedded micro-controllers -> •Formal functional specification (completed) Какой-то разрыв шаблона. Evgeny_CD(39 знак., 12.02.2016 00:34, ссылка)
  - Не понял, что удивляет-то? - LightElf(12.02.2016 10:56)
- Довольно интересен список поддерживаемого харда ->, есть на редкость интересные платы --> BD-SL-i.MX6 ◦The Sabre Lite i.mx6 board. - Evgeny_CD(12.02.2016 00:28, ссылка, ссылка)

Средства и методы разработки