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

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

На правах рукописи

Васильев Павел Константинович

РАЗРАБОТКА И РЕАЛИЗАЦИЯ СИСТЕМЫ ИНТЕРПРЕТАЦИИ СПЕЦИФИКАЦИЙ НА ЯЗЫКЕ ASM С ВРЕМЕНЕМ И ПРОВЕРКИ СВОЙСТВ ТРАСС ИХ ВЫПОЛНЕНИЯ

05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Санкт-Петербург - 2008

003450707

Работа выполнена на кафедре информатики математико-механического факультета Санкт-Петербургского государственного университета.

Научные руководители:

Официальные оппоненты:

Ведущая организация:

кандидат физико-математических наук, доцент Соловьев Игорь Павлович, доктор наук, профессор Бокье Даниэль (университет Париж 12).

доктор физико-математических наук, профессор Баранов Сергей Николаевич (ЗАО «Моторола ЗАО»), кандидат физико-математических наук, доцент Кознов Дмитрий Владимирович (Санкт-Петербургский государственный университет).

Санкт-Петербургский институт информатики и автоматизации РАН.

Защита состоится » МЛ^Л_ 2008 г. в & часов на заседании совета Д 212.232.51 по защите докторских и кандидатских диссертаций при Санкт-Петербургском государственном университете по адресу: 198504, Санкт-Петербург, Старый Петергоф, Университетский пр., д. 28, математико-механический факультет, ауд. 405.

С диссертацией можно ознакомиться в Научной библиотеке им. М. Горького Санкт-Петербургского государственного университета по адресу: 199034, Санкт-Петербург, Университетская наб., д. 7/9.

Автореферат разослан « ^ »

2008 г.

Ученый секретарь диссертационного совета, доктор физико-математических наук, „ ,

профессор Мартыненко Б.К.

Общая характеристика работы

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

Формализм машин абстрактных состояний (abstract state machines или ASM [17]) был введен в начале 1990-х годов Юрием Гуревичем. Изначально известные под именем развивающиеся или эволюционирующие алгебры (evolving algebras), машины Гуревича фактически стали одним из методов формальной спецификации компьютерных систем. Некоторые идеи метода ASM в виде отдельных концепций уже были известны на момент его создания: псевдокод, концепции виртуальных машин компании IBM и абстрактных машин Дейкстры [13], а также структуры Тарского [20], как наиболее общий метод представления абстрактных состояний некоторых вычислений. Метод ASM объединяет и развивает достоинства перечисленных концепций. С одной стороны, метод ASM является простым и понятным для пользователя, с другой, он позволяет разрабатывать крупномасштабные приложения. В качестве основных идей ASM включает в себя определение локального замещения абстрактного состояния некоторого вычисления (локальное изменение интерпретаций функциональных символов или, другими словами, переопределение значений интерпретирующих функций в отдельных точках), метод последовательного уточнения спецификации Н. Вирта [26] и концепцию базовой модели (ground model) [8], т. е. модель, полученную в результате формализации исходных требований пользователя.

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

Язык ASM, который используется нами в качестве основы языка спецификации, обладает большой выразительной силой. Даже его подмножество, охватывающее простейшие ASM (Basic ASMs [18]), позволяет описать любую алгоритмическую машину состояний, включая машину Тьюринга. Методология ASM нашла свое применение в таких практических задачах, как спецификация семантики языков VHDL, С, С++, Prolog, С#, Java, SDL 2000, спецификация протоколов и других прикладных задач (см. [10; 24]). Та же методология была' успешно применена в создании промышленных компьютерных систем, например, в проекте FALKO [9] компании Siemens (программное обеспечение для разработки и верификации расписаний железнодорожных линий). Еще одним примером применения машин Гуревича в промышленном масштабе'является система AsmHugs [25], предназначенная для валидации технологий Microsoft, в частности модели СОМ. Основные достоинства метода ASM, которые упоминают разработчики, — это выполнимость спецификаций, возможность моделирования на различных уровнях абстракции, а также формальный переход от одного уровня абстракции к другому.

В настоящее время известен целый ряд реализаций интерпретаторов и компиляторов для различных диалектов языка ASM: Microsoft AsmL и Spec Explorer [5], XASM [4], CoreASM [15], Timed ASM (TASM) [21], Distributed ASML [23], ASM Workbench [11], ASM Gofer [22].

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

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

Проектирование и реализация компьютерных систем с ограничениями на время реакции, которые рассматриваются в данной работе, подразумевают необходимость реализации подходящего механизма работы с временными значениями и входными данными. Исходный формализм ASM не предусматривает встроенной временной модели, однако существует ряд работ, предлагающих варианты решения этой задачи. Впервые решение проблемы предложили Гуревич и Хаггинс [19], которые представили вычисления в виде отображения из области временных значений в область состояний ASM. Затем последовали работы [7, 12], в которых проблема верификации временных алгоритмов сводится к верификации формальных спецификаций в виде формул специальной временной логики первого порядка FOTL (First Order Timed Logic).

Для описания свойств спецификаций в формализме ASM требуется достаточно выразительный язык логики. Самым простым логическим языком является язык пропозициональной логики. Однако, нетрудно заметить, что он плохо приспособлен для спецификаций систем с временем. Существует ряд расширений пропозициональной логики, такие, как логики с временем, или темпоральные логики [14], которые обладают большей выразительной способностью, например, LTL, CTL или их модификации. Такие логики широко используются для формальной спецификации программ и вычислительных систем. Хотя указанные логики и являются мощным инструментом формальной спецификации динамических систем, некоторые свойства, например, ограничения на время реакции системы, в них выразить очень сложно. В данной работе для спецификации свойств проектируемой системы применяется язык временной логики первого порядка FOTL. Логика FOTL была специально разработана Д. Бокье и А. Слисенко [6] как метод спецификации алгоритмов и их свойств с непрерывным временем. С помощью языка логики FOTL можно компактно специфицировать сложные свойства поведения компьютерных систем во времени.

В некоторых работах, посвященных использованию времени в методе ASM, предлагается явное использование функции времени, например, в [5,16]. Кроме того, вводятся временные задержки на выполнение либо отдельных фрагментов вычислений, либо замещений [12, 21]. В перечисленных работах содержится множество идей и предложений по использованию и уточнению языка ASM, но, несмотря на это, в них не сформулирована явная методика спецификации систем с ограничениями на время реакции и проверки их свойств.

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

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

Для достижения обозначенных целей были поставлены следующие задачи:

• разработка временной модели для ASM, синтаксиса и семантики рас-■ ширенного временем языка ASM;

• разработка метода проверки ограничительных свойств на языке FOTL применительно к спецификации на расширенном языке;

• разработка и реализация программной системы интерпретации расширенного языка ASM и проверки ограничительных свойств.

Основные результаты. Приведем основные результаты диссертационной работы:

• разработана временная модель ASM с непрерывным временем для спе-. цификации компьютерных систем с ограничениями на время реакции;

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

• разработан синтаксис языка описания временных ограничений на базе языка временной логики первого порядка FOTL;

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

• разработан алгоритм проверки свойств трасс выполнения спецификаций в виде формул логики FOTL без вхождения внешних функций и в случае кусочно-постоянных внешних функций;

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

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

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

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

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

1. Международная конференция «Космос, астрономия и программирование» (Лавровские чтения). СПбГУ, Санкт-Петербург, 2008;

2. Конференция «Процессы управления и устойчивость», СПбГУ, Санкт-Петербург, 2008;

3. Конференция «Научное программное обеспечение в образовании и научных исследованиях». СПбГПУ, Санкт-Петербург, 2008;

4. Четырнадцатый международный семинар ASM'07. Тримстад, Норвегия, 2007;

