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

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

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



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






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


Модел. и анализ информ. систем, 2010, том 17, номер 4, страницы 88–100 (Mi mais39)  

Эта публикация цитируется в 6 научных статьях (всего в 6 статьях)

Верификация C-программ в мультиязыковой системе СПЕКТР

В. А. Непомнящийab, И. С. Ануреевa, М. М. Атучинb, И. В. Марьясовa, А. А. Петровb, А. В. Промскийa

a Институт систем информатики им. А. П. Ершова СО РАН
b Новосибирский государственный университет

Аннотация: Представлена расширяемая мультиязыковая система анализа и верификации СПЕКТР, разрабатываемая в рамках одноименного проекта, и показаны перспективы ее использования на примере верификации C-программ. Проект СПЕКТР направлен на создание нового интегрированного подхода к верификации императивных программ, который позволяет интегрировать, унифицировать и комбинировать методы и техники верификации императивных программ, накапливать и использовать знания о них. Особенностью подхода является использование специализированного языка выполнимых спецификаций Atoment для разработки средств верификации программ, который позволяет представить в едином унифицированном формате как методы и техники верификации, так и данные для них (программные модели, аннотации, логические формулы). C-компонента системы СПЕКТР использует двухуровневый метод верификации C-программ. Этот метод является хорошей иллюстрацией интегрированного подхода, поскольку он обеспечивает комплексную верификацию C-программ, базирующуюся на комбинации операционного, аксиоматического и трансформационного подходов.

Ключевые слова: верификация, спецификация, операционная семантика, аксиоматическая семантика, предметно-ориентированные языки, системы верификации

Полный текст: PDF файл (293 kB)
Список литературы: PDF файл   HTML файл
Тип публикации: Статья
УДК: 519.681
Поступила в редакцию: 18.10.2010

Образец цитирования: В. А. Непомнящий, И. С. Ануреев, М. М. Атучин, И. В. Марьясов, А. А. Петров, А. В. Промский, “Верификация C-программ в мультиязыковой системе СПЕКТР”, Модел. и анализ информ. систем, 17:4 (2010), 88–100

Цитирование в формате AMSBIB
\RBibitem{NepAnuAtu10}
\by В.~А.~Непомнящий, И.~С.~Ануреев, М.~М.~Атучин, И.~В.~Марьясов, А.~А.~Петров, А.~В.~Промский
\paper Верификация C-программ в мультиязыковой системе СПЕКТР
\jour Модел. и анализ информ. систем
\yr 2010
\vol 17
\issue 4
\pages 88--100
\mathnet{http://mi.mathnet.ru/mais39}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais39
  • http://mi.mathnet.ru/rus/mais/v17/i4/p88

    ОТПРАВИТЬ: 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. М. М. Атучин, И. С. Ануреев, “Атрибутные аннотации и их применение в дедуктивной верификации C-программ”, Модел. и анализ информ. систем, 18:4 (2011), 21–33  mathnet
    2. И. С. Ануреев, “Типовые примеры использования языка Atoment”, Модел. и анализ информ. систем, 18:4 (2011), 7–20  mathnet
    3. И. С. Ануреев, “Дедуктивная верификация телекоммуникационных систем, представленных на языке Си”, Модел. и анализ информ. систем, 19:6 (2012), 34–44  mathnet
    4. И. С. Ануреев, “На пути к технологии разработки операционной семантики компьютерных языков: унифицированный формат помеченных систем переходов”, Тр. СПИИРАН, 25 (2013), 255–276  mathnet
    5. И. С. Ануреев, С. Н. Баранов, Д. М. Белоглазов, Е. В. Бодин, П. Д. Дробинцев, А. В. Колчин, В. П. Котляров, А. А. Летичевский, А. А. Летичевский, В. А. Непомнящий, И. В. Никифоров, С. В. Потиенко, Л. В. Прийма, Б. В. Тютин, “Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений”, Тр. СПИИРАН, 26 (2013), 349–383  mathnet
    6. М. С. Ушакова, А. И. Легалов, “Инструментальная поддержка формальной верификации программ, написанных на языке функционально-потокового параллельного программирования”, Вестн. ЮУрГУ. Сер. Выч. матем. информ., 4:2 (2015), 58–70  mathnet  crossref  elib
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:243
    Полный текст:89
    Литература:32
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020