автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Верификация распределенных программ методом проверки на модели

Введение

Идея формальных методов.

Принципы формальной верификации.

Цель работы.

Основные результаты.

Структура работы.

1 Современные средства формальной верификации

1.1 Классификация моделей программ и языков спецификации.

1.2 Верификация моделей программ.

1.2.1 Методы верификации.

1.2.2 Обзор современных систем верификации моделей программ.

1.2.3 Тенденции развития средств верификации программ.

1.3 Формальная постановка задачи

1.3.1 Распределенные программы.

1.3.2 Модели распределенных программ.

1.3.3 Логика ветвящегося времени СТЬ.

1.3.4 Формальная постановка задачи.

2 Общая схема алгоритмов верификации программ

2.1 Теоретико-множественная схема верификации программ методом проверки на модели.

2.2 Поиск подтверждающего вычисления.

2.2.1 Линейные трассы

2.2.2 Циклические трассы.

2.3 Алгоритмы верификации справедливых моделей программ.

2.3.1 Формальное определение справедливости

2.3.2 Верификация слабо справедливых моделей программ.

2.3.3 Верификация сильно справедливых моделей программ.

2.3.4 Модификация алгоритма восстановления трасс.

3 Построение моделей распределенных программ

3.1 MM-язык описания распределенных программ

3.1.1 Основные конструкции языка ММ

3.1.2 Понятие временного автомата.

3.1.3 Временные автоматы контекста.

3.1.4 Семантика языка ММ.

3.2 Язык спецификаций.

3.3 Язык представления моделей MDL.

3.3.1 Основные конструкции языка MDL.

3.3.2 Семантика языка MDL.

3.3.3 Композиционная семантика MDL-программ.

3.4 Построение модели распределенной программы.

3.4.1 Абстракция MM-программ.

3.4.2 Трансляция элементарных конструкций языка ММ.

3.4.3 Моделирование взаимодействия.

3.5 Корректность трансляции

3.6 Извлечение контрпримера вычисления на ММ.

4 Графовая реализация алгоритмов верификации

4.1 Графовое представление модели.

4.2 Графовый алгоритм.

4.3 Алгоритм восстановления трасс.

4.4 Справедливая верификация

4.4.1 Графовый алгоритм верификации в ограничениях слабой справедливости

4.4.2 Графовый алгоритм верификации в ограничениях сильной справедливости

5 Символьная реализация алгоритмов верификации

5.1 Представления булевых функций.

5.1.1 Базовые сведения о BDD.

5.1.2 Операции над BDD.

5.2 Символьное представление модели

5.3 Алгоритм символьной верификации.

5.3.1 Методы повышения эффективности символьной верификации.

5.4 Алгоритм восстановления трасс.

5.5 Справедливая верификация

5.5.1 Алгоритм символьной верификации в ограничениях слабой справедливости

5.5.2 Алгоритм символьной верификации в ограничениях сильной справедливости

6 Система верификации в среде ДИАНА

6.1 Устройство системы верификации в среде ДИАНА.

6.2 Практические результаты применения системы верификации.

Возможность применения строгих математических методов для доказательства правильности программ была осознана уже давно [4, 5]. Однако сложность этих методов и невысокая эффективность вычислительной техники того времени препятствовали их широкому использованию. В последнее десятилетие положение дел существенно изменилось. Бурное развитие информационных технологий привело к широкому внедрению вычислительной техники во многих сферах человеческой деятельности. В соответствии с этим значительно повысились требования, предъявляемые к технологии разработки аппаратуры и программного обеспечения. Все более широкое распространение получают новые типы информационных систем — встроенные системы управления, сетевые протоколы и др. Очень скоро обнаружилось, что традиционные средства отладки и обоснования правильности программ неадекватны современным требованиям, предъявляемым к обоснованию правильности и надежности программ. Тестирование и моделирование программ требуют значительной ручной работы, проводятся медленно и не позволяют гарантировать отсутствие ошибок в программе. Поэтому требуются новые методы, позволяющие:

• гарантировать правильную работу программ;

• минимизировать или полностью исключить участие человека при проверке правильности программы;

• доказывать корректность программ, не ухудшая временной график процесса разработки программ (по сравнению с традиционными средствами).

Надежды, связанные с разработкой и внедрением этих методов небеспочвенны. Имеется широкий класс реагирующих программ, обоснование правильности которых предполагает анализ корректности взаимодействия отдельных компонентов программных систем друг с другом и с окружающей средой. Здесь требуется уметь выявить такие свойства, как отсутствие взаимной блокировки, корректность отклика, синхронность взаимодействия и др. (см. [109]). Именно такие свойства наиболее трудны для проверки с использованием традиционных средств отладки программ, хотя именно они определяют безопасность и надежность функционирования сложных систем, состоящих из многих взаимодействующих процессов.

В начале 80-х было установлено, что все эти свойства программ можно выразить при помощи той или иной разновидности темпоральных логик, а саму проверку правильности программы организовать полностью автоматически с использованием специальных алгоритмов верификации моделей программ [123, 125, 42]. Такой подход, при котором требования, предъявляемые программе, записываются на формальном логико-математическом языке, а для проверки их выполнимости применяются строго обоснованные математические методы, получил название формального подхода к проверке правильности программ.

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

В 1992 году Кларк (Clarke) использовал верификатор SMV [113] для верификации протокола когерентности кеша в стандарте IEEE Futurebus-|- [45, 104]. В результате был найден ряд не обнаруженных прежде ошибок и возможных ошибок в дизайне.

Проект NewCoRe, продолжающийся в AT&T с 1989 по 1992 год, преследовал цель автоматически доказать корректность протокола ITU ISDN/IUPP [38, 81]. Во время работы проекта было найдено и исправлено 112 ошибок дизайна. Примерно 55% исходных требований оказались логически противоречивыми.

В настоящей работе в рамках этого формального подхода нами разработаны и реализованы методы и алгоритмы автоматической проверки правильности распределенных императивных программ. Для описания свойств поведения используется темпоральная логика.

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

Идея формальных методов

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

Хорошо известно [5, 4, 6, 79, 70, 56, 122, 3], что программу можно рассматривать как формальный математический объект, который характеризуется синтаксисом и семантикой.

Свойства программы можно разделить на структурные (синтаксические свойства) и свойства поведения и функциональности (семантические свойства). В то время, как проверить выполнимость синтаксических свойств сравнительно просто (в силу простоты используемого формализма; этим, в частности, занимаются компиляторы программ), семантические свойства проверять гораздо сложнее. Трудность проверки семантических свойств обусловлена, в первую очередь, теоремой Райса [130], гласящей, что ни одно нетривиальное функциональное свойство программ в естественных системах: программирования неразрешимо. Поэтому при верификации программ приходится ограничиваться полуразрешающими процедурами.

Наиболее общая формулировка задачи верификации программ такова [17]. С каждой программой П можно связать множество Сп всевозможных вычислений, которые порождаются программой. Это множество Сд будем называть поведением программы. Требования к программе также задаются на формальном математическом языке. Формальную запись требований к программе мы будем называть далее спецификацией программы. Спецификация 5 выделяет множество С5 вычислений, согласованных с этой спецификацией.

Задача верификации программы — это обоснование того, что поведение программы удовлетворяет ее спецификации, т.е. Сд С

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

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

Принципы формальной верификации

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

1. Построение модели программы.

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

В любом случае выбранный класс формальных моделей и сам процесс построения модели программы должен удовлетворять следующим требованиям [47]:

Консервативность. Для каждой рассматриваемой программы П ее модель Мп должна сохранять определенные свойства поведения программы. Обычно для сложных программ это требование соблюсти невозможно. Поэтому при верификации программ приходится ограничиваться требованием слабой консервативности: выполнимость заданного свойства Б на модели влечет выполнимость этого же свойства для исходной программы. Более формально, если М — модель программы П, а См ~ поведение модели, то из См С С5 должно следовать Сд С С3, то есть модель должна удовлетворять требованию Сп С См

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

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

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

2. Построение спецификации программы.

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

Согласованность с моделью программы. Язык спецификаций должен быть согласован с языком моделирования. Это означает, что требования, предъявляемые к поведению программы могут быть в равной мере отнесены и к поведению модели программы. С учетом требования консервативности модели, задача верификации программы сводится, таким образом, к задаче проверки правильности спецификации на модели программы.

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

Формальность. Как и язык моделирования, язык спецификаций должен либо являться непосредственным представлением информации для известных и хорошо разработанных математических теорий и методов, либо иметь возможность трансляции в такое представление.

3. Верификация модели программы.

