Верификация 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.