maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1055Research ArticleОригинальные статьиArticlesВерификация C-программ в мультиязыковой системе СПЕКТРC Program Verication in the Multilanguage System SpectrumНепомнящийВ. А.NepomniashyV. A.vnep@iis.nsk.suАнуреевИ. С.AnureevI. S.anureev@iis.nsk.suАтучинМ. М.AtuchinM. M.noemail@neicon.ruМарьясовИ. В.MaryasovI. V.noemail@neicon.ruПетровА. А.PetrovA. A.noemail@neicon.ruПромскийА. В.PromskyA. V.promsky@iis.nsk.suИнститут систем информатики имени А.П. Ершова СО РАН, Новосибирский государственный университетRussian FederationИнститут систем информатики имени А.П. Ершова СО РАНRussian FederationНовосибирский государственный университетRussian Federation20102012201017488100Copyright © Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В., 20102010Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В.Nepomniashy V.A., Anureev I.S., Atuchin M.M., Maryasov I.V., Petrov A.A., Promsky A.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1055

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

This paper presents the expendable multi-language analysis and verication system SPECTRUM, which is being developed within the framework of the project SPEC- TRUM. The project prospects are discussed using the example of C program verication. The project aims at the development of a new integrated approach to program verica- tion which will allow the integration, unication and combination of program verication techniques together with accumulation and reuse of knowledge about them. One of the project features consists in the use of the specialized executable specication language Atoment. This language provides a unied format to represent both verication meth- ods and data for them (program models, annotations, logic formulas). The C-targeted component of the SPECTRUM system is based on our two-level C program verication method. This method represents a good illustration of the integrated approach, since it provides a complex C program verication that combines operational, axiomatic and transformational approaches.

верификацияспецификацияоперационная семантикааксиоматическая семантикапредметно-ориентированные языкисистемы верификацииveri cationspeci cationoperational semanticsaxiomatic semanticsdomain-speci c languagesveri cation systemsReferencesАнуреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C- программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Том 17, № 3. С. 5-28.Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C- программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Том 17, № 3. С. 5-28.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. N 6. С. 1-16.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. N 6. С. 1-16.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: Сб. науч. тр. Новосибирск: Издательство СО РАН, 2004. Вып. 9: Формальные методы и модели информатики. С. 51-134.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: Сб. науч. тр. Новосибирск: Издательство СО РАН, 2004. Вып. 9: Формальные методы и модели информатики. С. 51-134.Непомнящий В.А., Ануреев И.С., Промский А.В., Дубрановский И.В. На пути к верификации C# программ: трехуровневый подход // Программирование. 2006. № 4. С. 4-20.Непомнящий В.А., Ануреев И.С., Промский А.В., Дубрановский И.В. На пути к верификации C# программ: трехуровневый подход // Программирование. 2006. № 4. С. 4-20.Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1-29.Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1-29.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.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.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.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.Filliatre J.C., Marche C. Multi-prover verification of C programs // Proc. ICFEM 2004. LNCS. 2004. Vol. 3308. P. 15-29.Filliatre J.C., Marche C. Multi-prover verification of C programs // Proc. ICFEM 2004. LNCS. 2004. Vol. 3308. P. 15-29.Jacobs B., Kiniry J.L., Warnier M. Java program verification challenges // Proc. FMCO 2002. Lect. Notes Comput. Sci. 2003. Vol. 2852. P. 202-219.Jacobs B., Kiniry J.L., Warnier M. Java program verification challenges // Proc. FMCO 2002. Lect. Notes Comput. Sci. 2003. Vol. 2852. P. 202-219.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.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.

The authors declare that there are no conflicts of interest present.