5. Семинар лаборатории LACL (laboratoire d'algorithmique, complexité et logique). Университет Париж 12, Кретей, Франция, 2007;

6. Семинар, посвященный разработке открытых программных средств для работы с ASM (Pisa Workshop on ASM Open Source Tools). Пиза, Италия, 2007;

7. Четвертая международная конференция FORMATS «Формальное моделирование и анализ систем с временем» (Formal Modeling and Analysis of Timed Systems). Париж, Франция, 2006;

8. Четвертый международный семинар MSVVEIS «Моделирование, симу, ляция, верификация и валидация промышленных информационных систем» (Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems). Пафос, Кипр, 2006;

9. Семинар кафедры информатики математико-механического факультета. СПбГУ, Санкт-Петербург, 2005.

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

Структура и объем диссертации. Диссертация состоит из введения, заключения, пяти глав, пяти приложений и списка литературы. Главы разбиты на разделы и подразделы. Объем основной части работы — 94 страницы. Список литературы состоит из 121 наименования. Полный объем работы — 151 страница.

Содержание работы

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

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

В первой главе вводятся основные понятия, относящиеся к методу ASM. Сначала описывается исходная концепция ASM Гуревича (GASM), затем методы расширения синтаксиса и семантики языка спецификаций. В целом, спецификацию системы с временными ограничениями можно задать парой < ENV,ASMSPEC >, где ENV — это спецификация окружения, которая содержит определения функций окружения, значения задержек для различных операций языка, а также функцию, определяющую способ раскрытия недетерминизмов, a ASMSPEC — это спецификация машины абстрактных состояний Гуревича с временем. ASM с временем, в свою очередь, молено задать тройкой < VOC,INIT,PROG >, где VOC — словарь функциональных символов, IN IT — описание начального состояния машины и PROG — ее программа. Словарь ASM состоит из множества сортов, множества функциональных символов и множества предикатных символов. Некоторые из них имеют фиксированную интерпретацию, например: К — сорт вещественных чисел, Z — сорт целых чисел, N — сорт натуральных чисел, BOOL — сорт булевых значений, Т = 11+ — выделенный сорт значений времени, UNDEF = {undef} — специальный сорт, содержащий одно значение, применяющийся для задания неопределенных значений. Метод ASM позволяет использовать несколько уровней абстракции спецификаций, поэтому на самом высоком уровне абстракции сорт вещественных чисел является математическим множеством вещественных чисел. При переходе на более низкие уровни абстракции базовый сорт может быть уточнен, так на уровне реализации вступают в силу программно-аппаратные ограничения конкретной компьютерной системы. В частности, разработанный интерпретатор в качестве уточнения сорта вещественных чисел использует подмножество рациональных чисел, предоставляемое языком реализации.

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

спецификации систем рассматриваемого класса вводится временная модель, адаптирующая универсальный метод ASM. В числе дополнений необходимо отметить специальное представление внешних функций, которые задают входные данные и формируют окружение. Определение внешних функций формулируется следующим образом. Рассмотрим внешнюю функцию f : X к обозначим соответствующую ей функцию с временным параметром : Тх X —► У, где / — имя функции, X — абстрактный сорт или прямое произведение двух абстрактных сортов, Т — временной сорт, У — абстрактный сорт или сорт TZ. Вариант функции с временным параметром непосредственно в программе ASM не используется, чтобы не усложнять семантику языка. Такие функции предназначены только для описания ограничений пользователя. Для определения внешних функций применяется следующий подход. Рассматривается некоторая интерпретация абстрактного конечного сорта X и множество элементов этой интерпретации нумеруется натуральными числами. Тогда для каждого элемента интерпретации значения некоторой функции / можно задать с помощью индексированной последовательности: /(«). := (4> ft> 4> Л; • • •; 4 Я; • • •). где г G 1,..., n; п - мощность сорта X; t\,t\, ■ •., tlk,... — начальные точки интервалов времени; /{, ..., ... — значения функции, определенные на интервалах. Начальные точки временных интервалов t\ пронумерованы в порядке возрастания. Также поддерживается спецификация функций от двух переменных, т. е. функций, заданных на прямом произведении двух абстрактных сортов Х'хХ". Тогда определение таких функций принимает вид: /(г, j) := (t\3, f{'3\tif, ...; t\3, ft3;...), где i € 1,..., n,j £ 1,..., m; n — мощность сорта X'; m — мощность сорта X"\ остальные обозначения аналогичны использованным в описании одноместной функции.

Далее в этой главе описываются методы приписывания временных задержек операциям языка спецификации с временем. Для обозначения задержек введем функцию <5. Будем считать, что функция задержки задана на множестве правильных предложений языка спецификации и действует в множество временных значений Т. Пусть S — множество всевозможных предложений языка. Тогда тип функции задержки будет выглядеть следующим образом: 6 : S —> Т. Для каждой базовой операции или конструкции значение функции 5 явно задается пользователем и используется интерпретатором для расчета задержек более сложных предложений языка. Чтобы получить задержку суперпозиции синтаксических конструкций Pi и Рг, например, последовательного блока {Р1Р2}, необходимо просуммировать значения задержек всех его составляющих замещений: <5({PiP2}) = <5(Pi) + ¿(Р2). Исключением является случай параллельного замещения, к примеру, [Р1Р2]. В данном случае задержка вычисляется как максимальная задержка среди замещений в параллельном блоке, т. е. ¿([РхРг]) = max{<5(Pi),¿(Рг)}-

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

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

Семантика языка ASM с временем значительно отличается от семантик других известных языков, основанных на методе ASM. Синтаксически конструкции языка выглядят привычным образом, но операции языка имеют ряд дополнительных побочных эффектов. Так, все арифметические действия и операции чтения/записи имеют побочный эффект: изменение состояния глобального счетчика времени. Следовательно, при переходе к следующему состоянию глобальной ASM могут измениться значения внешних функций, что в свою очередь может повлечь за собой изменение потока, управления. Модифицирована также семантика условных операторов цикла, которые при определенных условиях выполнения должны «предвидеть» будущие изменения интерпретаций внешних функций.

В третьей главе описывается метод проверки свойств спецификаций ASM, представленных в виде формул языка некоторой логики. В данной работе была выбрана подходящая для этих целей логика первого порядка с временем FOTL [7]. Приводится описание логики FOTL, описываются ее синтаксические и семантические особенности. Словарь FOTL состоит из конечного числа сортов, функциональных и предикатных символов. Каждая переменная привязана к некоторому сорту. Некоторые из сортов имеют фиксированную интерпретацию. Среди них вещественные числа 1Z и временной сорт Т. Для логики FOTL понятия интерпретации, модели, выполнимости и истинности имеют те же значения, что и для логики предикатов первого порядка. Исключение составляют несколько символов словаря, имеющих фиксированную интерпретацию.

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

на несколько этапов:

• синтаксический анализ формулы;

• элиминация кванторов над абстрактными переменными;

• элиминация функциональных символов;

• элиминация временных переменных;

• получение результата проверки в виде истинностного значения.

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

В Заключении приведен список основных результатов, полученных в работе. Приложение А содержит грамматику языка спецификации ASM с временем. В Приложении Б описана грамматика языка задания свойств на основе логики FOTL. Приложения В и Г содержат примеры спецификаций с применением разработанного языка ASM с временем. В Приложении Д приводится руководство пользователя программной реализации разработанной системы.

Цитированная литература

[1] Агафонов, В. Н. Спецификация программ: понятийные средства и их организация / В. Н. Агафонов. — Новосибирск: Наука, 1990.— 224 с.

[2] Баранов, С. Н. Индустриальная технология автоматизации тестирования мобильных устройств на основе верифицированных поведенческих моделей проектных спецификаций требований / С. Н. Баранов, В. П. Котляров, А. А. Летичевский // Материалы международной научной конференции «Космос, астрономия и программирование» (Лавровские чтения), СПбГУ, Санкт-Петербург. — 2008. — С. 134-145.

[3] Соловьев, И. П. Формальные спецификации вычислительных систем. Машины абстрактных состояний (машины Гуревича) / И. П. Соловьев. - Издательство СПбГУ, 1998. — 32 с.

[4] Anlaujf, М. XASM — an extensible, component-based ASM language / M. Anlauff // Abstract State Machines, Theory and Applications, International Workshop, ASM 2000, Monte Verity Switzerland, March 19-24, 2000 / Ed. by Y. Gurevich, P. W. Kutter, M. Odersky, L. Thiele. - Vol. 1912 of Lecture Notes in Computer Science. — Springer, 2000. — Pp. 69-90.

[5] AsmL: The Abstract State Machine Language, Foundations of Software Engineering — Microsoft Research, 2002. — October, http://research. microsoft.com/fse/asml/.

[6] Beauquier, D. Decidable verification for reducible timed automata specified in a first order logic with time / D. Beauquier, A. Slissenko // Theor. Com-put. Sci. - 2002,- Vol. 275, no. 1-2. - Pp. 347-388.

[7] Beauquier, D. A first order logic for specification of timed algorithms: Basic properties and a decidable class / D. Beauquier, A. Slissenko // Annals of Pure and Applied Logic. - 2002. - Vol. 113, no. 1-3. - Pp. 13-52.

[8] Borger, E. Logic programming: The evolving algebra approach. / E. Borger // IFIP 13th World Computer Congress / Ed. by B. Pehrson, I. Simon.— Vol. I: Technology/Foundations. — Elsevier, Amsterdam, the Netherlands: 1994.-Pp. 391-395.

[9] Borger, E. Report on a practical application of AS Ms in software design / E. Borger, P. Pappinghaus, J. Schmid // Abstract State Machines, Theory and Applications, International Workshop, ASM 2000, Monte Verity Switzerland, March 19-24, 2000, Proceedings / Ed. by Y. Gurevich,

P. W. Kutter, M. Odersky, L. Thiele. - Vol. 1912 of Lecture Notes in Computer Science. — Springer, 2000. — Pp. 361-366.

[10] Börger, E. Abstract State Machines: A Method for High-Level System Design and Analysis / E. Börger, R. Stärk. — Springer-Verlag, Berlin, 2003. — 440 pp.

[11] Castillo, G. D. Towards comprehensive tool support for abstract state machines: The ASM workbench tool environment and architecture / G. D. Castillo // Applied Formal Methods - FM-Trends'98 / Ed. by D. Hut-ter, W. Stephan, P. Traverso, M. Ullmann. — Vol. 1641 of Lecture Notes in Computer Science. — Springer-Verlag, 1998. — Pp. 311-325.

[12] Cohen, J. On verification of refinements of timed distributed algorithms / J. Cohen, A. Slissenko // Proc. of the Intern. Workshop on Abstract State Machines (ASM'2000), March 20-24, 2000, Switzerland, Monte Verita, Tici-no. Lect. Notes in Comput. Sei., vol. 1912 / Ed. by Y. Gurevich, P. Kutter, M. Odersky, L. Thiele. - Springer-Verlag, 2000,- Pp. 34-49.

[13] Dijkstra, E. W. The structure of the "THE'-multiprogramming system / E. W. Dijkstra // Communications of the ACM.— 1968, May. — Vol. 11, no. 5.-Pp. 341-346.

[14] Emerson, E. A. Temporal and modal logic / E. A. Emerson // Handbook of Theoretical Computer Science / Ed. by J. van Leeuwen.— New York, N.Y.: Elsevier Science Publishers B.V.: Amsterdam, The Netherlands, 1990,- Vol. B: Formal Models and Semantics. - Pp. 996-1072.

[15] Farahbod, R. CoreASM: An extensible ASM execution engine / R. Farahbod, V. Gervasi, U. Glässer // Abstract State Machines. - 2005. - Pp. 153-166.

[16] Graf, S. Time in state machines / S. Graf, A. Prinz // Fundam. Inform. — 2007,- Vol. 77, no. 1-2. - Pp. 143-174.

[17] Gurevich, Y. Evolving algebras 1993: Lipari Guide / Y. Gurevich // Specification and Validation Methods / Ed. by B. Egon. — Oxford University Press, 1995.-Pp. 9-36.

[18] Gurevich, Y. Sequential abstract-state machines capture sequential algorithms / Y. Gurevich // ACM Transactions on Computational Logic.— 2000.-July. - Vol. 1, no. 1. - Pp. 77-111.

[19] Gurevich, Y. The railroad crossing problem: An experiment with instantaneous actions and immediate reactions / Y. Gurevich, J. Huggins // Proceed-

ings of CSL'95 (Computer Science Logic). - Vol. 1092 of LNCS. - Springer, - 1996. - Pp. 266-290.

[20] Guttag, J. V. Abstract data types and software validation / J. V. Guttag, E. Horowitz, D. R. Musser // CACM.- 1978.-Dec. - Vol. 21, no. 12.-Pp. 1048-1064.

[21] Ouimet, M. Timed abstract state machines: An executable specification language for reactive real-time systems: Tech. rep. / M. Ouimet, M. Nolin, K. Lundqvist: Massachusetts Institute of Technology, Cambridge, 2006.

[22] Schmid, J. Introduction to AsmGofer: Tech. rep. / J. Schmid: Siemens Corporation, 2001.

[23] Soloviev, I. The language of interpreter of distributed abstract state machines / I. Soloviev, A. Usov // Tools for Mathematical Modeling. Mathematical Research. - 2003. - Vol. 10. - Pp. 161-170.

[24] Univ. of Michigan, ASM homepage, http://www.eecs.umich.edu/gasm/.

[25] Using abstract state machines at Microsoft: A case study / M. Barnett, E. Bôrger, Y. Gurevich et al. // Abstract State Machines, Theory and Applications, International Workshop, ASM 2000, Monte Verità, Switzerland, March 19-24,2000, Proceedings / Ed. by Y. Gurevich, P. W. Kutter, M. Oder-sky, L. Thiele. — Vol. 1912 of Lecture Notes in Computer Science. — Springer, 2000.-Pp. 367-379.

[26] Wirth, N. Program development by stepwise refinement / N. Wirth // Communications of the Association of Computing Machinery. — 1971. — April. — Vol. 14, no. 4. - Pp. 221-227.

Работы автора по теме диссертации по годам

1. П. Васильев, И. Соловьев, А. Усов. Разработка распределенной системы электронных торгов с использованием методов формальной спецификации вычислительных систем // Материалы межвузовской конференции в области современных технологий программирования компании Microsoft, 2-4 декабря 2002, С. 23.

2. П. Васильев, И. Соловьев. Применение инженерии знаний в спецификации программных проектов // Журнал «Компьютерные инструменты в образовании», С.-Петербург, №6, 2003, С. 25-34.

3. П. Васильев. Разработка и верификация спецификаций программных продуктов, основанная на знаниях предметной области // Материалы Санкт-Петербургского конкурса-конференции для студентов, аспирантов и молодых ученых. Санкт-Петербург, декабрь 2003, С. 20.

4. P. Vasilyev. Simulator for Real-Time Abstract State Machines // Proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, In conjunction with ICEIS 2006, Paphos, Cyprus, May 2006, pp. 202-205.

5. P. Vasilyev. Simulator for Real-Time Abstract State Machines // Proceedings of the 4th International Conference on Formal Modeling and Analysis of Timed Systems, Paris, France, September 25-27, 2006, pp. 337-351.

6. P. Vasilyev. Simulator-Model Checker for Reactive Real-Time Abstract State Machines // Proceedings of the ASM'07 the 14th International ASM Workshop (http://ikt.hia.no/asm07/), Grimstad, Norway, 2007.

7. П. Васильев. Расширение языка машин абстрактных состояний Гуреви-ча рациональным временем // Вестник С.-Петерб. ун-та. Сер. 10. 2007. Вып. 4. С. 128-140.

8. П. Васильев. Применение расширенного языка абстрактных машин Гу-ревича с временем для спецификации протокола IEEE 1394 Root Contention // Материалы конференции «Научное программное обеспечение в образовании и научных исследованиях», СПбГПУ, Санкт-Петербург, 2008. С. 15-21.

9. П. Васильев. Верификация FOTL-свойств машин абстрактных состояний Гуревича с временем // Материалы конференции «Процессы управления и устойчивость», СПбГУ, Санкт-Петербург, 2008. С. 302-307.

10. П. Васильев. Задача спецификации протокола выбора корневого устройства стандарта IEEE 1394 на языке абстрактных машин Гуревича с временем // Материалы международной научной конференции «Космос, астрономия и программирование» (Лавровские чтения), СПбГУ, Санкт-Петербург, 2008. С. 32-43.

Подписано в печать 10.10.2008. Формат 60x84/16 Отпечатано с готового оригинал-макета в типографии ЗАО «КопиСервис». Печать ризографическая. Заказ № 1/1010. П. л. 1.0. Уч.-изд. л. 1.0. Тираж 100 экз.

ЗАО «КопиСервис» Адрес: 197376, Санкт-Петербург, ул. Проф. Попова, д. 3. тел.: (812) 327 5098

Введение .б

Глава 1. Расширение ASM временем

1.1. Метод ASM.

1.2. ASM Гуревича.

1.3. Турбо ASM.

1.4. Временная модель для ASM

1.5. Задание внешних функций.

1.6. Задание временных задержек

1.7. Раскрытие недетерминизмов.

Глава 2. Синтаксис и семантика языка ASM с временем

2.1. Синтаксис ASM с временем.

2.2. Семантика языка ASM с временем

2.3. Алгоритмы интерпретации

Глава 3. Проверка свойств ASM с временем

3.1. Временная логика первого порядка FOTL

3.2. Пример свойств ASM на языке FOTL.

3.3. Проверка FOTL-свойств

3.4. Пример спецификации FOTL-свойства

3.5. Алгоритмы проверки FOTL-свойств.

Глава 4. Архитектура интерпретатора ASM с временем

4.1. Ядро интерпретатора

4.2. Синтаксический анализатор входного языка

4.3. Загрузчик параметров выполнения

4.4. Хранилище трасс выполнения

4.5. Интерпретатор ASM.

4.6. Подсистема проверки FOTL-свойств

4.7. Графический интерфейс пользователя

4.8. Пример интерпретации спецификации

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

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

Формализм машин абстрактных состояний (abstract state machines или ASM [71]) был введен в начале 1990-х годов Юрием Гуревичем. Изначально известные под именем развивающиеся или эволюционирующие алгебры (evolving algebras), машины Гуревича фактически стали одним из методов формальной спецификации компьютерных систем. Некоторые идеи метода ASM в виде отдельных концепций уже были известны на момент его создания: псевдокод, концепции виртуальных машин компании IBM и абстрактных машин Дейкстры [58], а также структуры Тарского [76] как наиболее общий метод представления абстрактных состояний некоторых вычислений. Метод ASM объединяет и развивает достоинства перечисленных концепций. С одной стороны, метод ASM является простым и понятным для пользователя, с другой, он позволяет разрабатывать крупномасштабные приложения. В качестве основных идей ASM включает в себя определение локального замещения абстрактного состояния некоторого вычисления (локальное изменение интерпретаций функциональных символов или, другими словами, переопределение значений интерпретирующих функций в отдельных точках), метод последовательного уточнения спецификации Н. Вирта [116] и концепцию базовой модели (ground model [45, 46]), т. е. модель, полученную в результате формализации исходных требований пользователя.

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

Язык ASM, который используется нами в качестве основы языка спецификации, обладает большой выразительной силой. Даже его подмножество, охватывающее простейшие ASM (Basic ASMs [72]), позволяет описать любую алгоритмическую машину состояний, включая машину Тьюринга. Формализм ASM помогает понять и специфицировать задачу как с точки зрения технологии программирования, так и математической логики. Методология ASM нашла свое применение в таких практических задачах, как спецификация семантики языков VHDL, С, С++, Prolog, спецификация протоколов и других прикладных задач (см. [52, 107]). Из более поздних работ, в которых был применен язык ASM, упомянем спецификацию формальной семантики языков Java [104] и С# [77], а также языка SDL 2000 [66]. Та же методология была успешно применена в создании промышленных компьютерных систем, например, в проекте FALKO [48] компании Siemens (программное обеспечение для разработки и верификации расписаний железнодорожных линий). Еще одним примером применения машин Гуревича в промышленном масштабе является разработанная в компании Microsoft система AsmHugs [108], предназначенная для валидации технологий Microsoft, в частности модели СОМ. В качестве основных аргументов в пользу ASM разработчики упоминают выполнимость спецификаций, возможность моделирования на различных уровнях абстракции, а также формальный переход от одного уровня абстракции к другому [98].

В настоящее время известен целый ряд реализаций интерпретаторов и компиляторов для различных диалектов языка ASM. Первый компилятор для ASM был реализован Анжеликой Каппель на языке Пролог в 1990 году [83]. Примерно в это же время одним из студентов мичиганского университета было разработано ядро первого интерпретатора ASM на языке Си [70]. На основе этого ядра можно построить полноценный интерпретатор. В настоящее время известен целый ряд реализаций интерпретаторов и компиляторов для различных диалектов языка ASM: Microsoft AsmL (Spec Explorer [32]), XASM [31], CoreASM [63], Timed ASM (TASM) [96], ASMETA [64], Distributed ASML [103], ASM Workbench [53], ASM Gofer [101].

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

Существует два основных подхода к решению задачи формальной верификации: модельный и доказательный. При доказательном (или логическом) подходе в некоторой логике строится теория, описывающая разрабатываемую систему. Ограничительные свойства, накладываемые на систему, описываются в виде формул этой же теории. Верификация при таком подходе сводится к доказательству истинности рассматриваемых свойств в рамках разработанной теории. Часто полученные теории являются неразрешимыми, поэтому средства автоматизации процесса доказательства, такие, как HOL [90], PVS [97], KIV [106], Coq [95], Larch Prover [65], используют различные стратегии поиска доказательств, которые не всегда приводят к успеху. Поэтому при верификации с помощью таких инструментальных средств часто требуется вмешательство пользователя для выбора того или иного метода или стратегии доказательства. Таким образом, процесс верификации при доказательном подходе обычно является полуавтоматическим.

При модельном подходе верифицирующая система (модельный верификатор или model checker) проверяет, удовлетворяет ли спецификация системы исходным требованиям. Изначально проверка на модели подразумевала в качестве спецификации системы использовать конечные автоматы (finite state machines), но при введении времени и параметров множество состояний модели становится бесконечным. Для того, чтобы применить методы проверки на модели, их необходимо адаптировать к рассматриваемому классу задач и разработать методы сокращения множества состояний модели.

Проектирование и реализация компьютерных систем с ограничениями на время реакции, которые рассматриваются в данной работе, предусматривают необходимость реализации подходящего механизма работы с временными значениями и входными данными. Исходный формализм ASM не предусматривает встроенной временной модели, однако, существует ряд работ, предлагающих варианты решения этой задачи. Впервые решение проблемы предложили Гуревич и Хаггинс [73], которые представили вычисления в виде отображения из области временных значений в область состояний ASM. Затем последовали работы [43, 55], в которых проблема верификации временных алгоритмов сводится к верификации формальных спецификаций в виде формул специальной временной логики первого порядка FOTL (First Order Timed Logic). Логика FOTL введена D. Beauquier и A. Slissenko в работах [40, 42] как метод спецификации алгоритмов и их свойств с непрерывным временем. В работах [41, 44] анализируются разрешимые подклассы логики FOTL.

Задачи, которые рассматриваются в данной работе, часто специфицируются с применением темпоральных логик. Для описания свойств спецификаций в формализме ASM требуется достаточно выразительный язык логики. Самым простым логическим языком является язык пропозициональной логики (логики высказываний [19]). Однако, нетрудно заметить, что язык классической пропозициональной логики плохо приспособлен для спецификаций систем с временем. Существует ряд расширений пропозициональной логики, такие как логики с временем, или темпоральные логики [61], которые обладают большей выразительной способностью. Это такие логики, как LTL

Linear Temporal Logic), CTL (Computational Tree Logic) или их модификации. Упомянутые логики широко используются для формальной спецификации программ и вычислительных систем. Среди программных инструментов, использующих темпоральные логики, можно выделить: STeP [105], SPIN [78], SMV [88], NuSSMV [94]. Хотя указанные логики и являются мощным инструментом формальной спецификации динамических систем, некоторые свойства, например, ограничения на время реакции системы, в них выразить очень сложно. В данной работе для спецификации свойств проектируемой системы применяется язык временной логики первого порядка FOTL, которая достаточно подробно описана в главе 3. FOTL является расширением теории со сложением вещественных чисел абстрактными функциями. С помощью языка FOTL можно компактно специфицировать сложные свойства поведения компьютерных систем во времени.