Верификация модели программы — это формальное доказательство соответствия модели программы ее спецификации. Основные требования к процедуре верификации таковы.

Эффективность. Доказательство правильности моделей реальных программ должно проводиться автоматически за разумное время.

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

Цель работы

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

По результатам анализа существующих моделей цель работы была уточнена следующим образом:

1. Способ представления формальных требований.

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

2. Метод проверки.

В качестве метода проверки выбран метод проверки на модели (Model checking, [47]). Этот метод может использовать логику как язык для спецификации свойств программ. Преимущества метода в том, что возможна полностью автоматическая проверка правильности свойств программ на основе высокоэффективных алгоритмов проверки.

3. Способ представления программ в процессе верификации.

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

На основании предложенных уточнений в рамках данной работы ставятся следующие задачи:

• разработать алгоритмы верификации программ методом проверки на модели;

• предложить методы построения абстрактной модели распределенной программы, записанной на языке программирования высокого уровня;

• реализовать систему формальной верификации распределенных программ.

Основные результаты

Основные результаты, полученные при решении поставленной задачи, таковы.

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

2. Разработан язык MDL для внутреннего представления моделей распределенных программ. Построен алгоритм трансляции описаний распределенных программ на языке программирования высокого уровня в описания моделей программ на языке MDL. Корректность предложенного алгоритма доказана.

3. На основе полученных теоретических результатов разработано инструментальное средство верификации распределенных программ, включающее:

• язык внутреннего представления модели;

• транслятор описаний распределенных программ в формальное описание моделей программ;

• процедуры символьной и графовой проверки CTL спецификаций на моделях распределенных программ;

• процедуры извлечения контрпримеров и их отображения в описания распределенных программ.

Структура работы

Работа состоит из введения и шести глав.

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

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

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

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

Четвертая глава посвящена графовым алгоритмам верификации программ методом проверки на модели. В этой главе описывается конкретная реализация теоретико-множественных алгоритмов из главы 2 для использования применительно к моделям Крипке, представленным графом переходов.

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

Шестая глава описывает реализацию разработанных алгоритмов в среде ДИАНА. Г

1. Ахо А., Хопкрофт Д., Ульман Д. Построение и анализ вычислительных алгоритмов. М., Мир, 1979.

2. Котов В. Е., Сабельфельд В. К. Теория схем программ. М., Наука, 1991.

3. Янов Ю. И. О логических схемах алгоритмов. Проблемы кибернетики, вып. 1, М., Физматгиз, 1958.

4. Ляпунов А. А. О логических схемах программ. Проблемы кибернетики, вып. 1, М.:Физматгиз, 1958.

5. Ершов А. П. Современное состояние теории схем программ. Проблемы кибернетики, Вып.27. — М.:Наука, 1973.

6. Нигматуллин Р. Г. Сложность булевых функций. Издательство Казанского университета, 1983.

7. Смелянский P. JI. Формальная модель функционирования распределенных вычислительных систем. Вестник Московского университета, 15(3):3-19, 1990.

8. Бакалов Ю. В. Алгоритмический анализ поведения распределенных систем. PhD thesis, МГУ, Москва, 1996.

9. Подловченко Р. И. От схем Янова к теории моделей программ. Математические вопросы кибернетики, вып. 7, 1998.

10. Кончаков Р. В. Об одном языке для спецификации распределенных программ. Труды IV Международной конференции «Дискретные модели в теории управляющих систем», 2000.

11. Питерсон Д. Теория сетей Петри и моделирование систем. М., Мир, 1984.

12. Alur R., Courcoubetis С., Dill D. L. Model checking in dense real time. Information and Computation, 104(l):2-34, 1993.

13. Alur R., Dill D. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994.

14. Alur R., Yannakakis M. Model checking of message sequence charts. In Proc. 10th Intl. Conf. on Concurrency Theory, pages 114-129. Springer Verlag, 1999.

15. Andersen H. R. An introduction to binary decision diagrams. Manuscript, 1997.

16. Apt K., Olderog E.-R. Verification of Sequential and Concurrent Programs. Texts and monographs in computer science. Springer Verlag, 1991.

17. Aziz A., Tasiran S., Brayton R. K. BDD variable ordering for interacting finite state machines. In Proc. of the Design Automation Conf, pages 283-288, June 1994.

18. Baeten J. С. M., Weijland W. P. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.

