На главную

На главную ИПС РАН

Назад в список проектов

Верификация программ посредством их параметризованного тестирования специализаторами на базе моделей этих программ, реализация верификатора для языка программирования JAVA

  • Номер контракта: 02.514.11.4049
  • Период выполнения: 18.05.2007 — 31.10.2008
  • Исполнитель: Учреждение Российской академии наук Институт программных систем  РАН
  • Ключевые слова: верификация, тестирование, отладка, эксперименты, model checking, язык программирования JAVA, языки спецификаций, параметризированные модели программ, распределенные вычислительные системы, оптимизация, специализация программ, суперкомпиляция, формальные модели, прототип.

Объектом исследования являются методы верификации программных систем со сложным поведением на базе моделей этих программ, методы верификации распределённых вычислительных систем.

Целью работы является создание эффективных автоматических методов верификации на основе специализации и реализация на основе этих методов прототипа верификатора программ написанных на языке программирования Java.

Методы исследований включают в себя кодировки верифицируемых объектов в виде программ с последующей их глубокой оптимизацией (суперкомпиляцией). Инструменты суперкомпиляции содержат элементы рассуждений методом математической индукции по структуре данных преобразуемой программы.

Полученные результаты включают в себя:
Показана возможность использования разработанного метода для верификации параметризованных (т.е. число процессоров в системе конечно, но неизвестно сколько) cache coherence протоколов с условиями глобальной корректности.

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

По разработанной схеме проведены автоматические доказательства корректности следующих snooping cache coherence протоколов с условиями глобальной корректности: Synapse N+1, Xerox PARC Dragon, MOESI, IEEE Futurebus+, MESI, MOSI, MSI, “The University of Illinois”, DEC Firefly, “Berkeley” (см. [37], [10], [11]). Мы удачно проверифицировали Steve German’s directory consistency клиент-сервер протокол [13] и Load Balancing протокол [12].

Построена формальная модель, описывающая инструменты суперкомпиляции (одной из технологий автоматической специализации программ), использование которых достаточно для верификации рассматриваемого класса cache coherence протоколов. Доказана теорема корректности этой формальной модели.

Разработаны алгоритмы суперкомпилятора и верификатора объектно-ориентированного языка Java на основе ранее разработанных методов верификации средствами суперкомпляции и опыта применения суперкомпилятора SCP4 языка Рефал к задаче верификации программ и программных систем со сложным поведением на примере задач верификации моделей параметризованных cache coherence протоколов с условиями глобальной корректности. Разработанные алгоритмы реализованы в прототипе верификатора Java программ JVer, отлажены и оттестированы.

Разработан набор тестовых программ для верификатора языка Java, которые являются сложными содержательными задачами, имеющими практическое значение, — моделями различных параметризованных коммуникационных протоколов. Один тест представляет собой неправильную модель протокола и предназначен для проверки того, как верификатор отрабатывает неверные программы и спецификации. В этом случае верификатор должен определить начальные данные, для которых выдается false.

Разработана методика экспериментальных исследований и подготовлены тестовые программы. Реализован прототип верификатора Java программ (JVer). Прототип верификатора JVer прошел отладку, тестирование и апробацию как на разработанных тестах, так и на внешних тестовых примерах.

Часть тестов была разработана в рамках данного проекта. В частности, к ним относится набор тестовых программ для верификатора языка Java, которые являются сложными содержательными задачами, имеющими практическое значение, — моделями различных параметризованных коммуникационных протоколов.

Другая часть алгоритмов и построенных на их основе тестовых программ является внешней по отношению к данному проекту. Например, в качестве тестовых программ использовались программы для вычисления быстрого преобразования Фурье, бинарного поиска числа в упорядоченном массиве чисел, предикат кодирующий головоломку А.Эйнштейна.

Разработанные тестовые программы проверяют основные элементы алгоритмов верификации на основе суперкомпиляции: распространение условий на значения параметров вдоль путей метаинтерпретации, автоматического определения глубины развертки графа программы, автоматического построения промежуточных индуктивных гипотез, правильность работы конфигурационного анализа, построения моделей программ адекватных контексту их использования.