В некоторых работах, посвященных использованию времени в методе ASM, предлагается явное использование функции времени, например в работах [32, 68]. Кроме того, вводятся временные задержки на выполнение либо отдельных фрагментов вычислений, либо замещений [55, 96]. В перечисленных работах содержится множество идей и предложений по использованию и уточнению языка ASM, но, несмотря на это, в них не сформулирована явная методика спецификации систем с ограничениями на время реакции и последующей проверкой корректности их свойств.

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

Обзор существующих подходов и инструментов

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

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

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

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

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

Полученные несоответствия между смоделированной системой и ее практической реализацией могут выявить ряд ошибок, таких как: ошибки при создании кода программы, ошибки в модели программы, ошибки спецификации системы и логические ошибки дизайна проекта. Кроме языка AsmL данное средство разработки поддерживает язык спецификации Spec#, который является надстройкой языка

Extensible ASM. XASM [31] — расширяемый язык ASM. Реализован на основе работ [86] по структурированию и обобщению семантики ASM. Основное нововведение XASM — это понятие XASM-вызова (XASM call). В остальном разработчики попытались минимизировать изменения метода ASM. Обобщение определения машины Гуревича в подходе XASM заключается в том, что каждое выражение или конструкция языка имеет как возвращаемый результат вычислений, так и множество замещений (точечных изменений состояния вычисления). Напомним, что в определении машины Гуревича подразумевается, что только выражения имеют некоторый возвращаемый результат вычислений, а правила ничего не возвращают, но образуют множество замещений интерпретаций функций ASM.

