Формальная верификация: методы и приложения В. Кулямин Е. Корныхин

2/23 План Общие вопросы Модели Методы Инструменты и приложения

3/23 Потребности Определение Верификация – проверка корректности результатов некоторого этапа разработки по отношению к требованиям, сформулированным на предыдущих этапах Валидация Требования Проектные решения Система (Проектные решения)'

4/23 Формальная верификация Формальная проверка Должны быть представлены в виде формальных моделей Результаты Требования Соответствие между ними должно быть определено формально = реализация I = спецификация S

5/23 Формальное и неформальное Формально можно проверить только что-то формальное Реальные потребности и реальная система – неформальны Проверять адекватность самих формальных моделей нужно другими способами Потребности Спецификация Реализация Система

6/23 Объект верификации Программное и аппаратное обеспечение Формальная верификация Предистория Взлом шифраторов: E. F. Moore – 1956 Начало ПО: Floyd – 1967, Hoare – 1969 Развитие В основном АО: 1979–1995 Почему АО? Более простые примитивы + более однородная структура Стоимость ошибок значительно выше Повторно используется больше проектной информации Инженеры привычны к строгим ограничениям и точным описаниям

7/23 Общие требования Полезные системы достаточно сложны Есть несколько уровней детализации Верификация должна быть иерархической Верификация должна быть модульной

8/23 Абстракция и уточнение Абстракция упрощает модель Но уточнение должно обеспечить перенос результатов Виды абстракций Структурная абстракция Функциональная абстракция Абстракция данных Абстракция взаимодействий Временная абстракция

9/23 План Общие вопросы Модели Методы Инструменты и приложения

10/23 Основные виды моделей Виды формализмов Логико-алгебраическиеL Операционные (исполнимые)E Виды соответствий Выводимость I S ( I S ) L - L Моделирование I S E - L Симуляция I S E - E

11/23 Логико-алгебраические Алгебраические Реляционные алгебры (Codd ) Абстрактные типы данных (Zilles, Liskov – 1974) Алгебры процессов CSP (Hoare ) CCS (Milner ) ACP (Bergstra, Klop ) … Abstract State Machines (Гуревич ) Логические

12/23 Логические Исчисление высказываний Логика 1-го порядка по объектам типы λ по объектам по предикатам/типам λ по типам G, F, X, U A, E μ, ν λ -исчисление (Church – 1936) λ -исчисления высшего порядка (Girard – 1971) Логики высших порядков (Peirce – 1885) LTL (Prior ) интервалы явное время ITL (Moszkowski – 1983) CTL (Clarke, Emerson ) μ- исчисление (Pratt, Kozen – 1982) TPTL (Alur, Henzinger ) Hoare logic (Hoare )

13/23 Операционные FSM (Huffman ) CFSM (Brand, Zafiropulo ) взаимодействие данные разделение I/O IOA (Tuttle, Lynch – 1987) [ASM] EFSM (1973 ?) Сети Петри (Petri – 1962) ω-слова таймеры ω -автоматы (Buchi – 1960) гибридные (Alur, Henzinger ) временные (Alur, Dill ) LTS (1980 ?) [алгебры процессов] Машины (Тьюринг – 1936) Statecharts (Harel – 1987)

14/23 План Общие вопросы Модели Методы Инструменты и приложения

15/23 Методы верификации С полным моделированием – Спецификация и реализация известны С неполным моделированием – Известна только спецификация SI Система SI ? ?

16/23 Полное моделирование Дедуктивный анализ (theorem proving) Floyd – 1967 Проверка моделей (model checking) Clarke, Emerson – 1981 Проверка симуляции (simulation checking, equivalence checking) Moore – 1956 Символическое выполнение (symbolic execution) Topor, Burstall – 1972 Абстрактная интерпретация (abstract interpretation) Cousot – 1975

17/23 Неполное моделирование Формальное тестирование (formal conformance testing) Василевский – 1973 Hennessy, DeNicola – 1984 Верификационный мониторинг (runtime verification, passive testing) С 1970-х было много работ, в которых этот термин не употреблялся ~1999 – термин (Havelund, Rosu ?)

18/23 Распределение работ Model checking Model checkers Theorem proving Provers, SAT solvers Symbolic execution Formal conformance testing Runtime verificatio n Abstract interpretation Simulation checking

19/23 План Общие вопросы Модели Методы Инструменты и приложения

20/23 Дедуктивный анализ Неавтоматизированный анализ ASM Автоматизированный анализ ACL2 (Boyer, J. S. Moore – 1971) ~ 20 примеров, JVM (700 страниц) HOL (Gordon, 1988) ~ 30 примеров PVS (Owre, Rushby, Shankar – 1992) ~ 30 примеров Isabelle Coq

21/23 Проверка моделей и симуляции Model checkers SPIN (Holzman ~ 1982) SMV (McMillan et al.– 1994) и производные Murφ (Dill – 1992) UPPAAL (Larsen et al. – 1995) Equivalence checkers Verity (Kuehlmann et al. – 1995) Смешанные CADP (INRIA ~ 1990) ~ 50 примеров приложений

22/23 Что осталось? Тестирование TGV (1997) Gotcha (1999) Мониторинг TemporalRover (1995) ESC/Java 2 (2002) Java PathFinder (2004) Abstract interpretation ASTREE (2001)

23/23 Спасибо за внимание!

24/23 Дедуктивный анализ I Неавтоматизированный анализ: ASM Модель взаимодействия потоков Java (без исключений и пр.) Гуревич, Schulte, Wallace – 1999 Семантика JVM, Java и преобразования (без параллелизма) Borger, Schimd, Stark – 2001 Семантика SDL 2000 Eschbach, Glasser, Gotzhein, Prinz – 2000

25/23 Дедуктивный анализ II R. S. Boyer, J. S. Moore Ограниченная логика 1-го порядка + Applicative Common Lisp 1971 первый инструмент 1986 Nqthm 2001 ACL2 Ранние приложения Процессоры FM8501, FM8502 (1985); FM9001 (1997) Motorola MC68020 (1993), CAP DSP (100 страниц) AMD K5 (1995), Athlon (1997) IBM 4758 security model Rockwell JVM ( ) (700 страниц)

26/23 Дедуктивный анализ III HOL (Gordon – 1988) Основан на LCF (Milner – 1973) + higher-order logic + ML Несколько десятков работ по применению HOL Банки памяти (1996) Процессоры TAMARACK (1987) Viper (1987) Intel (Harrison, OLeary) ПО Web-сервер (1995) Протоколы Первый верифицированный коммерческий процессор После верификации найдена ошибка!

27/23 Дедуктивный анализ IV PVS (Owre, Rushby, Shankar – 1992) higher-order logic + язык, похожий на VDM Тоже несколько десятков приложений Протоколы Авионика + космос (NASA) ( ) Часть ядра ОС (1998) Управляющая система АЭС (1999) Процессоры AAMP5 (1995) VAMP FPU (2005)