Верификация С-программ с помощью смешанной аксиоматической семантики

• Автор: Марьясов, Илья Владимирович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2012
• Место защиты: Новосибирск
• Количество страниц: 110 с.

Оглавление
Введение
Г лава
Языки программ и спецификаций
1.1 Язык С-и§ф1
1.2 Язык С-кеше1
1.3 Язык утверждений
1.3.1 Типы и алфавит
1.3.2 Выражения
1.3.3 Подстановка
1.3.4 Интерпретация выражений
1.3.5 Логические утверждения
Глава
Модифицированная операционная семантика языка С-Н
2.1 Абстрактная машина языка С-Н§ф1
2.2 Параметры и абстрактные функции
2.3 Аксиомы и правила вывода
2.4 Семантика частичной корректности
2.5 Трансляция языка С-Н в С-кете1
2.5.1 Перевод операторов и деклараций
2.5.2 Перевод выражений
Глава
Смешанная аксиоматическая семантика языка С-кете1
3.1 Предварительные понятия
3.2 Выражения
3.3 Декларации
3.4 Операторы
3.5 Другие правила
3.6 Перевод инвариантов из С-Н в С-кете1
Глава
Непротиворечивость смешанной аксиоматической семантики
4.1 Предварительные понятия
4.2 Теорема о непротиворечивости
Глава
Примеры применения смешанной аксиоматической семантики
5.1 Вычисление факториала
5.2 Поиск в линейном односвязном списке
5.3 Топологическая сортировка
Заключение
Литература

Введение
В диссертации представлены формальные семантики языков C-light и C-kemel, ориентированные на верификацию методом Хоара. Доказана теорема о корректности аксиоматической семантики языка C-kemel, исследован вопрос перехода инвариантов циклов при трансляции программ из языка С-light в язык C-kemel, приведены примеры, иллюстрирующие применение предложенных семантик.
Актуальность темы
Формальная верификация программ — актуальное направление современного программирования. Особый интерес представляет верификация программ, написанных на распространённых языках системного программирования таких, как С. Область применения этого языка огромна: от программного обеспечения для бытовой техники до операционных систем и авионики.
Обозримая формальная семантика является необходимой предпосылкой того, что язык удобен для верификации. Однако формальной детерминированной семантики для полного языка С, соответствующего стандарту ISO [62], не существует. Во-первых, сказывается заложенная в С возможность работать на низком уровне — обращение к памяти на уровне отдельных байтов и даже битов. Во-вторых, стандартизация С произошла намного позже его широкого распространения, поэтому многие аспекты поведения С-программ в стандарте ISO просто не специфицированы. В-третьих, сам стандарт написан большей частью на обычном английском языке, что влечёт за собой двусмысленности и неясности, характерные для любого человеческого языка.
В проекте Шармы, Дходапкара, Рамеша и др. (Bhabba Atomic Research Centre, Indian Institute of Technology) представлен метод [66] дедуктивного поиска ошибок в программах на языке MISRA С, который является индустриальным стандартом для написания безопасных программ, ориентированным в основном на встраиваемые системы. Входная С-программа моделиру-

Условная операция. Пусть т0 — скалярный тип. Правила для условной операции имеют вид:
т = type(7:, type(e1> typeiej, type{e2)),
(e0,cr) ->* (Уа1(у,т0), &'), cast(val(y),T0, int) Ф 0 (2.21)
{e07 e±e2, a) -> <(7)6 a')
т = type(7:, type(ex, type(e1), type(e2)),
(e0,a} -** (Val(v,t0), ff'}, cast(yal(y),x0l int) = 0 (2.22)
<(r)e2,o-')
Другие унарные операции. Унарные операции, для которых нет отдельных правил, определяются общим правилом:

(о е, а) -»(У al(UnOpSem(°, val(v), т)), <т'}
Другие бинарные операции. Бинарные операции, для которых нет отдельных правил, определяются общим правилом:
(е2,<т0) ->* (Ра1(ц2,г2),п1),(е1,а1) ->* (Уа.т,)
(ei о е2,о) -»(Val(BinOpSem(°,val(y1),T1,val(v2),T2)), о2)
Декларации переменных. Семантику декларации переменной определяют три правила — одно для декларации без инициализатора и два для декларации с инициализатором.
Пусть е; —- декларация переменной, не включающая спецификатора enum и имеющая единственный декларатор без инициализатора. Правило для декларации переменной без инициализатора имеет вид:
т £ logtypeie.MD.MDnc) = а),
(MD'.V) £ init(r, storage(e), upd(MDa, пс, щ)) (2.25)
(еш,, а) -»(г, a(MD <- upd(MD',пс, fst(V)))
Пусть е = е; — декларация переменной, не включающая спецификатора enum и имеющая единственный декларатор с инициализатором. Правила для декларации переменной с инициализатором имеют вид: