История создания компьютерных систем всегда сопровождалась поиском средств точной спецификации программных или аппаратных продуктов. Жесткие требования, предъявляемые к качеству и срокам выхода продукта на современный рынок информационных технологий, заставляют специалистов постоянно работать над этой проблемой, пересматривать существующие подходы и предлагать новые решения проблемы в виде все более совершенных языков и систем спецификации. Такие языки и системы часто первоначально появляются в качестве исследовательских проектов университетских лабораторий.
Как правило, разработка компьютерной системы делится на несколько этапов, такие как анализ и спецификация требований к разрабатываемому продукту, спецификация программной части системы (спецификация интерфейсов, алгоритмов и данных), разработку целевого выполняемого кода и тестовых примеров, а также различные проверки того, что разработанная спецификация системы и программный код являются полными, непротиворечивыми и удовлетворяют исходным требованиям. Многие разработчики компьютерных систем согласятся с тем фактом, что этап формирования требований является одним из самых сложных. По большей части на этапе спецификации решается задача формализации требований, т. е. задача перехода от описательных требований на одном из естественных языков (часто неполных, неточных, неоднозначных и даже противоречивых) к описаниям точным, однозначным, непротиворечивым, полным и неизбыточным. Полученный результат уже может стать основой для соглашения между заказчиком или экспертом и архитектором компьютерной системы. Цель формальной спецификации заключается в том, чтобы предоставить архитектору проекта точное и адекватное описания метода решения требуемой задачи или целого класса задач. Модель, полученную в результате определения требований, будем называть базовой моделью. Практика показывает, что полученный набор требований, описывающий базовую модель, может быть еще несколько раз уточнен или дополнен новыми требованиями.
Формализм машин абстрактных состояний (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) := (t3, 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.