В языке XASM расширено понятие внешней функции (external function). Внешние функции метода ASM предназначены возвращать текущую интерпретацию. В языке XASM внешние функции получают побочный результат — множество замещений. Таким образом, внешние функции соответствуют процедурам в императивных языках программирования. Кроме внешних функций XASM дополнен функциями окружения, которые позволяют вывести на внешний уровень результаты внутренних вычислений абстрактной машины для использования в дальнейших вычислениях. Функции окружения являются специальными динамическими функциями и задаются как начальные параметры для абстрактной машины. Используя вышеперечисленные типы функций можно, рассматривать вычисление некоторой внешней функции как вызов соответствующей абстрактной подмашины, а функции окружения в этот момент играют роль параметров, передаваемых вызываемой подмашине. С помощью понятия XASM-вызова значительно упрощается процесс- спецификации сложных систем, так как появляется возможность разделять модель системы на модули, которые оформляются в виде подмашин ASM. Следует заметить, что такая концепция модульности близка общим тенденциям разработки и развития программного обеспечения. Разработчики XASM старались следовать исходным идеям Гуревича и минимизировали количество дополнений метода ASM (по сути только одно), что позволяет эффективно использовать данный метод спецификации.

CoreASM. CoreASM [63] — проект, состоящий из расширяемого ядра для интерпретации языка ASM и вспомогательного программного обеспечения, позволяющего разрабатывать спецификации, а также проводить необходимую отладку и верификацию полученных абстрактных моделей. Областью применения системы CoreASM является широкий круг задач, включая распределенные и встроенные системы. Программная реализация состоит из платформонезависимого ядра, выполняющего спецификации на языке CoreASM. Ядро дополняется графическим интерфейсом пользователя, предназначенным для интерактивной визуализации и управления выполнением спецификации. Ядро системы CoreASM рассчитано на дальнейшее расширение такими функциональными возможностями, как проверка модели или создание тестового покрытия.

