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

Полный текст:


Аннотация

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

Об авторах

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


И. С. Ануреев
Институт систем информатики имени А.П. Ершова СО РАН
Россия


М. М. Атучин
Новосибирский государственный университет
Россия


И. В. Марьясов
Институт систем информатики имени А.П. Ершова СО РАН
Россия


А. А. Петров
Новосибирский государственный университет
Россия


А. В. Промский
Институт систем информатики имени А.П. Ершова СО РАН
Россия


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

1. Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C- программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Том 17, № 3. С. 5-28.

2. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. N 6. С. 1-16.

3. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: Сб. науч. тр. Новосибирск: Издательство СО РАН, 2004. Вып. 9: Формальные методы и модели информатики. С. 51-134.

4. Непомнящий В.А., Ануреев И.С., Промский А.В., Дубрановский И.В. На пути к верификации C# программ: трехуровневый подход // Программирование. 2006. № 4. С. 4-20.

5. Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1-29.

6. Alkassar E., Hillebrand M.A., Leinenbach D., Schirmer N.W., Starostin A. The Verisoft Approach to Systems Verification // VSTTE 2008. Lect. Notes Comput. Sci. 2008. Vol. 5295. P. 209-224.

7. Cohen E., Dahlweid M., Hillebrand M.A., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // Proc. TPHOLs 2009. LNCS. 2009. Vol. 5674. P. 23-42.

8. Filliatre J.C., Marche C. Multi-prover verification of C programs // Proc. ICFEM 2004. LNCS. 2004. Vol. 3308. P. 15-29.

9. Jacobs B., Kiniry J.L., Warnier M. Java program verification challenges // Proc. FMCO 2002. Lect. Notes Comput. Sci. 2003. Vol. 2852. P. 202-219.

10. Promsky A.V. Towards C-light Program Verification: Overcoming the Obstacles // Proc. International Workshop on Program Understanding, 19-23 June, Altai Mountains, Russia, 2009. P. 53-63.


Дополнительные файлы

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

For citation: Nepomniashy V.A., Anureev I.S., Atuchin M.M., Maryasov I.V., Petrov A.A., Promsky A.V. C Program Verication in the Multilanguage System Spectrum. Modeling and Analysis of Information Systems. 2010;17(4):88-100. (In Russ.)

Просмотров: 11

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)