Верифікація ПЗ

Робоча програма навчальної дисципліни (відповідно до вимог МОН України).
Документ містить мету, результати навчання, структуру змісту, систему оцінювання та літературу.

Код курсу: КА-121-04

Кафедра: Кафедра мовного забезпечення

Кількість кредитів ECTS: 6 (180 годин)

Рівень: Бакалавр / Магістр

Базис: BTRON Coq Base Library & OCaml Oracles (btron.pro/b-system/theorems)

Мета та завдання

Вивчення методів формальної верифікації програмного забезпечення на прикладі повної механічної формалізації операційної системи BTRON (Cleanroom Reference) у Rocq/Coq 9.x з виконавчими моделями на OCaml 5.x. Курс охоплює 11 підсистем, 1 818 замкнених теорем, 21 641 рядок Coq, нуль аксіом і нуль admissions, з суворою 1:1 трасованістю до bare-metal C-реалізації.

Результати навчання

Структура курсу (модулі за підсистемами BTRON)

  1. Вступ. Методологія формалізації BTRON
    Cleanroom Reference, 1:1 трасованість до C, нуль аксіом, нуль admissions. Загальна статистика: 12 Coq-модулів, 13 OCaml-моделей, 1 818 теорем, 21 641 рядок Coq. Ресурс: btron.pro/b-system/theorems/index.html
  2. B-FS 64-Bit Allocator
    6 теорем. Масовий баланс на 64-бітних bitmap Allocation Group, просторова диз’юнктність, бієктивне кодування FID. Файли: bfs_allocator.{ml,v}
  3. B-FS Parameterized B+Tree
    6 теорем. Збереження відсортованості ключів, логарифмічна коректність пошуку, відсутність втрати ключів при розщепленні. Файли: bfs_btree.{ml,v}
  4. B-FS Volume V2 Journal
    39 теорем. Атомарність WAL-транзакцій, карантин мутацій при збої живлення, ідемпотентність replay журналу. Файли: bfs.{ml,v}
  5. Hypermedia & TAD DND
    61 теорема. Збереження DAG, conservation тіл при drag-and-drop, безвтратна серіалізація TAD. Файли: hypermedia_dnd.{ml,v}
  6. InterCore Streaming Protocol
    602 теореми. Mutex Elimination Theorem, non-blocking O(1) receive, нульова priority inversion. Файли: media_intercore.{ml,v}
  7. RTP Media Pipeline
    161 теорема. Zero-minting на пулах буферів, conservation кадрів, монотонність timestamp. Файли: media_rtp.{ml,v}
  8. SMP / AMP Concurrency
    69 теорем. Lock-free CAS progress, консистентність seqlock, безпека передачі периферії. Файли: media_smp.{ml,v}
  9. ITRON Microkernel Core
    815 теорем. Решітка станів задач, 140 FIFO-черг, детермінізм wait-release, zero-copy rendezvous. Файли: tron.{ml,v}
  10. OpenGL ES 1.1 / TinyGL
    18 теорем. EGL double buffering, обмеження глибини стека матриць, монотонність Z-буфера. Файли: opengl.{ml,v}
  11. GUI Compositor & Blitter
    15 теорем. Алгебра кліпінгу, накопичення damage, 2D memory safety. Файли: ui_compose.{ml,v}
  12. Window Manager & UI Shell
    14 теорем. Геометрія вкладок, унікальність фокусу, FIFO-черга подій. Файли: ui_elements.{ml,v}
  13. Hardware Drivers (VirtIO, DMA, HID)
    13 теорем. Монотонність черг VirtIO, безпека DMA stride, автомат станів клавіатури. Файли: drivers.{ml,v}
  14. Практична лабораторна
    Аналіз однієї підсистеми: читання Coq-теорії, відповідного OCaml-оракула та зіставлення з C-реалізацією.

Система оцінювання (100 балів)

Шкала: 90–100 — відмінно; 75–89 — добре; 60–74 — задовільно; <60 — незадовільно.

Рекомендована література

← Назад до каталогу курсів