iSAQB CPSA-A FM

Описание

Участие в курсе 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-решатели для проверки ограничений произвольных программных систем
• Применять абстрактную интерпретацию для статического прогнозирования динамического поведения