19. Beer I., Ben-David S., Eisner C., Engel Y., Gewirtzman R., Landver A. Establishing PCI compliance using formal verification: a case study. In Intl. Phoenix Conf. on Сотр. and Comm., 1995.

20. Beer I., Ben-David S., Eisner C., Geist D., Gluhovsky L., Heyman Т., Landver A., Paanah P., Rodeh Y., Ronin G., Wolfsthal Y. RuleBase: Model checking at IBM. In Proceedings of С A V'97, 1997.

21. Bellini P., Mattolini R., Nesi P. Temporal logics for real-time system specification. ACM Computing Surveys, 32(l):12-42, March 2000.

22. Bengtsson J., Christensen P., Jensen P., Larsen K. G., Larsson F., Pettersson P., S0rensen Т., Yi W. UPPAAL: a tool suite for validation and verification of real-time systems. http://www.docs.uu.se/rtmv/uppaal/uppaalguide.ps.gz, 1996.

23. Berry G., Gonthier G. The Esterel synchronous programming language : Design, semantics, implementation. Science of Computer Programming, 19(2):87-152, 1992.

24. Bertin V., Closse E., Poize M., Pulou J., Sifakis J., Venier P., Weil D., Yovine S. Taxys = Esterel + Kronos. A tool for verifying real time properties of embedded systems. In Proc. CD С'01, 2001.

25. Bertin V., Poize M., Pulou J., Sifakis J. Towards validated real-time software. In 12th Euromicro Conference on Real-Time Systems, June 2000.

26. Biberstein O., Buchs D., Guelfi N. Object-oriented nets with algebraic specifications: The CO-OPN/2 formalism. In Concurrent Object-Oriented Programming and Petri Nets, pages 73-130, 2001.

27. Bouali A., Ressouche A., Roy V., de Simone R. The fc2tools set. In Alur R., Henzinger T. A., editors, Proc. of 8th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 441-445. Springer Verlag, July 1996.

28. Brookes S. D., Hoare C. A. R., Roscoe A. W. A theory of communicating sequential processes. Journal of the ACM, 31(3):560-599, 1984.

29. Browne A., Manna Z., Sipma H. Modular verification diagrams, tech. rep., Computer Science Department, Stanford University, 1996.

30. Browne M. C., Clarke E. M., Dill D. L., Mishra B. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12): 1035-1044, 1986.

31. Bryant R. E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.

32. Bryant R. E. Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Suruays, 24(3):293-318, September 1992.

33. Buchi J. R. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Methodology and Philosophy of Science, pages 1 11. Stanford University Press, 1960.

34. Burch J. R., Clarke E. M., Long D. E., McMillan K. L., Dill D. L. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401-424, April 1994.

35. Burch J., Clarke E. M., McMillan K. L., Dill D. L., Hwang L. J. Symbolic model checking: 1020 states and beyond. Inform, and Comput., 98:142-170, 1992.

36. Chandy K. M., Misra J. Parallel Program Design — a Foundation. Addison Wesley, 1988.

37. Chaves J. Formal methods at AT&T: An industrial usage report. In Formal Description Techniques IV 1991, pages 83-90, North Holland, 1992.

38. Clarke E., Grumberg O., Hamaguchi K. Another look at LTL model checking. Formal Methods in System Design, 10(1):57-71, February 1997.

39. Clarke E. M., Emerson E. A. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer Verlag, 1981.

40. Clarke E. M., Emerson E. A., Jha S., Sistla A. P. Symmetry reduction in model checking. In 10th International Conference CAV'98, volume 1427 of LNCS, pages 147-158, Vancouver, BC, Canada, June/July 1998.

41. Clarke E. M., Emerson E. A., Sistla A. P. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. Programming Languages Systems, 8(2):244-263, 1986.

42. Clarke E. M., Grumberg O., Hiraishi H., Jha S., Long D. E., McMillan K. L., Ness L. Verification of the Futurebus+ cache coherence protocol. In CHDL, 1993.

43. Clarke E. M., Grumberg O., McMillan K. L., Zhao X. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proc. 32nd Design Automat. Conf., pages 427432, June 1995.

44. Clarke E. M., Grumberg O., Peled D. Model Checking. MIT Press, December 1999.

45. Cleaveland R., Smolka S. A. Strategic directions in computing research — concurrency working group report. Bulletin of the European Association for Theoretical Computer Science, 60:97122, 1996.

