Formal Methods- based Technologies for Safeware COURSE PC1 EU Tempus project TEMPUS-UK-TEMPUS-JPCR National Safeware Engineering Network of Centres of Innovative Academia-Industry Handshaking (SAFEGUARD)

2 Course Summary Prerequisites Компьютерные системы Надежность компьютерных систем Системный анализ Object of Study Формальные методы разработки, верификации и анализа надежности и безопасности. Subject of Study Методы, технологии и инструментальные средства формальной разработки, верификации и анализа надежности и компьютерных систем и ПО критического применения. Aims Обзор методов и подходов к оценке и обеспечению надежности на основе риск-анализа, анализа вида, причин и последствий отказов и технологий формальной спецификации и верификации требований.

3 Course Structure Module 1. Modern formal methods for safeware engineering. Module 2. Model Checking. Module 3. Petri nets. Module 4. Integrated application of formal methods in critical systems development

4 Module 1. Advanced formal methods for safeware engineering Формальные методы разработки и спецификации требований (VDM, Event-B) Методы моделирования динамических дискретных систем (автоматы, сети Петри) Методы формальной верификации (Model Checking) Методы качественного анализа надежности и безопасности (HAZOP, FTA, FME(C)A) Методы количественной оценки (RBD, Марковские модели)

5 Module 2. Model Checking Логики и формальные исчисления Подход Model Checking Представление системы в виде структуры Крипке Представление требований с использованием LTL и CTL логик Алгоритмы верификации LTL и CTL Инструментарий Model Checking

6 Module 3. Сети Петри Виды сетей Петри (временная, стохастическая, функциональная, цветная, иерархическая, …) Верификация и анализ сетей Петри Инструментарий сетей Петри

7 Module 4. Integrated application of formal methods in critical systems development Invariant-based approach Композиция формальных методов Модели жизненного цикла при использовании формальных методов

8 Lab work Комплексный анализ и моделирование системы управления Lab 1. FTA, FME(C)A Lab 2. Event-B Lab 3. Model Checking Lab 4. Сети Петри

9 Lab 1. Анализ видов, причин и последствий отказов FME(C)A Цель: практическое использование метода анализа видов, причин и последствий отказов, а также оценка их критичности на примере многозвенных архитектур Web-сервисов Структура: ЛР состоит из двух частей: выявление и классификация отказов сервис- ориентированной системы качественный и количественный анализ критичности отказов

10 Lab 2. Оптимальный выбор методов и средств снижения критичности отказов Цель: овладение методикой анализа и оптимального выбора средств снижения критичности отказов Структура: анализ методов и средств снижения критичности (тяжести последствий, вероятности возникновения и/или времени неработоспособности) для СОА формулировка и решение оптимизационной задачи минимизации затрат на приобретение и внедрение методов и средств снижения критичности отказов

11 Lab 3. Построение и анализ деревьев отказов FTA Цель: изучение и практическое использование методики оценки надежности компьютерных систем на основе построения и анализа деревьев отказов FTA Структура: построение дерева отказов резервированной сервис- ориентированной архитектуры анализ и экспертная оценка вероятности наступления нижних событий дерева FTA, а также расчет вероятности ВНЗ – отказ в обслуживании

12 Lab 4. Разработка формальной спецификации Event-B компьютерной системы Цель: изучение методики разработки формальных спецификаций с использованием нотации Event-B Структура: получение навыков разработки формальных спецификаций Event-B с использованием платформы Rodin на учебном примере разработка формальной спецификации КС в соответствии с вариантом задания применение объектно-ориентированного подхода к разработке формальной спецификации Event-B

13 Учебно-методическое обеспечение Тарасюк О.М., Горбенко А.В. Формальные методы разработки критического программного обеспечения. Практикум / Учеб. пособие. под ред. Харченко В.С.– Харьков: Нац. аэрокосм. ун-т «Харьк. авиац. ин-т», – 116 с. Тарасюк О.М., Горбенко А.В. Формальные методы разработки критического программного обеспечения. Лекционный материал / Учеб. пособие. под ред. Харченко В.С.– Харьков: Нац. аэрокосм. ун-т «Харьк. авиац. ин-т», – 214 с.

14 Course Program