Разработка и реализация системы интерпретации спецификаций на языке ASM с временем и проверки свойств трасс их выполнения

• Автор: Васильев, Павел Константинович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Санкт-Петербург
• Количество страниц: 151 с.

Содержание

Введение . б

Глава 1. Расширение А8М временем.

1.1. Метод АМ

1.2. АЭМ Гуревича

1.3. Турбо АЭМ.

1.4. Временная модель для АБМ .

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

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

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

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

2.1. Синтаксис А8М с временем
2.2. Семантика языка АБМ с временем .
2.3. Алгоритмы интерпретации
Глава 3. Проверка свойств А8М с временем .
3.1. Временная логика первого порядка РОТЬ
3.2. Пример свойств АБМ на языке РОТЬ
3.3. Проверка РОТЬсвойств
3.4. Пример спецификации РОТЬсвойства
3.5. Алгоритмы проверки РОТЬсвойств.
Глава 4. Архитектура интерпретатора АЭМ с временем
4.1. Ядро интерпретатора
4.2. Синтаксический анализатор входного языка
4.3. Загрузчик параметров выполнения
4.4. Хранилище трасс выполнения .
4.5. Интерпретатор АБМ.
4.6. Подсистема проверки РОТГевойетв .
4.7. Графический интерфейс пользователя .
4.8. Пример интерпретации спецификации
Заключение .
Список литературы


Впервые решение проблемы предложили Гуревич и Хаггинс [], которые представили вычисления в виде отображения из области временных значений в область состояний ASM. Затем последовали работы [, ], в которых проблема верификации временных алгоритмов сводится к верификации формальных спецификаций в виде формул специальной временной логики первого порядка FOTL (First Order Timed Logic). Логика FOTL введена D. Beauquier и A. Slissenko в работах [, ] как метод спецификации алгоритмов и их свойств с непрерывным временем. В работах [, ] анализируются разрешимые подклассы логики FOTL. Задачи, которые рассматриваются в данной работе, часто специфицируются с применением темпоральных логик. Для описания свойств спецификаций в формализме ASM требуется достаточно выразительный язык логики. Самым простым логическим языком является язык пропозициональной логики (логики высказываний []). Однако, нетрудно заметить, что язык классической пропозициональной логики плохо приспособлен для спецификаций систем с временем. Существует ряд расширений пропозициональной логики, такие как логики с временем, или темпоральные логики [G1], которые обладают большей выразительной способностью. Linear Temporal Logic), CTL (Computational Tree Logic) или их модификации. Упомянутые логики широко используются для формальной спецификации программ и вычислительных систем. Среди программных инструментов, использующих темпоральные логики, можно выделить: STeP [5], SPIN [7S], SMV [], NuSSMV []. Хотя указанные логики и являются мощным инструментом формальной спецификации динамических систем, некоторые свойства, например, ограничения на время реакции системы, в них выразить очень сложно. В данной работе для спецификации свойств проектируемой системы применяется язык временной логики первого порядка FOTL, которая достаточно подробно описана в главе 3. FOTL является расширением теории со сложением вещественных чисел абстрактными функциями. С помощью языка FOTL можно компактно специфицировать сложные свойства поведения компьютерных систем во времени. В некоторых работах, посвященных использованию времени в методе ASM, предлагается явное использование функции времени, например в работах [, ]. Кроме того, вводятся временные задержки на выполнение либо отдельных фрагментов вычислений, либо замещений [, ]. В перечисленных работах содержится множество идей и предложений по использованию и уточнению языка ASM, но, несмотря на это, в них не сформулирована явная методика спецификации систем с ограничениями на время реакции и последующей проверкой корректности их свойств. Из всего сказанного следует, что разработка и реализация специализированного расширения метода ASM для формальной спецификации систем с временными ограничениями, а также разработка и реализация алгоритмов интерпретации спецификаций на расширенном языке и проверки ограничительных свойств являются актуальными задачами. Microsoft AsmL. Microsoft AsmL — одно из самых известных средств для работы со спецификациями, основанное на методологии ASM. Язык AsmL создавался как инструментальное средство для поддержки создания спецификаций программных продуктов, при этом разработчики языка среди прочих преследовали две цели. Первая цель — обеспечить выразительность и доступность языка для работающего с ним пользователя. Вторая цель — обеспечить выполнение спецификаций машиной. В AsmL реализованы все основные идеи подхода ASM: минимизация объема спецификации, выполнимость, разделение модели на несколько уровней детализации, ясная и однозначная семантика. В AsmL добавлен ряд прикладных расширений, например, поддержка, объектно-ориентированного подхода и возможность создание тестовых примеров. Язык поддерживает стандартные для языков программирования типы данных и конструкции: структуры, классы, последовательности, множества, кортежи, отображения, а также стандартные библиотеки для ввода/вывода. В настоящее время для создания спецификаций на языке AsmL разработчик (компания Microsoft) предлагает пользоваться инструментальным средством Spec Explorer. Данный инструмент предназначен для проектировщиков компьютерных систем, для отделов качества и рядовых программистов.