RUS  ENG
Полная версия
ЖУРНАЛЫ // Информатика и автоматизация // Архив

Тр. СПИИРАН, 2013, выпуск 26, страницы 349–383 (Mi trspy563)

Эта публикация цитируется в 5 статьях

Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений

И. С. Ануреевa, С. Н. Барановb, Д. М. Белоглазовa, Е. В. Бодинa, П. Д. Дробинцевc, А. В. Колчинd, В. П. Котляровc, А. А. Летичевскийd, А. А. Летичевскийd, В. А. Непомнящийae, И. В. Никифоровc, С. В. Потиенкоd, Л. В. Приймаc, Б. В. Тютинc

a Институт систем информатики им. А. П. Ершова СО РАН
b Санкт-Петербургский институт информатики и автоматизации РАН
c Санкт-Петербургский государственный политехнический университет
d Институт кибернетики им. В. М. Глушкова НАН Украины
e Новосибирский государственный университет

Аннотация: В работе описываются разработанные авторами инструментальные средства и комплексный подход на их основе, при котором методы и средства анализа и верификации обеспечены для представителей всех четырех основных классов языков, на которых обычно описываются телекоммуникационные приложения: языки выполняемых спецификаций общего назначения (SDL), языки для описания и анализа укрупненных образцов поведения и выявления зависимостей между ними в сложных системах (UCM), специализированные языки, ориентированные на верификацию спецификаций телекоммуникационных систем (язык интерпретированных MSC диаграмм, язык взаимодействующих конечных автоматов, язык Dynamic-REAL) и индустриальные императивные языки (C/С++). Верификация спецификаций дополняется автоматизированным построением тестовых наборов, обеспечивающих заданную степень покрытия исходных поведенческих требований, причем эти тестовые наборы оптимизированы по заданным критериям производительности. Исполнение тестов происходит в среде автоматизированного тестирования на моделях систем, либо непосредственно на их реализациях, погруженных в соответствующие программные оболочки, обеспечивающие взаимодействие тестируемой системы с тестовым окружением. Тестовая оболочка позволяет одновременно с прогоном тестов проводить автоматизированный анализ результатов тестирования.

Ключевые слова: базовые протоколы, верификация, ключевые агенты, операционная семантика, логика безопасности, телекоммуникационные системы, помеченные системы переходов, язык спецификаций SDL, язык спецификаций Dynamic-REAL, система верификации SPIN, системы конечных автоматов, раскрашенные сети Петри.

УДК: 004.92+004.94

Поступила в редакцию: 25.12.2012



© МИАН, 2024