Основная часть инструментального средства CoreASM — это его функциональное ядро (CoreASM engine), которое состоит из четырех компонентов: синтаксического анализатора, интерпретатора, планировщика и абстрактного хранилища. Эти компоненты осуществляют выполнение спецификации ASM, а управление процессом выполнения осуществляется через программный интерфейс, который определяет такие функции, как загрузка спецификации, старт выполнения, выполнение одного шага спецификации. Задача синтаксического анализатора — анализ исходной спецификации и создание аннотированного дерева. Интерпретатор занимается анализом правил замещения и созданием множеств замещения. Абстрактное хранилище собирает всю историю состояний ASM, включая текущее состояние, что позволяет анализировать ход выполнения, передавать информацию дополнительным инструментальным средствам или совершать откат состояния абстрактной машины на несколько шагов назад. Планировщик управляет всем процессом взаимодействия компонентов системы. Он обрабатывает такие события, как случаи возникновения несовместного изменения состояния, а в случае распределенных ASM планировщик выбирает множество агентов для выполнения следующего шага программы. Основным преимуществом подхода CoreASM является концепция расширяемости, которая реализуется через механизм дополнений. Дополнения могут добавлять новые грамматические правила для синтаксического анализатора, семантические правила для интерпретатора, новые операции для абстрактного хранилища, а также новые схемы работы для планировщика. Ядро системы поддерживает минимальный набор базовых операций, словарь языка включает такие константы, как undef, true, false, сорт Boolean, универсум Agents. Зарезервированная функция program ссылается на программу агента, а ссылка self указывает на текущего агента, в правиле которого она используется. Также определен предикат равенства. Любые конструкции языка, включая условные правила замещения, блоки параллельных операторов, операцию выбора choose, итератор forall подключаются при необходимости. Кроме набора базовых возможностей языка ASM существуют дополнения для работы с Турбо ASM [51], циклами, математическими функциями, а также операции с коллекциями (списками, множествами, очередями, стеками) и операции ввода/вывода.

Timed ASM. Timed ASM (TASM) [96] — проект, разработанный в лаборатории встроенных систем массачусетского института технологий (MIT), нацеленный на адаптацию метода ASM к спецификации реактивных систем реального времени. Проект TASM включает в себя язык спецификации и программные средства для разработки и интерпретации спецификаций. В основе языка TASM лежат языки ASM и XASM. Для взаимодействия между отдельными ASM используется техника в стиле CCS [89] (Calculus of Communication Systems), т. е. с помощью передачи сообщений через каналы связи.

Спецификация системы на языке TASM состоит из спецификации окружения (множество функций и множество типов) и спецификации самой ASM, состоящей из множества входных переменных MV (monitored variables), контролируемых переменных CV (controlled variables) и набора правил перехода вида if С then А, где С — охраняющее условие, а А — действие (action). Под действием подразумевается замещение вида v := expr, где v принадлежит множеству CV, а ехрг является вычислимым выражением того же типа, что и v, так как язык TASM является строго типизированным.

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

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

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

ASM-SL и система ASM Workbench. Язык ASM-SL [53] (ASM-bascd Specification Language) является одним из диалектов языка ASM и предназначен для спецификации программных систем для инструментального средства ASM Workbench. ASM-SL развивает метод ASM для решения практических задач. Основными свойствами подхода ASM-SL являются строгая система типов, состоящая из множества предопределенных элементарных типов (булевы значения, целые числа, числа с плавающей точкой, строки) и предопределенных структур данных (кортежи, списки, конечные множества, отображения) вместе с конструкторами для построения новых типов данных. Кроме перечисленного язык ASM-SL поддерживает рекурсивные определения функций, операции сопоставления с образцом, операции над множествами.

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

ASM Workbench представляет собой набор прикладных инструментальных средств, состоящий из ядра системы и нескольких конвертеров для обмена данными с другими компонентами в текстовом формате. Компоненты инструментального средства включают в себя подсистему проверки типов, интерпретатор и графический интерфейс пользователя для отладочных целей. Кроме того разрабатывается генератор кода для виртуальной машины Java и интерфейс взаимодействия с верификатором SMV [87].

Distributed ASML. Distributed ASML (язык распределенных ASM) — объектно-ориентированный язык, предназначенный для разработки спецификаций сложных динамических, в том числе распределенных, систем. Предлагаемый язык спецификации распределенных MAC достаточно близок по синтаксису к языку AsmL, предложенному в рамках проекта компании Microsoft, но является частью комплексного проекта по созданию расширяемой инструментальной среды разработки и анализа выполнимых формальных спецификаций iDASML [109]. Язык распределенных ASM основан на концепциях распределенных ASM, изложенных в работах [67]. Он поддерживает объектно-ориентированные конструкции, структурную организацию проекта, пространства имен. Распределенные системы реализуются с помощью агентов, которые имеют свое собственное внутреннее состояние. Агенты работают независимо и умеют взаимодействовать с окружением и друг с другом. С точки зрения метода ASM, агент соответствует подмашине абстрактных состояний, а в языке DASML он описывается в объектно-ориентированном стиле с помощью «класса» со своими полями и методами. К синтаксическим особенностям DASML можно отнести (в отличие от AsmL) использование скобочной записи для обозначения блоков параллельных и последовательных вычислений.