46. Closse E., Poize M., Pulou J., Sifakis J., Venier P., Weil D., Yovine S. TAXYS: a tool for the developpment and verification real-time embedded systems. In CAV'01, volume 2102 of LNCS, 2001.F

47. D'Argenio P. R., J.P., Katoen, Ruys Т., Tretmans J. Modeling and verifying a bounded retransmission protocol. In Proc. of COST 247, International Workshop on Applied Formal Methods in System Design, 1996.

48. Daws C., Olivero A., Tripakis S., Yovine S. The tool Kronos. In Proc. Hybrid Systems III, Verification and Control, volume 1066 of Lecture Notes in Computer Science. Springer Verlag, 1996.

49. Daws C., Olivero A., Yovine S. Verifying ET-LOTOS programs with KRONOS. In Proc. FORTE'94, pages 227-242, October 1994.

50. Daws C., Yovine S. Symbolic forward analysis of timed automata. Technical report, Spectre 9516, Verimag, November 1995.

51. Daws C., Yovine S. Two examples of verification of multirate timed automata with KRONOS. In Proc. IEEE RTSS'95. IEEE Computer Society Press, December 1995.

52. Dijkstra E. W. Cooperating sequential processes. Programming Languages, pages 43-112, 1968. Originally appeared as Technical Report EWD123, Technical University of Eindhoven, the Netherlands, 1965.

53. Dill D. L., Drexler A. J., Hu A. J., Yang С. H. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522-525. IEEE Computer Society, 1992.

54. Dill D. L., Park S., Nowatzyk A. G. Formal specification of abstract memory models. In Borriello G., Ebeling C., editors, Proceedings of the Intl. Symposium Research on Integrated Systems, pages 38-52. MIT Press, 1993.

55. Eisner C. CC/NUMA formal verification project — summary and report. Technical report, IBM Internal Memorandum, 1995.

56. Eisner C. AS/400 SCU formal verification interim report. Technical report, IBM Internal Memorandum, 1997.

57. Eisner C., Shurek G., Meil G., Raghavan R. CCP (cache coherence protocol) formal verification project distributed shared memory cache coherence protocol — summary and report. Technical report, IBM Internal Memorandum, 1997.

58. Emerson E., Sistla A. Symmetry and model checking, formal Methods in System Design, 9 (1/2)-.105-130, 1996.

59. Emerson E. A. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, pages 997-1072. Elsevier Science Publishers, 1990.

60. Emerson E. A., Mok A. K., Sistla A. P., Srinivasan J. Quantitative temporal reasoning. In Proc. Workshop on Finite-State Concurrency, 1989.

61. Esparza J. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85-107, 1997.

62. Fernandez J. An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13(2-3):219-236, May 1990.

63. Floyd R. V. Assigning meanings to programs. Proc. Symp. on Applic. Math., 19:19-32, 1967.

64. Fujii H., Ootomo G., Hori C. Interleaving based variable ordering methods for ordered binary decision diagrams. In Proc. Intl. Conf. on ComputerAided Design, pages 38-41, Nov 1993.

65. Garabel H., Lang F., Mateesku R. An overview of CADP 2001. Technical Report 0254, INRIA, 2001.

66. Gerth R., Peled D., Vardi M. Y., Wolper P. Simple on-the-fly automatic verification of linear temporal logic. In IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pages 3-18. Chapman & Hall, June 1995.

67. Groote J., Ponse A., Usenko Y. Linearization in parallel pCRL. Journal of Logic and Algebraic Programming, 48(1 2):39-72, 2001.

68. Halpern J., Manna Z., Moszkowski B. A hardware semantics based on temporal intervals. In Proceedings of the 10th Colloquium on Automata Languages and Programming, 1983.

69. Hennessy M. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts, 1988.

70. Henzinger T., Nicollin X., Sifakis J., Yovine S. Symbolic model checking for real-time systems. Information and Computation, 111(2):193 244, 1994.

71. Hoare C. A. R. An automatic basis for computer programming. Comm. ACM, 10(12):576 583, 1969.

72. Hoare C. A. R. Communicating Sequential Processes. Prentice Hall, London, 1985.

73. Holzmann G. The theory and practice of a formal method: NewCoRe. In IFIP World Computer Congress, Hamburg, Germany, August 1994.

74. Holzmann G. J. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, N.J., 1991.

75. Holzmann G. J. An analysis of bit-state hashing. In Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pages 301-314, 1995.

