RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Общая информация
Последний выпуск
Архив

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Тр. СПИИРАН:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


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

Эта публикация цитируется в 5 научных статьях (всего в 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, системы конечных автоматов, раскрашенные сети Петри

Полный текст: PDF файл (1276 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 004.92+004.94
Поступила в редакцию: 25.12.2012

Образец цитирования: И. С. Ануреев, С. Н. Баранов, Д. М. Белоглазов, Е. В. Бодин, П. Д. Дробинцев, А. В. Колчин, В. П. Котляров, А. А. Летичевский, А. А. Летичевский, В. А. Непомнящий, И. В. Никифоров, С. В. Потиенко, Л. В. Прийма, Б. В. Тютин, “Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений”, Тр. СПИИРАН, 26 (2013), 349–383

Цитирование в формате AMSBIB
\RBibitem{AnuBarBel13}
\by И.~С.~Ануреев, С.~Н.~Баранов, Д.~М.~Белоглазов, Е.~В.~Бодин, П.~Д.~Дробинцев, А.~В.~Колчин, В.~П.~Котляров, А.~А.~Летичевский, А.~А.~Летичевский, В.~А.~Непомнящий, И.~В.~Никифоров, С.~В.~Потиенко, Л.~В.~Прийма, Б.~В.~Тютин
\paper Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений
\jour Тр. СПИИРАН
\yr 2013
\vol 26
\pages 349--383
\mathnet{http://mi.mathnet.ru/trspy563}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/trspy563
  • http://mi.mathnet.ru/rus/trspy/v26/p349

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles

    Эта публикация цитируется в следующих статьяx:
    1. П. Д. Дробинцев, В. П. Котляров, И. В. Никифоров, А. А. Летичевский, В. С. Песчаненко, “Подход к автоматизации отладки поведенческих сценариев”, Модел. и анализ информ. систем, 21:6 (2014), 44–56  mathnet
    2. С. А. Черненок, В. А. Непомнящий, “Анализ и верификация MSC-диаграмм распределённых систем с помощью раскрашенных сетей Петри”, Модел. и анализ информ. систем, 21:6 (2014), 94–106  mathnet
    3. П. Д. Дробинцев, В. П. Котляров, И. В. Никифоров, А. А. Летичевский, “Инкрементальный подход к технологии создания тестов для индустриальных проектов”, Модел. и анализ информ. систем, 21:6 (2014), 144–154  mathnet
    4. Н. В. Визовитин, В. А. Непомнящий, А. А. Стененко, “Применение раскрашенных сетей Петри для верификации конструкций управления сценариями языка UCM”, Модел. и анализ информ. систем, 23:6 (2016), 688–702  mathnet  crossref  mathscinet  elib
    5. P. D. Drobintsev, V. P. Kotlyarov, I. V. Nikiforov, N. V. Voinov, I. A. Selin, “Conversion of abstract behavioral scenarios into scenarios applicable for testing”, Труды ИСП РАН, 28:3 (2016), 145–160  mathnet  crossref  elib
  • Просмотров:
    Эта страница:154
    Полный текст:40
    Литература:20
    Первая стр.:1

     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019