Приемы дедуктивной верификации программного кода с использованием AstraVer Toolset

doi:10.17223/2226308X/15/21

Эндаумент фонд ТГУ!
Впиши своё имя в историю университета
- Сделать пожертвование -

Add to "Quick Collection"

Description	Size	Format
Приемы дедуктивной верификации программного кода с использованием AstraVer Toolset	547 KB	Adobe Acrobat PDF	Read	Download
DOI Доступ к ресурсу на сайте издателя			10.17223/2226308X/15/21

#дедуктивная верификация программного кода

#Astra Linux, операционная система

#AstraVer Toolset, система дедуктивной верификации

Title: Приемы дедуктивной верификации программного кода с использованием AstraVer Toolset
Creator: Кокорин, Артем Олегович
|
Тиевский, Станислав Дмитриевич
|
Девянин, Петр Николаевич
Date: 2022
DOI: 10.17223/2226308X/15/21
Description: Описывается ряд практических приёмов дедуктивной верификации программного кода на языке Си на соответствие спецификациям его функций, заданных на языке ACSL. Для такой верификации используется основанный на платформе Frama-C набор инструментов AstraVer Toolset. Апробация этих приёмов осуществлена при верификации программного кода модуля управления доступом, реализованного в подсистеме безопасности PARSEC отечественной защищённой операционной системы специального назначения Astra Linux Special Edition. Благодаря использованию этих приёмов удалось упростить спецификации функций PARSEC, уменьшить трудоёмкость и ускорить процесс их дедуктивной верификации.

Relationships: Show Relationship Browser for this Object
collection(s): Журналы ТГУ
Identifier: смотреть в электронном каталоге НБ ТГУ
Type: статьи в журналах
Source: Прикладная дискретная математика. Приложение. 2022. № 15. С. 80-90
Language: rus

Created: 08-09-2022

635 Visitors

466 Hits

210 Downloads

Журналы ТГУ Приемы дедуктивной верификации программного кода с использованием AstraVer Toolset