iSAQB® CPSA-A - Формальні методи (курс)

Опис

Участь у курсі iSAQB® CPSA-A Formal Methods (FM) дає учасникам 20 балів за технічну компетентність (TC) та 10 балів за методологічну компетентність (MC) у межах 70 балів, необхідних для допуску до іспиту iSAQB CPSA-A з Brightest. Важливо пам’ятати, що в межах 70 балів, необхідних для складання іспиту iSAQB CPSA-A з Brightest, потрібно набрати щонайменше десять балів за компетентності в кожній із таких областей: 

• Технічна компетентність (TC)
• Методологічна компетентність (MC)
• Комунікативна компетентність (CC)

Акредитоване навчання iSAQB® FM - Formal Methods (CPSA-A) базується на актуальній навчальній програмі iSAQB®:

Частина 1 - Логіка

• Знати базову структуру пропозиційної логіки
• Знати базову структуру логіки предикатів/логіки першого порядку
• Знати базову структуру темпоральних операторів
• Розуміти основні поняття логічного числення
• Розуміти різницю між інтуїціоністською та класичною логікою

Частина 2 -  Специфікація та реалізація

• Розрізняти поняття специфікації
• Розуміти, що специфікації можуть стосуватися різних типів компонентів
• Розуміти, що специфікації можуть стосуватися різних характеристик якості
• Розрізняти формальні специфікації та інші типи специфікацій
• Знати відмінні властивості щонайменше трьох різних мов специфікації
• Розуміти поняття уточнення (refinement)

Частина 3 - Формальні методи та процес розробки

• Визначати сфери застосування формальних методів
• Знати відповідні характеристики якості, які вказують на доцільність використання формальних методів
• Розуміти значення точної специфікації
• Знати компроміси між різними формальними методами
• Поступово впроваджувати формальні методи
• Вибирати відповідні формальні методи
• Оцінювати архітектуру за допомогою формальних методів

Частина 4 - Інструменти

• Застосовувати тестування на основі властивостей (property-based testing)
• Розуміти роль систем типів
• Застосовувати перевірку моделей (model checking) для верифікації властивостей автоматів
• Застосовувати асистенти доказів для верифікації властивостей довільних програмних систем
• Застосовувати SMT-розв’язувачі для перевірки обмежень довільних програмних систем
• Застосовувати абстрактну інтерпретацію для статичного прогнозування динамічної поведінки