Реферат 2
ВВЕДЕНИЕ 4
1. Основные понятия и определения 5
2. Обзор инструментов и языков описания систем 6
2.1. Balm-II и язык MVSIS 6
2.2. UPPAAL 7
2.3. mCRL2 7
2.3.1. Спецификация mcrl2 и линеаризация 8
2.3.2. Синтаксис языка описания mCRL2 10
3. Формат представления автоматов kitidis 11
4. Архитектуры программной реализации 13
4.1. Независимая архитектура 13
4.2. Архитектура на основе инструментов mCRL2 14
4.3. Алгоритм построения переходов автомата 15
4.4. Промежуточные инструменты 16
4.4.1. Набор инструментов mCRL2 16
4.4.2. Инструменты лексического и синтаксического разбора 16
ЗАКЛЮЧЕНИЕ 19
СПИСОК ИСПОЛЬЗОВАННОЙ ЛИТЕРАТУРЫ 20
При создании устройства или системы важна проверка правильности его функционирования. Одним из способов такой проверки является построение тестов на основе формальной модели. На кафедре (ИТИДиС) был разработан пакет прикладных программ FSMTest2.0[1], который при помощи инструментов входящих в этот пакет решают такую задачу. Особенностью инструментов является, то, что они способны принимать на вход файл с определенным форматом, kitidis [1] c расширением .fsm. Однако существует большое количество различных языков и форматов описания дискретных систем, не совпадающих с форматом kitidis. Чтобы воспользоваться инструментом FSMTest2.0 для построения тестов по этим описаниям, необходимо перевести их в формат kitidis. Осуществить такой перевод (преобразование) можно и вручную, но это, во-первых, трудоёмкая задача, а во-вторых, чревато ошибками. Поэтому построение инструмента автоматического перевода различных описаний дискретных систем является задачей актуальной.
Данная работа посвящена разработке архитектуры программной реализации преобразующей описание автомата на некотором языке (например, на языке инструмента BALM-II[2], инструмента UPPAAL[3], инструмента pCRL2[4] и т.д.) к формату kitidis. Полученное описание автомата в формате kitidis затем можно использовать в задачах анализа систем, построения композиций, тестов и т.д. с помощью инструментов, входящих в пакет прикладных программ FSMTest.2.0.
В данной работе мы разработали архитектуры программной реализации для преобразования описания системы на языке pCRL2 в формат kitidis для использования инструментом FSMTest2.0. Для этого вначале мы сделали обзор языков и инструментов описания, таких как BALM-II, UPPAAL и тСКЪ2.Также был изучен формат описания автомата kitidis .Разработали алгоритм для преобразования описания pCRL2 в описание в формате kitidis . На основе этого мы предложили две архитектуры программной реализации, независимая архитектура не зависит от инструментов mCRL2. Недостатком этой архитектуры является необходимость построения лексического и синтаксического анализаторов. Вторая архитектура основана на использование инструментов mCRL2, она является более упрощенной.