ASMETA. Проект ASMETA предлагает метамодель для семейства языков ASM, основанную на подходе Model Driven Engineering (MDE). Метамодель ASM (AsmM) отображает концепции и конструкции формального метода ASM в абстрактном виде. Она обладает простой для восприятия обычных пользователей стандартной графической нотацией.

В связи с расширением применения метода ASM были разработаны средства интерпретации, тестирования, механической верификации спецификаций с помощью доказательства теорем и проверки модели. Недостатком большинства таких систем является их узкая специализация, ориентация на решение отдельных задач. Таким образом, разработчик вынужден пользоваться набором инструментальных средств с разными возможностями, архитектурой, синтаксисом и даже семантикой. Сложности с комбинированием различных средств и подходов делают их использование неэффективным в полном цикле разработки программного обеспечения. Можно использовать конвертеры при переходе от одного инструментального средства к другому, но кроме синтаксических различий в диалектах языка ASM необходимо анализировать семантические особенности и настройки окружения. Метамодель ASM предлагает использовать промежуточный способ хранения совокупных метаданных о каждом из возможных языков ASM, таким образом решая упомянутые проблемы перехода. Для каждого из используемых языков строится его метамодель в общих для AsmM абстрактных терминах. Далее строится отображение из метамодели конкретного языка в опорную метамодель. Таким образом, AsmM представляет опорную метамодель для семейства языков на основе метода ASM. AsmM включает в себя следующее: определение абстрактного синтаксиса в соответствии с метаязыком Meta Object Facility (MOF), абстрактное и графическое описания основных понятий данного метода и конструкций, синтаксис обмена данными для разных подходов и конкретный синтаксис в виде текста грамматики.

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

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

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

Для достижения обозначенных целей были поставлены следующие задачи:

• разработка временной модели для ASM, синтаксиса и семантики расширенного временем языка ASM;

• разработка метода проверки свойств на языке FOTL применительно к спецификации на расширенном языке;

• разработка и реализация программной системы интерпретации расширенного языка ASM и проверки ограничительных свойств.

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

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

В первой главе вводятся основные понятия, относящиеся к методу ASM. Сначала описывается исходная концепция ASM Гуревича (GASM), затем методы расширения синтаксиса и семантики языка спецификаций. В целом, спецификацию системы с временными ограничениями можно задать парой < ENV, ASMSPEC >, где ENV — это спецификация окружения, которая содержит определения функций окружения, значения задержек для различных операций языка, а также функцию, определяющую способ раскрытия недетерминизмов, a ASMSPEC — это спецификация машины абстрактных состояний Гуревича с временем. ASM с временем, в свою очередь, можно задать тройкой < VOC, IN IT, PROG >, где VOC — словарь функциональных символов, INIT — описание начального состояния машины и PROG — ее программа. Словарь ASM состоит из множества сортов, множества функциональных символов и множества предикатных символов. Некоторые из них имеют фиксированную интерпретацию, например: 7Z — сорт вещественных чисел, Z — сорт целых чисел, М — сорт натуральных чисел, BOOL — сорт булевых значений, Т = 71+ — выделенный сорт значений времени, UNDEF = {undef} — специальный сорт, содержащий одно значение, применяющийся для задания неопределенных значений. Метод ASM позволяет использовать несколько уровней абстракции спецификаций, поэтому на самом высоком уровне абстракции сорт вещественных чисел является математическим множеством вещественных чисел. При переходе на более низкие уровни абстракции базовый сорт может быть уточнен, так на уровне реализации вступают в силу программно-аппаратные ограничения конкретной компьютерной системы. В частности, разработанный интерпретатор в качестве уточнения сорта вещественных чисел использует подмножество рациональных чисел, предоставляемое языком реализации.

Далее описываются дополнительные возможности расширенного языка ASM, ориентированного на спецификацию класса систем с ограничениями по времени. Метод ASM не предполагает фиксированной временной модели, так как является универсальным методом описания алгоритмов, поэтому для спецификации систем рассматриваемого класса вводится временная модель, адаптирующая универсальный метод ASM. В числе дополнений необходимо отметить специальное представление внешних функций, которые задают входные данные и формируют окружение. Определение внешних функций формулируется следующим образом. Рассмотрим внешнюю функцию f : X У и обозначим соответствующую ей функцию с временным параметром : Тх X —» У, где / — имя функции, X — абстрактный сорт или прямое произведение двух абстрактных сортов, Т — временной сорт, У — абстрактный сорт или сорт 7Z. Вариант функции с временным параметром /° непосредственно в программе ASM не используется, чтобы не усложнять семантику языка. Такие функции предназначены только для описания ограничений пользователя. Для определения внешних функций применяется следующий подход. Рассматривается некоторая интерпретация абстрактного конечного сорта X и множество элементов этой интерпретации нумеруется натуральными числами. Тогда для каждого элемента интерпретации значения некоторой функции / можно задать с помощью индексированной последовательности: f(i) := (t\, ft, 4, /J;.; 4, Л; • • •)> гДе « G 1,., n; п - мощность сорта Х\ t\, tl2,., tlk,. — начальные точки интервалов времени; /2, • — значения функции, определенные на интервалах. Начальные точки временных интервалов t\ пронумерованы в порядке возрастания. Также поддерживается спецификация функций от двух переменных, т. е. функций, заданных на прямом произведении двух абстрактных сортов Х'хХ". Тогда определение таких функций принимает вид: /(г, j) := (t\3, t?, ff].] t^, ff].), где г G 1,., n, j G 1,., m\ n — мощность сорта Л"; m — моищость сорта Х"\ остальные обозначение аналогичны использованным в описании одноместной функции.

