Об одном формальном подходе к построению автоматных программ1 icon

Об одном формальном подходе к построению автоматных программ1


Смотрите также:
Удк 004. 838: 004. 853: 004. 855. 5 Об одном подходе к порождению гипотез в дсм-методе...
Лекция, прочитанная 12 мая 1995 г в Москве...
Служба примирения: от замысла до распространения о восстановительном подходе...
Исследование подходов к построению...
Программа: santools программный комплекс для верификации синхронно-автоматных моделей систем...
Сифат тизими менеджменти система менеджмента качества об одном подходе к систематизации методик...
Лекция 3 курса «Методы автоматизации тестирования»...
«О едином подходе к обучению детей с нарушениями письменной речи и оцениванию их работ по...
Результат образования в традиционном и компетентностном подходе...
Верификация автоматных программ...
Методические указания по построению...
Курс, проводятся в коммуникативном подходе. Стадии уроков следующие: а...



Загрузка...

ОБ ОДНОМ ФОРМАЛЬНОМ ПОДХОДЕ К ПОСТРОЕНИЮ АВТОМАТНЫХ ПРОГРАММ1



Е.В. Кузьмин, В.А. Соколов, Д.Ю. Чалый


Ярославский государственный университет им. П.Г. Демидова, Ярославль, Россия


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

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

Одной из таких методологий является технология автоматного программирования [2], в рамках которой предлагаются новые формальные модели автоматных программ [3]. При использовании этой технологии по словесному описанию системы строится набор взаимодействующих конечных автоматов Мура-Мили (далее просто – автоматная программа).

Метод формальных утверждений о трассах (TAM-метод) был предложен в работе Бартуссека и Парнаса [1]. Метод активно развивается [5], а также имеется опыт использования его на практике для спецификации реальных управляющих систем [6].

В работе [2] предлагается начинать построение автоматной программы с анализа неформального текстового описания системы, выделять компоненты объекта управления и состояния системы взаимодействующих автоматов. Такой подход имеет ряд недостатков [6]: неформальное описание может быть неоднозначно истолковано, быть неполным, противоречивым и т.д. Действительно, наиболее критичные ошибки в программных системах являются следствием недочетов, допущенных на стадии определения требований к системе, а их исправление на более поздних стадиях проектирования программы может быть на несколько порядков более трудоемким. В то же время, при использовании TAM-метода спецификация описывается математическим языком и может быть проанализирована формально.

При построении автоматной программы ^ A TAM-метод используется для определения семантики входных и выходных воздействий, а также запросов к объекту управления для каждого автомата программы A (см. [4]).

Построенная автоматная программа может быть верифицирована с использованием следующих подходов [4]:

  • тестирование автоматной программы ^ A может быть проведено с использованием TAM-спецификации и учетом определенной на этапе построения программы семантики элементов программы A;

  • на основе TAM-спецификации может быть проведена верификация созданной программы с использованием метода Model Checking.

Таким образом, в нашей работе показано, что TAM-спецификация является не только базисом для задания семантики компонентов автоматной программы, но и основой для ее верификации и тестирования.
^

Список литературы


  1. Bartussek W., Parnas D.L. Using assertions about traces to write abstract specifications for software modules. // Proc. of the 2nd Conf. on European Cooperation in Informatics. LNCS № 65. 1978. p. 211-236.

  2. Шалыто А.А. Switch-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998.

  3. Кузьмин Е.В., Соколов В.А. Моделирование, спецификация и верификация «автоматных» программ // Программирование. №1, 2008. С. 38-60.

  4. Кузьмин Е.В., Соколов В.А., Чалый Д.Ю. Применение метода формальных утверждений о трассах для спецификации, построения и верификации автоматных программ // Программирование, № 1. 2009.

  5. Janicki R., Sekerinski E. Foundations of the trace assertion method of module interface specification // IEEE Trans. Soft. Eng. V. 27, №7. 2001. p. 577-598.

  6. Baber R.L., Parnas D.L., Vilkomir S.A., Harrison P., O’Connor T. Disciplined methods of software specification: a case study. // Int. Conf. on Information Technology: Coding and Computing’2005. V. 2, 2005. p. 428-437.




1 Работа поддержана грантом РФФИ №07-01-00702-а.




Скачать 29.05 Kb.
оставить комментарий
Дата28.09.2011
Размер29.05 Kb.
ТипДокументы, Образовательные материалы
Добавить документ в свой блог или на сайт

Ваша оценка этого документа будет первой.
Ваша оценка:
Разместите кнопку на своём сайте или блоге:
rudocs.exdat.com

Загрузка...
База данных защищена авторским правом ©exdat 2000-2017
При копировании материала укажите ссылку
обратиться к администрации
Анализ
Справочники
Сценарии
Рефераты
Курсовые работы
Авторефераты
Программы
Методички
Документы
Понятия

опубликовать
Загрузка...
Документы

Рейтинг@Mail.ru
наверх