76. Holzmann G. J. The model checker SPIN. IEEE Trans, on Software Engineering, 23(5):279-295, May 1997.

77. Holzmann G. J. State compression in SPIN: Recursive indexing and compression training runs. In Langerak R., editor, Proc. Third SPIN Workshop. Twente Univ., Apr 1997.

78. Holzmann G. J., Peled D. An improvement in formal verification. In Proc. Seventh FORTE Conf. Formal Description Techniques, pages 177-194, Oct 1994.

79. Holzmann G. J., Peled D., Yannakakis M. On nested depth-first search. In Proc. Second SPIN Workshop, pages 23-32. Am. Math. Soc., Aug 1996.

80. Ip C. N., Dill D. L. Efficient verification of symmetric concurrent systems. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 230-234. IEEE Computer Society, 1993.

81. Ip C. N., Dill D. L. Better verification through symmetry. Formal Methods in System Design, 9(1/2):41-55, August 1996.

82. Ip C. N., Dill D. L. State reduction using reversible rules. In 33rd Design Automation Conference, June 1996.

83. Ip C. N., Dill D. L. Verifying systems with replicated components in murphi. In International Conference on Computer-Aided Verification, 1996.

84. Jensen H. E., Larsen K. G., Skou A. Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL. In Proc. of 2nd International Workshop on the SPIN Verification System, pages 1-20, 1996.

85. Keller R. Formal verification of parallel programs. Communications of the ACM, 19(7):371 384, July 1976.

86. Kesten Y., Pnueli A. Modularization and abstraction: The keys to practical formal verification. In Mathematical Foundations of Computer Science, pages 54-71, 1998.

87. Konchakov R. On the semantics of concurrent programming languages: An automata-theoretic approach. In ESSLLI'01 student session., 2001.

88. Kupferman O., Grumberg O. Branching-time temporal logic and tree automata. Inform, and Comput., 125:62-69, 1996.

89. Kurshan R. P. Computer-aided Verification of Coordinating Processes: the automata-theoretic approach. PhD thesis, Princeton University Press, 1994.

90. Larsen K. G., Peterson P., Yi W. UPPAAL in a nutshell. Software Tools for Technology Transfer, 1:134-153, 1997.

91. Larsen K. G., Pettersson P., Yi W. Model-checking for real-time systems. In Proc. of Fundamentals of Computation Theory, volume 965 of Lecture Notes in Computer Science, pages 62-88, August 1995.

92. Larsson F., Larsen K. G., Pettersson P., Yi W. Efficient verification of real-time systems: Compact data structures and state-space reduction. In Proc. of the 18th IEEE RealTime Systems Symposium, pages 14-24, December 1997.

93. Long D. L. Model checking, abstraction, and compositional reasoning. PhD thesis, Carnegie Mellon Computer Science Department, 1993.

94. Lonn H., Pettersson P. Formal verification of a TDMA protocol startup mechanism. In Proc. Pacific Rim International Symposium on Fault-Tolerant Systems, December 1997.

95. Lynch N. A., Tuttle M. R. An introduction to input/output automata. CWI Quarterly, 2(3):219-246, September 1989.

96. M. J. C. Gordon. HOL: A machine oriented formulation of higher order logic. Technical Report 68, University of Cambridge, Computer Laboratory, 1985.

97. Maidl M. The common fragment of CTL and LTL. In IEEE Symposium on Foundations of Computer Science, pages 643-652, 2000.

98. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Verlag, 1992.

99. Mateescu R., Garavel H. XTL: A meta-language and tool for temporal logic model-checking. In Margaria T., editor, Proceedings of the International Workshop on Software Tools for Technology Transfer STTT'98, pages 33-42. BRICS, July 1998.

100. Mazurkiewicz A. Trace theory. In Brauer W., Reisig W., Rozenberg G., editors, Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets, volume 255 of Lecture Notes in Computer Science, pages 279-324, 1987.

101. McMillan K. L. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, May 1992.

102. Milner R. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

103. Milner R. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

104. Mitchell J. C., Mitchell M., Stern U. Automated analysis of cryptographic protocols using Murphi. In IEEE Symposium on Security and Privacy, 1997.

105. Mitchell J. C., Shmatikov V., Stern U. Finite-state analysis of SSL 3.0. In 7th USENIX Security Symposium, 1998.