На примере неудачной спецификации протокола Xerox PARC Dragon данной Ж. Дельзанно [11] показана возможность использования верификатора JVer для обнаружения ошибок спецификации и построения тестов на эти ошибки.

Проведено теоретическое обобщение результатов работ по данному проекту. Результаты исследований опубликованы в рецензируемых международных журналах и доложены на российских и международных конференциях. Результаты исследований проводившихся в рамках данного проекта представлены 15-ю докладами на международных и всероссийских конференциях.

Результаты теоретических исследований и практической реализации прототипа верификатора использованы в образовательном процессе в Университете г. Переславля.

Разработанные и реализованные в ходе выполнения проекта программные продукты прошла государственную регистрацию:

Проведены патентные исследования с целью получения обоснованных данных для проверки патентной чистоты созданных по теме НИР объектов интеллектуальной собственности, получения обоснованных данных для анализа созданных по теме НИР объектов интеллектуальной собственности на соответствие их критерию патентоспособности «новизна» и получения сведений об охранных и иных документах, которые могли бы препятствовать использованию созданных по теме НИР объектов интеллектуальной собственности на территории РФ и зарубежом, а также условий использования таких документов.

Возможная область применения: автоматическая верификация спецификаций программных систем со сложным поведением, реализованных на языке программирования Java, распределённых вычислительных систем и электронных устройств; полуавтоматическое построение подозрительных тестов, возможно, указывающих на ошибки спецификации.

Значимость данной работы. Актуальность данной работы определяется широким распространением языка программирования Java, быстрым развитием возможностей для организации распределённых вычислений, большой трудоёмкостью проверки корректности спецификаций объектов и громадными неэффективными материальными затратами при реализации и внедрении ошибочно специфицированных объектов.

Экономический эффект от внедрения разрабатываемых методов верификации и поддерживающих их программных инструментов не вызывает сомнений в контексте неэффективных материальных затрат при реализации и внедрении ошибочно специфицированных вычислительных систем, в частности, Java программ со сложным поведением.

Список использованных источников

[1] R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic Symbolic Verification of Embedded Systems. IEEE Transactions on Software Engineering, v. 22, pp: 181-201, 1996.

[2] К.А. Васильева, Е.В. Кузьмин. Верификация автономных программ с использованием LTL. Журнал “Моделирование и анализ информационных систем”, Ярославль: ЯрГУ, том 14, №1, стр. 3-14, 2007.

[3] Laurent van Begin. The BABYLON Project: A Tool for Specification and Verification of Parameterized Systems to Benchmark Infinite-State Model Checkers. http://www.ulb.ac.be/di/ssd/lvbegin/CST/

[4] B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82-96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society.

[5] R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transac-tion on Computers, C-35(8), pp: 677-691, 1986.

[6] J.E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. of Workshop on Logic of Programs, LNCS, v. 131, Springer, 1981.

[7] J.E.M. Clarke, E.A. Emerson and A.P. Sistla. Automatic verification of finite-state con-current systems using temporal specifications. In Proc. of the 10th Annual ACM Sympo-sium on Principles of Programming Languages. pp:117-125, 1983.

[8] J.E.M. Clarke, E.A. Emerson and A.P. Sistla. Automatic verification of finite-state con-current systems using temporal specifications. ACM Transactions on Programming Lan-guages and Systems. V. 6, № 2, pp: 244-263, 1986.

[9] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analy-sis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp: 238-252, 1977.

[10] G. Delzanno. Automatic Verification of Parameterised Cache Coherence Protocols, in Proc. of the 12th Int. Conference on Computer Aided Verification, LNCS 1855, pp: 53-68, Springer-Verlag, 2000.

[11] G. Delzanno. Automatic Verification of Cache Coherence Protocols via Infinite-state Constraint-based Model Checking, http://www.disi.unige.it/person/DelzannoG/protocol.html.

Назад в список проектов