|
Труды СПИИРАН, 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, системы конечных автоматов, раскрашенные сети Петри.
Поступила в редакцию: 25.12.2012
Образец цитирования:
И. С. Ануреев, С. Н. Баранов, Д. М. Белоглазов, Е. В. Бодин, П. Д. Дробинцев, А. В. Колчин, В. П. Котляров, А. А. Летичевский, А. А. Летичевский, В. А. Непомнящий, И. В. Никифоров, С. В. Потиенко, Л. В. Прийма, Б. В. Тютин, “Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений”, Тр. СПИИРАН, 26 (2013), 349–383
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/trspy563 https://www.mathnet.ru/rus/trspy/v26/p349
|
Статистика просмотров: |
Страница аннотации: | 305 | PDF полного текста: | 90 | Список литературы: | 50 | Первая страница: | 1 |
|