Верификация программ посредством их параметризованного тестирования специализаторами на базе моделей этих программ, реализация верификатора для языка программирования Java. Институт Программных Систем РАН Институт Прикладной Математики им. М.В. Келдыша РАН Университет г. Переславля Сергей Михайлович Абрамов Институт Программных Систем РАН

2Актуальность Верификация автоматическая проверка свойств программ с целью повышения их надёжности: –Корректность программ сложного поведения, разработанных коллективами разработчиков. –Программы на языке широкого использования Java. –Сокращение больших материальных рисков (даже при верификации небольших программ, управляющих космическими аппаратами). Все данные задачи являются актуальными для развития теории и практики IT

3 Цели исследований Разработка технологии верификации управляющих программ со сложным поведением на базе моделей этих программ. –Технология должна быть основана на изучении процесса верификации как параметризованного тестирования. –Технология должна базироваться на автоматической специализации программ. Реализация прототипа верификатора для языка программирования Java. Использование результатов теоретических исследований и практической реализации в образовательном процессе.

4 Задачи исследований на 2007 г. Разработка основных принципов технологии верификации, основанной на изучении процесса верификации как параметризованного тестирования: –технологии построения параметризованных моделей программ, посредством их специализации по контексту использования; –технологии автоматической верификации моделей программ посредством специализации методами суперкомпиляции; –апробация разработанных принципов технологии на верификации различных программных моделей. Разработка методов построения тестовых гипотез, указывающих на ошибки в программах. На основе разработанных технологий начата разработка прототипа верификатора для программ, написанных на Java.

5 Традиционная верификация на базе моделей Проверяемая программа Модель программы Критические свойства Спецификация Верификатор Контрпример Верно исправления моделирование формализация

6 Тестирование Проверяемая программа Критические свойства спецификация- предикат Исполнение Контрпример Верно исправления формализация Спецификация композиция конкретные данные

7 Параметризованное тестирование Проверяемая программа Критические свойства спецификация- предикат Специализация Контрпример Программа, вычисляющая константу Верно исправления формализация Спецификация композиция параметризованный контекст синтаксически очевидная

8 Традиционная верификация на базе моделей Проверяемая программа Модель программы Критические свойства Спецификация Верификатор Контрпример Верно исправления моделирование формализация

9 Задача специализации Пусть программа p(x,y) P определяет функцию F(x,y): X Y D, где X D, Y D. Зафиксируем значение первого аргумента этой функции x 0 X. В задаче специализации требуется построить другую программу q p (y) P такую, что y Y. (q p (y) = p(x 0, y)) Таким образом, программа q p определяет некоторое продолжение функции F(x 0,y) по второй компоненте. Программу q p называют остаточной программой.

10 Пример специализации Специализатор n 0 =10 p(n,m) q p (m) p(n,m) -- умножение натуральных чисел q p (m) = p(10,m) = m0

11Суперкомпиляция Основная цель суперкомпиляции: – выполнить как можно больше действий параметризованного применения программы равномерно по значениям параметров предыдущий узел...

12 Пример дерева развёртки программы (дерева конфигураций) S( n, 1+m) = 1+S( n, m ); S( n, 0 ) = n; S(n,m)1+S(n,m-1) m > 0 m =? 0 n 1+(1+S(n,m-2)) m-1 > 0 m-2 > 0..… m-1 =? 0 m-2 =? 0 1+n 2+n

