Студопедия
Случайная страница | ТОМ-1 | ТОМ-2 | ТОМ-3
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатика
ИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханика
ОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторика
СоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансы
ХимияЧерчениеЭкологияЭкономикаЭлектроника

Конструкция и символы SDL

Читайте также:
  1. III. КОНЦЕПЦИИ И СИМВОЛЫ ЦЕЛИ
  2. А21.Знаки препинания в предложениях со словами и конструкциями, грамматически не связанными с членами предложения.
  3. АССОРТИМЕНТ И КОНСТРУКЦИЯ ШВЕЙНЫХ ИЗДЕЛИЙ
  4. В максимальной реалистичности и логичности реконструкция;
  5. Ведьмы и священные символы
  6. Вибробункер. Конструкция и принцип работы. Расчет производительности вибробункера
  7. Воинские символы и ритуалы

Конструкция start. Стартовое состояние процесса конвертируется в БП, у

которого в качестве предусловия записано (начальное) состояние init. В постусловии БП записывается состояние, заданное конструкцией start. Заметим, что все агенты инициируются состоянием init как в исходном состоянии, так и для случая динамически созданных экземпляров агентов.

Состояние процесса. Конструкция state <имя состояния> транслируется в

соответствующую проверку специального атрибута state в предусловии:

Так как конструкция state * означает «все состояния», то она просто игнорируется при трансляции.

Конструкция state *(x) означает «все состояния кроме х» и записывается в

предусловии в виде соответствующих неравенств:

Чтение сигнала из очереди (input). Функциональность приема/посылки

сигналов реализуется с помощью структуры данных типа «очередь» и набором операторов над ней: is_in_list, add_elem, remove_elem, и др. Так же определена функция First(<имя списка>, <условие>), которая находит первый элемент из списка <имя списка>, удовлетворяющий условию <условие>. Для полной реализации работы с входящими сообщениями необходимо описать обработку конструкции SAVE <имя сигнала>. Для этого организуем дополнительный список save_list, в который будут записываться сохраняемые сигналы в постусловии:

Тогда конструкция input запишется с использованием функции First:

В постусловии сигнал удаляется из очереди посредством выполнения операции remove_elem(<элемент>, <имя очереди>) и выполняется присваивание атрибута SENDER:

<имя типа процесса> <процесс>.SENDER:= pid

Посылка сигнала (output). Посылка сигнала транслируется в оператор

add_tail(<имя сигнала>,<имя очереди входящих сигналов адресата>) в постусловии.

Оператор task и вызовы процедур. Этот оператор выполняет присваивания,

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

Символы SDL

SDL/GR SDL/PR Значение символов
STATE NEXTSTATE Состояние Следующее состояние
TASK Задача
INPUT Ввод
OUTPUT Вывод
SAVE Сохранение
DECISION Решение
CALL Вызов процедуры
MACRO Вызов макро
CREATE Запрос создания процесса
ALTERNATIVE Опции
STOP Останов
RETURN Возврат из процедуры
ENDMACRO Выход из макро
START Старт процесса
PROCEDURE Начало процедуры
MACRO EXPANSION Вход в макро
  Расширение текста
COMMENT Kомментарии
X: JOIN X Входной соединитель Выходной соединитель
Все
Все, кроме
PROVIDED Непрерывный сигнал

 

40) Методы формальной спецификации программ; 41) Объектно – ориентированные методы

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

Можно выделить три уровня применения формальных методов:

Нулевой уровень

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

Первый уровень

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

Второй уровень

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

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

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

Языки формальных спецификаций были разработаны для того, чтобы

упростить и там, где это возможно, автоматизировать процессы создания и

анализа программного обеспечения.


Дата добавления: 2015-08-13; просмотров: 193 | Нарушение авторских прав


Читайте в этой же книге: Краткая характеристика и основные свойства SDL | Сигналы управления | Система абонентской сигнализации по цифровым линиям (E-DSS1) | Каналы и сигналы SDL. 14) Определение SDL-системы; | Сигнализация по 1ВСК для универсальных СЛ двустороннего использования; 25) Индуктивный код ( линейные сигналы, декадный код). | Сценарий обмена сигналами ( междугородный вызов) ( абонент свободен, разъединение от АМТС) | Многочастотная сигнализация Импульсный челнок. | Краткая характеристика и основные свойства SDL; 31) Архитектура SDL-модели. | ОО отладка в среде одного языка | Спецификация программ на языке RSL |
<== предыдущая страница | следующая страница ==>
Виды описания языка базовых протоколов| Функциональное программирование

mybiblioteka.su - 2015-2024 год. (0.008 сек.)