106. Ostroff J. S. Temporal Logic for Real Time system. Wiley Advances software development series. John Wiley and Sons, Inc., 1989.

107. Park S., Dill D. L. An executable specification, analyzer and verifier for RMO (relaxed memory order). In 7th ACM Symposium on Parallel Algorithms and Architectures, pages 34-41, 1995.

108. Peled D. Combining partial order reductions with on-the-fly model-checking. In Sixth Int'l Conf. Computer Aided Verification (CAV94), volume 818 of Lecture Notes In Computer Science, pages 377-390. Springer Verlag, 1994.

109. Penczek W., Szreter M., Gerth R., Kuiper R. Partial order reductions preserving simulations. In Proc. of Concurrency, Specification and Programming (CS&P'99), pages 153-172, Warsaw, 1999.

110. Petri C. A. Communication with automata. RADCTR65377 1, Applied Data Research, 1966.

111. Pnueli A. The temporal logic of programs. In 18-th IEEE Symposium on Foundations of Computer Science, pages 46-57. Computer Society Press, 1977.

112. Qmips Groups. The timed (coloured) petri net formalism: position paper. Available at: http://citeseer.nj.nec.com/266439.html.

113. Queille J. R., Sifakis J. Specification and verification of concurrent system in caesar. In Proc. 5th International Symp. on Programming, volume 137 of LNCS, pages 337-351, 1981.

114. Rabin M. Weakly definable relations and special automata. In Proc. Symp. Mathematical Logic and Foundations of Set Theory, pages 1-23. Elsevier, 1970.

115. Ranjan R. K., Aziz A., Plessier B., Pixley C., Brayton R. K. Efficient BDD algorithms for FSM synthesis and verification. In IEEE/ACM Proceedings International Workshop on Logic Synthesis, May 1995.

116. Razouk R., Gorlick M. Real-time interval logic for reasoning about executions of real-time programs. SIGSOFT Softw. Eng. Notes, 14(8):10 19, 1989.

117. Reisig W. Petri Nets — An Introduction, volume 4 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.

118. Rice H. G. Classes of recursively enumerable sets and their decision problems. Transactions of American Mathematical Society, 74(2), 1953.

119. Schmidt D. A. Deniotational Semantics: A Methodology for Language Development. Allyn k. Baco, 1986.

120. Schwartz R. L., Mellar-Smith P. M. From state machines to temporal logic: Specification methods for protocol standarts. IEEE Trans. Comm., 30(12):2486-2496, 1982.

121. Sipma H., Uribe T., Manna Z. Deductive model checking. In Alur R., Henzinger T. A., editors, Proc. of 8th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science. Springer Verlag, July 1996.

122. Stern U., Dill D. L. Automatic verification of the SCI cache coherence protocol. In Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995.

123. Stern U., Dill D. L. Improved probabilistic verification by hash compaction. In Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995.

124. Stern U., Dill D. L. Parallelizing the Murphi verifier. In 9th International Conference on Computer Aided Verification, 1997.

125. Tarjan R. Depth first search and linear graph algorithms. SI AM J. Computing, 1(2):146-160, 1972.

126. Team T. D. The project DrTesy final report, http://www.first.gmd.de/~drtesy, 1999.

127. Tripakis S., Yovine S. Analysis of timed systems based on time-abstracting bisimulations. Technical report, Spectre 9515, Verimag, November 1995.

128. UPPAAL Team. Formal modeling and analysis of an audio/video protocol: An industrial case study using UPPAAL. Technical report, Univ. Uppsala, Univ. Aaltzburg, 1997.

129. Vardi M. Y. Nontraditional application of automata theory. In Proc. Int. Symp. TACS'94, pages 575-597, 1994.

130. Vardi M. Y., Wolper P. Reasoning about infinite computations. Information and Computation, 115:1-37, 1994. appeared as a conference paper in 1983.

131. Virbitskaite I. B., Bystrov A. V. Implementing Model Checking and Equivalence Checking for Time Petry Nets by the RT-MEC Tool, volume 1662 of Lecture Notes in Computer Science, pages 194-200. Springer Verlag, 1999.

132. Visser W. Memory efficient storage in SPIN. In Proc. Second SPIN Workshop. Am. Math. Soc., Aug 1996.

133. Yi W., Pettersson P., Daniels M. Automatic verification of real-time communicating systems by constraint-solving. In Proc. of the 7th International Conference on Formal Description Techniques, 1994.