13 Пример специализации интерпретатора арифметического выражения public static double mySqrt(double a, int iters) { IStatements statements = Assignments.create( new String[] { "a", "x" }, new Assignment[] { new Assignment( new Var("x"), // x = 0.5 * (x + a/x) new Bin('*', new Const(0.5), new Bin('+', new Var("x"), new Bin('/', new Var("a"), new Var("x"))))) }); statements.setValues(new double[] {a, 1.0}); for (int i=0; i

14 Некоторые инструменты суперкомпиляции сужение области определения функции (например, до пустой) аппроксимация образа функции (построение выходных форматов) частично рекурсивные константы частично рекурсивные тождественные функции частично рекурсивные мономы конкатенации

15 Аппроксимация образа функции один из ключевых инструментов

16 Верификация программных моделей Верифицированы параметризованные протоколы когерентности кэш-памяти (cache coherence): –IEEE Futurebus+, MOESI, MESI, MSI, The University of Illinois, DEC Firefly, Berkeley, Xerox PARC Dragon. Верифицированы протоколы: –Java Meta-Locking Algorithm, Reader-Writer protocol, Steve German's directory-based consistency protocol. Верифицированы ряд модельных протоколов описанных в формализме сетей Петри.

17 Программная модель на языке Java протокола MOESI public boolean runModel(Actions actions, int[] pars) throws ActionNonapplicableException { // переменные состояния модели int invalid = pars[0], invalid_ = invalid; int exclusive = 0, exclusive_ = exclusive; int shared = 0, shared_ = shared; int modified = 0, modified_ = modified; int owned = 0, owned_ = owned; require (invalid >= 1); // выполнить последовательность действий Loop: for (Iterator iter = actions.iterator(); iter.hasNext();) { int action = ((Integer)iter.next()).intValue(); // выполнить одно действие switch (action) {... default: require(false); } invalid = invalid_; exclusive = exclusive_; shared = shared_; modified = modified_; owned = owned_; } // проверить конечное состояние if (exclusive + shared + owned >= 1 && modified >= 1) return false; if (exclusive >= 1 && shared + owned >= 1) return false; if (modified >= 2) return false; if (exclusive >= 2) return false; return true; } // описание действий case rm: require (invalid >= 1); invalid_ = invalid - 1; exclusive_ = 0; modified_ = 0; shared_ = shared + exclusive + 1; owned_ = owned + modified; break; case wh2: require (exclusive >= 1); exclusive_ = exclusive - 1; modified_ = modified + 1; break; case wh3: require (shared + owned >= 1); shared_ = 0; exclusive_ = 1; modified_ = 0; owned_ = 0; invalid_ = invalid + modified + exclusive + shared + owned - 1; break; case wm: require (invalid >= 1); shared_ = 0; exclusive_ = 1; modified_ = 0; owned_ = 0; invalid_ = invalid + modified + exclusive + shared + owned - 1; break; Доказываемое постусловие: никогда не выдается false

18 Структура доказательства корректности программной модели протокола MOESI (индукция по структуре данных) Theorem 1 Theorem 2 True2 Lemma $# # # $ $ $$$ True

19 Структура доказательства корректности программной модели протокола Dragon (индукция по структуре данных)

20 Структура доказательства корректности программной модели протокола Dragon (индукция по структуре данных)

21 Ошибка в спецификации Xerox PARC Dragon протокола С помощью суперкомпилятора SCP4 (специализатора программ) в одной из спецификаций этого протокола, обнаруженной в литературе, найдена ошибка и построен тест, указывающий на эту ошибку. Giorgio Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. Proc. of 13th Int. Conference on Computer Aided Verification LNCS 1855, Springer Verlag, 2000, pp: 53–68.

22 Поиск теста, указывающего на ошибку Если повезёт, то тест представлен явно в синтаксисе программы: F( описание теста ) = Ложь; ….. F( …. ) = Истина; ….. F( …. ) = Истина; В общем случае необходим анализ программы (раскрутка её снизу вверх от выходов Ложь ).

23 Использование результатов исследований в образовательном процессе Университета г. Переславля Фрагмент программы курса для студентов: Математические модели функциональных программ и методы спецификации свойств их корректности. Верификация свойств корректности функциональных программ. Математические модели распределённых вычислительных систем. Методы описания свойств их корректности. Верификация протокола передачи данных через ненадёжную среду. Анализ свойств корректности императивных программ. Метод индуктивных утверждений Флойда для доказательства корректности. Метод фундированных множеств для доказательства полной корректности императивных программ.

24Публикации [1] Немытых А.П., Суперкомпилятор SCP4: Общая структура. Монография. Издательство УРСС, Москва, стр. [2] Лисица А.П. и Немытых А.П., Верификация как параметризованное тестирование (Эксперименты с суперкомпилятором SCP4). ЖурналПрограммирование, 1, стр.22-34, (журнал переводится на английский язык Programming and Computer Software) [3] Lisitsa A.P. and Nemytykh A.P., Reachability Analysis in Verification via Supercompilation, The Proc. of the Satellite Workshops of DTL 2007 / TUCS General Publication, No. 45, Part 2, pp Finland [4] Lisitsa A.P., and Nemytykh A.P., A Note on Specialization of Interpreters, Lecture Notes in Computer Science, Vol. 4649, pp , The Proc. of CSR [5] Анд. В. Климов, Детерминированные параллельные вычисления с монотонными объектами, В трудах конференции «Научный сервис в сети Интернет: многоядерный компьютерный мир. 15 лет РФФИ», Изд- во Московского государственного университета, 2007.

25 Доклады на международных конференциях «The 2-nd International Symposium on Computer Science in Russia (CSR-2007)», г. Екатеринбург, сентябрь 2007 г. Доклад: A Note on Specialization of Interpreters «Workshop on Reachability Problems (RP-2007)», July 7–8, 2007, Turku, Finland, июль 2007 г. Доклад: Reachability Analysis in Verification via Supercompilation.

26 Доклады на Всероссийских конференциях «Научный сервис в сети Интернет: многоядерный компьютерный мир. 15 лет РФФИ», г. Новороссийск, сентябрь 2007 г. Доклад: Детерминированные параллельные вычисления с монотонными объектами.

27 Защищена кандидатская диссертация Специализация функциональных программ методами суперкомпиляции по специальности Теоретические основы информатики

28 Спасибо! Вопросы?

29Публикации [1] Немытых А.П., Суперкомпилятор SCP4: Общая структура. Монография. Издательство УРСС, Москва, стр. [2] Лисица А.П. и Немытых А.П., Верификация как параметризованное тестирование (Эксперименты с суперкомпилятором SCP4). ЖурналПрограммирование, 1, стр.22-34, (журнал переводится на английский язык Programming and Computer Software) [3] Lisitsa A.P. and Nemytykh A.P., Reachability Analysis in Verification via Supercompilation, The Proc. of the Satellite Workshops of DTL 2007 / TUCS General Publication, No. 45, Part 2, pp Finland [4] Lisitsa A.P., and Nemytykh A.P., A Note on Specialization of Interpreters, Lecture Notes in Computer Science, Vol. 4649, pp , The Proc. of CSR [5] Анд. В. Климов, Детерминированные параллельные вычисления с монотонными объектами, В трудах конференции «Научный сервис в сети Интернет: многоядерный компьютерный мир. 15 лет РФФИ», Изд- во Московского государственного университета, 2007.