Далее в этой главе описываются методы приписывания временных задержек операциям языка спецификации с временем. Для обозначения задержек введем функцию 5. Будем считать, что функция задержки задана на множестве правильных предложений языка спецификации и действует в множество временных значений Т. Пусть S — множество всевозможных предложений языка. Тогда тип функции задержки будет выглядеть следующим образом: S : S —> Т. Для каждой базовой операции или конструкции значение функции 5 явно задается пользователем и используется интерпретатором для расчета задержек более сложных предложений языка. Чтобы получить задержку суперпозиции синтаксических конструкций Pi и Р2, например, последовательного блока {Р1Р2}, необходимо просуммировать значения задержек всех его составляющих замещений: S({PiP2}) = + Исключением является случай параллельного замещения, к примеру, [Р1Р2]. В данном случае задержка вычисляется как максимальная задержка среди замещений в параллельном блоке, т. е. ^([PiP2]) = max{(5(Pi), д(Р2)}.

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

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

Семантика языка ASM с временем значительно отличается от семантик других известных языков, основанных на методе ASM. Синтаксически конструкции языка выглядят привычным образом, но операции языка имеют ряд дополнительных побочных эффектов. Так, все арифметические действия и операции чтения/записи имеют побочный эффект: изменение состояния глобального счетчика времени. Следовательно, при переходе к следующему состоянию глобальной ASM могут измениться значения внешних функций, что в свою очередь может повлечь за собой изменение потока управления. Модифицирована также семантика условных операторов цикла, которые при определенных условиях выполнения должны «предвидеть» будущие изменения интерпретаций внешних функций.

В третьей главе описывается метод проверки свойств спецификаций ASM, представленных в виде формул языка некоторой логики. В данной работе была выбрана подходящая для этих целей логика первого порядка с временем FOTL [43]. Приводится описание логики FOTL, описываются ее синтаксические и семантические особенности. Словарь FOTL состоит из конечного числа сортов, функциональных и предикатных символов. Каждая переменная привязана к некоторому сорту. Некоторые из сортов имеют фиксированную интерпретацию. Среди них вещественные числа Л и временной сорт Т. Для логики FOTL понятия интерпретации, модели, выполнимости и истинности имеют те же значения, что и для логики предикатов первого порядка. Исключение составляют несколько символов словаря, имеющих фиксированную интерпретацию.

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

• синтаксический анализ формулы;

• элиминация кванторов над абстрактными переменными;

• элиминация функциональных символов;

• элиминация временных переменных;

• получение результата проверки в виде истинностного значения.

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

В Заключении приведен список основных результатов, полученных в работе. Приложение А содержит грамматику языка спецификации ASM с временем. В Приложении Б описана грамматика языка задания свойств на основе логики FOTL. Приложения В и Г содержат примеры спецификаций с применением разработанного языка ASM с временем. В Приложении Д приводится руководство пользователя программной реализации разработанной системы.

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

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

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

Перечислим основные результаты работы.

• разработана временная модель ASM с непрерывным временем для спецификации компьютерных систем с ограничениями на время реакции;

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

Заключение

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

• разработана временная модель ASM с непрерывным временем для спецификации компьютерных систем с ограничениями на время реакции;

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

• разработан синтаксис языка описания временных ограничений на базе языка временной логики первого порядка FOTL;

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

• разработан алгоритм проверки свойств трасс выполнения спецификаций в виде формул логики FOTL без вхождения внешних функций и в случае кусочно-постоянных внешних функций;

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

1. Агафонов, В. Н. Спецификация программ: понятийные средства и их организация / В. Н. Агафонов. — Новосибирск: Наука, 1990. — 224 с.

2. Агафонов, В. П. Надъязыковая методология спецификации программ / В. Н. Агафонов // Программирование. — 1993.— С. 28-48.

3. Баранов, С. Н. Процесс разработки программ как основа профессиональной деятельности программистов / С. Н. Баранов // Компьютерные инструменты в образовании. — 2002. — № 34.

4. Васильев, П. К. Расширение языка машин абстрактных состояний Гу-ревича рациональным временем / П. К. Васильев // Вестник Санкт-Петербургского университета. Сер. 10. Вып. 2007.— С. 128-140.

5. Васильев, П. К. Верификация FOTL-свойств машин абстрактных состояний Гуревича с временем / П. К. Васильев // Материалы конференции «Процессы управления и устойчивость». — СПбГУ, Санкт-Петербург: 2008. С. 302-307.

6. Васильев, П. К. Пример спецификации протокола выбора главного устройства стандарта IEEE 1394 на языке абстрактных машин Гуревича с временем / П. К. Васильев // Вестник Санкт-Петербургского университета. Сер. 10. Вып. ^. — 2008.— С. 126-138.

7. Васильев, П. К. Применение инженерии знаний в спецификации программных проектов / П. К. Васильев, И. П. Соловьев // Журнал «Компьютерные инструменты в образовании». — 2003. — № 6. — С. 25-34.

8. Верификационная технология базовых протоколов для разработки и проектирования программного обеспечения / С. Н. Баранов, П. Д. Дро-бинцев, А. А. Летичевский, В. П. Котляров // Программные продукты и системы. — 2005. — № 1. — С. 25-28.

9. Замулин, А. В. Родовые средства в объектно-ориентированных машинах абстрактных состояний / А. В. Замулин // Препринт / Под ред. JI. Карева. — Новосибирск: Институт систем информатики им. А.П. Ершова, РАН Сибирское Отделение, 1999. — 29 с.

10. Замулин, А. В. Формальные методы спецификации программ / А. В. Замулин. — Новосибирск: Новосибирский государственный университет, 2002. — 93 с.

11. Кознов, Д. Основы визуального моделирования / Д. Кознов. — Издательство «Бином. Лаборатория знаний», 2008. — 248 с.

12. Колмогоров, А. Н. Введение в математическую логику / А. Н. Колмогоров, А. Г. Драгалин. — Москва: Издательство МГУ, 1982.

13. Марков, А. А. Элементы математической логики / А. А. Марков.— Москва: Издательство МГУ, 1984.

14. Непомнящий, В. А. Новый язык В ASIC-REAL для спецификации и верификации моделей распределенных систем / В. А. Непомнящий, Н. В. Шилов, Е. В. Бодин // Препринт / Под ред. А. Шелухина. —

15. Новосибирск: Институт систем информатики им. А.П. Ершова, РАН Сибирское Отделение, 1999. — 40 с.

16. Покозий, Е. А. Метод верификации свойств параллелизма временных сетей петри / Е. А. Покозий // Препринт / Под ред. JI. Карева. — Новосибирск: Институт систем информатики им. А.П. Ершова, РАН Сибирское Отделение, 1999. — 30 с.

17. Процесс разработки программных изделий / С. Н. Баранов, А. Н. Дома-рацкий, Н. К. Ласточкин, В. П. Морозов. — Физматлит, Наука, 2000. — 176 с.

18. Соловьев, И. П. Формальные спецификации вычислительных систем. Машины абстрактных состояний (машины Гуревича) / И. П. Соловьев. Издательство СПбГУ, 1998. - 32 с.

19. Agafonov, V. N. The knowledge based system supporting work with precise definitions: Tech. Rep. 5 / V. N. Agafonov: Faculty of Applied Mathematics and Computing Science, Tver State University, Tver, 1995.

20. Alur, R. Model-checking in dense real-time / R. Alur, C. Courcoubetis, D. Dill // Information and Computation. — 1993. — Vol. 104. — Pp. 2-34.

21. Alur, R. A theory of timed automata / R. Alur, D. L. Dill // Theoretical Computer Science. 1994. - Vol. 126. - Pp. 183-235.

22. AsmL: The Abstract State Machine Language, Foundations of Software Engineering — Microsoft Research, 2002. — October, http://research, microsoft.com/fse/asml/.

23. Baier, C. Principles of Model Checking / C. Baier, J.-P. Katoen. — Cambridge, Massachusets: The MIT Press. — 975 pp.

24. Barnett, M. The ABCs of specification: AsmL, behavior, and components / M. Barnett, W. Schulte // Informatica (Slovenia). — 2001. — November.— Vol. 25, no. 4,- Pp. 517-526.

25. Beauquier, D. Automatic verification of real time systems: A case study / D. Beauquier, T. Crolard, E. Prokofieva // Third Workshop on Automated Verification of Critical Systems (AVoCS'2003). — University of Southampton, 2003. Pp. 98-108.

26. Beauquier, D. Decidable verification for reducible timed automata specified in a first order logic with time / D. Beauquier, A. Slissenko // Theor. Corn-put. Sci. 2002. - Vol. 275, no. 1-2. - Pp. 347-388.

27. Beauquier, D. A first order logic for specification of timed algorithms: Basic properties and a decidable class / D. Beauquier, A. Slissenko // Annals of Pure and Applied Logic. 2002. - Vol. 113, no. 1-3. - Pp. 13-52.

28. Beauquier, D. Periodicity based decidable classes in a first order timed logic / D. Beauquier, A. Slissenko // ANNALSPAL: Annals of Pure and Applied Logic. 2006. - Vol. 139. - Pp. 43-73.

29. Borger, E. Logic programming: The evolving algebra approach. / E. Borger // IFIP 13th World Computer Congress / Ed. by B. Pehrson, I. Simon.— Vol. I: Technology/Foundations.— Elsevier, Amsterdam, the Netherlands: 1994. Pp. 391-395.

30. Borger, E. The bakery algorithm: yet another specification and verification / E. Borger, Y. Gurevich, D. Rosenzweig // Specification and Validation Methods / Ed. by E. Borger. — Oxford University Press, 1995. — Pp. 231-243.

31. Borger, E. Capturing requirements by abstract state machines: The light control case study / E. Borger, E. Riccobene, J. Schmid // JUCS: Journal of Universal Computer Science. — 2000. — July. — Vol. 6, no. 7. — Pp. 597620.

32. Borger, E. A mathematical definition of full Prolog / E. Borger, D. Rosenzweig // Science of Computer Programming.— 1995.— June. — Vol. 24, no. 3. Pp. 249-286.

33. Borger, E. Composition and submachine concepts for sequential ASMs /

34. Borger, E. Abstract State Machines: A Method for High-Level System Design and Analysis / E. Borger, R. Stark. — Springer-Verlag, Berlin, 2003. — 440 pp.

35. Comon, H. Timed automata and the theory of real numbers / H. Comon, Y. Jurski // CONCUR'99, LNCS 1664. Springer, 1999.- Pp. 242-257.

36. Derrick, J. Refinement in Z and Object-Z: Foundations and Advanced Applications / J. Derrick, E. Boiten. Formal Approaches to Computing and Information Technology. — Springer, 2001. — May. — 466 pp.

37. Dijkstra, E. W. The structure of the "THE'-multiprogramming system / E. W. Dijkstra // Communications of the ACM. — 1968, May. — Vol. 11, no. 5. Pp. 341-346.

38. Dijkstra, E. W. The discipline of programming / E. W. Dijkstra. — Prentice-Hall, 1976. 217 pp.

39. Dolzmann, A. Real quantifier elimination in practice / A. Dolzmann, T. Sturm, V. Weispfenning // Algorithmic Algebra and Number Theory. — Springer, 1998. Pp. 221-247.

40. Emerson, E. A. Automated temporal reasoning about reactive systems / E. A. Emerson // Banff Higher Order Workshop / Ed. by F. Moller, G. M. Birtwistle. — Vol. 1043 of Lecture Notes in Computer Science. — Springer, 1995. Pp. 41-101.

41. Farahbod, R. CoreASM: An extensible ASM execution engine / R. Farah-bod, V. Gervasi, U. Glasser // Abstract State Machines. — 2005. — Pp. 153166.

42. Glasser, U. The formal semantics of SDL-2000: Status and perspectives / U. Glasser, R. Gotzhein, A. Prinz // Computer Networks (Amsterdam, Netherlands: 1999). 2003. - June. - Vol. 42, no. 3. - Pp. 343-358.

43. Glasser, U. An abstract communication model: Tech. Rep. MSR-TR-2002-55 / U. Glasser, Y. Gurevich, M. Veanes: Microsoft Research, 2002.

44. Graf, S. Time in state machines / S. Graf, A. Prinz // Fundam. Inform. — 2007. Vol. 77, no. 1-2. - Pp. 143-174.

45. Guide to the Software Engineering Body of Knowledge / A. Abran, J. W. Moore, P. Bourque, R. Dupuis. — IEEE Computer Society, 2004. — 200 pp.

46. Gurevich, Y. Evolving algebras: an attempt to discover semantics / Y. Gurevich // Current trends in theoretical computer science. — 1992, — Pp. 266292.

47. Gurevich, Y. Evolving algebras 1993: Lipari Guide / Y. Gurevich // Specification and Validation Methods / Ed. by B. Egon. — Oxford University Press, 1995. Pp. 9-36.

48. Gurevich, Y. Sequential abstract-state machines capture sequential algorithms / Y. Gurevich // ACM Transactions on Computational Logic.— 2000. July. - Vol. 1, no. 1. - Pp. 77-111.

49. Gurevich, Y. The railroad crossing problem: An experiment with instantaneous actions and immediate reactions / Y. Gurevich, J. Huggins // Proceedings of CSL'95 (Computer Science Logic). Vol. 1092 of LNCS. -Springer, 1996.- Pp. 266-290.

50. Gurevich, Y. Semantic essence of asmL: Tech. Rep. MSR-TR-2004-27 / Y. Gurevich, B. Rossman, W. Schulte: Microsoft Research, 2004.

51. Guttag, J. V. Abstract data types and software validation / J. V. Guttag, E. Horowitz, D. R. Musser // CACM.- 1978. Dec. - Vol. 21, no. 12.-Pp. 1048-1064.

52. A high-level modular definition of the semantics of C# / E. Borger, N. G. Fruja, V. Gervasi, R. F. Stark // Theor. Comput. Sci- 2005.-Vol. 336, no. 2-3. Pp. 235-284.

53. Lamport, L. A new solution of Dijkstra's concurrent programming problem. / L. Lamport // Communications of ACM, 17(8). — 1974. — Pp. 453455.

54. McMillan, K. L. Symbolic Model Checking / K. L. McMillan. — Kluwer Academic Publishing, 1993.

55. McMillan, K. L. Symbolic Model Checking / K. L. McMillan. Norwell Massachusetts: Kluwer Academic Publishers, 1993.

56. Milner, R. Communication and Concurrency / R. Milner. International Series in Computer Science. — New York, NY: Prentice Hall, 1989. — 272 pp.

57. M.J.C. Gordon. HOL: A proof generating system for higher-order logic. / M.J.C. Gordon // VLSI Specification, Verification and Synthesis / Ed. by G.M. Birtwistle, P.A. Subrahmanyam. — Boston: Kluwer Academic Publishers, 1988. Pp. 73-128.

58. Morgan, D. Numerical Methods: Real-time and Embedded Systems Programming / D. Morgan. San Mateo, CA, USA: M&T Books, 1992. -P. 496.

59. Oostdijk, M. Proof by computation in the Coq system / M. Oostdijk,

60. H. Geuvers // Theoretical Computer Science. — 2002. — Vol. 272, no. 12. Pp. 293-314.

61. Ouimet, M. Timed abstract state machines: An executable specification language for reactive real-time systems: Tech. rep. / M. Ouimet, M. Nolin, K. Lundqvist: Massachusetts Institute of Technology, Cambridge, 2006.

62. Schmid, J. Introduction to AsmGofer: Tech. rep. / J. Schmid: Siemens Corporation, 2001.

63. Soloviev, I. The language of interpreter of distributed abstract state machines / I. Soloviev, A. Usov // Tools for Mathematical Modeling. Mathematical Research. — 2003. Vol. 10. — Pp. 161-170.

64. Stark, R. Java and the Java Virtual Machine: Definition, Verification, Validation / R. Stark, J. Schmid, E. Borger. — Springer-Verlag, Berlin, 2001. — 392 pp.

65. Step: The Stanford temporal proven Tech. rep. / Z. Manna, N. Bjrner, A. Browne et al: Stanford, CA, USA: Stanford University, 1994.

66. Univ. of Michigan, ASM homepage, http: //www. eecs. umich. edu/gasm/.

67. M. Odersky, L. Thiele. — Vol. 1912 of Lecture Notes in Computer Science. — Springer, 2000. Pp. 367-379.

68. Usov, A. Development of the Interpreter for Distributed ASMs / A. Usov // Electronic Notes in Theoretical Computer Science. — 2004. — 8 pp. http: //www.elsevier.com/locate/entcs.

69. Vasilyev, P. Simulator-model checker for reactive real-time abstract state machines / P. Vasilyev // Proceedings of the ASM'07 the 14th International ASM Workshop, Grimstad, Norway / Ed. by A. Prinz. — 2007. — 12 pp. http://ikt.hia.no/asm07/.

70. Weispfenning, V. Simulation and optimization by quantifier elimination /

71. V. Weispfenning // Journal of Symbolic Computation.— 1997.— Aug. — Vol. 24, no. 2. Pp. 189-208.

72. Weispfenning, V. Mixed real-integer linear quantifier elimination / V. Weispfenning // Proc. of the 1999 Int. Symp. on Symbolic and Algebraic Computations (ISSAC'99). ACM Press, 1999. - Pp. 129-136.

73. Wirth, N. Program development by stepwise refinement / N. Wirth // Communications of the Association of Computing Machinery.— 1971.— April. Vol. 14, no. 4. - Pp. 221-227.

74. Yavorskiy, R. Translation of a fragment of asmL specification language to higher order logic: Tech. Rep. MSR-TR-2003-22 / R. Yavorskiy: Microsoft Research (MSR), 2003.-April.

75. Zamulin, A. Typed gurevich machines revisited / A. Zamulin // Joint NCC & IIS Bulletin, Computer Science, Novosibirsk. — 1997. — no. 5. — Pp. 126.

76. Zamulin, A. Specification of dynamic systems by typed gurevich machines / A. Zamulin // Proceedings of the 13th International Conference on System Science / Ed. by Z. Bubnicki, A. Grzech. — Wroclaw, Poland: 1998. 15-18 September. - Pp. 160-167.

77. Zamulin, A. V. Object-oriented abstract state machines / A. V. Zamulin // Proceedings of the 5th International Workshop on Abstract State Machines, Magdeburg, Germany, September 21-22.— 1998. — Pp. 1-21.