The post has been translated automatically. Original language: Russian
Modern software is checked constantly. They write unit tests, integration tests, load testing, static analysis, and code auditing.
But even if millions of tests have been passed, there remains a fundamental question.:
can we say that the program works correctly in all acceptable cases?
Regular testing does not provide such an answer.
This is exactly what formal verification is for.
The test checks individual cases
Consider a simple function that accepts two 32-bit numbers.
The number of possible combinations of input data can be measured in billions of billions. If you add a memory state, a sequence of previous operations, parallel processes, and external events, the space of possible states becomes almost endless.
Testing selects individual points from this space.:
input 1 → result is correct
input 2 → result is correct
input 3 → result is correct
...The better the tests, the more important situations they cover.
But running the tests successfully only means:
the program worked correctly in proven cases.
This does not logically mean that it will work correctly in all other cases.
This is not a lack of testing. It's his nature.
Formal verification asks a different question
Formal verification is based on mathematical methods.
First, the property that the system must fulfill is formally defined. Then it is checked whether this property follows from the implementation and the given assumptions.
Simplified:
Specification
+
implementation
, mathematical verification
, the property holds
for all states of the modelFor example, instead of checking thousands of different index values, you can formulate a property:
for any valid input
, accessing the array
Never goes beyond its boundariesAnd try to prove exactly this statement.
What can be proved
Formal verification does not necessarily try to prove the abstract statement "the program is perfect."
Usually, specific properties are proved.
For example:
- the program does not access beyond the allowed memory;
- a certain state of the system is not possible;
- a user without the appropriate rights will not be able to access the data.;
- two operations will not break the set order.;
- The value of a variable always remains within the acceptable range.;
- The algorithm produces a result corresponding to the formal specification.;
- The system will definitely switch to the required state after a certain event.
That is, the question becomes much more precise.:
what exactly is the property of the system that we want to guarantee?
This is an important difference between formal verification and the usual idea of error detection.
The proof also has boundaries
The phrase "the program has been formally verified" is not sufficient in itself.
You always need to ask:
what exactly has been proven and about which model?
Let's say we have proved the correctness of a certain program.
But it doesn't work by itself.
There are more:
the source code
, the compiler
, machine code
, operating system
↓
processorA compiler error can theoretically change the correct program.
The operating system's mistake is to violate its assumptions.
Processor error — execute a machine instruction not as expected.
In addition, the proof relies on a formal specification. If the specification itself does not describe what is really required of the system, a mathematically correct implementation may still be practically incorrect.
Therefore, formal verification does not eliminate the need for testing. Even with evidence, it remains necessary to verify assumptions, integration, and compliance of the real system with the model.
Then why do we need formal verification?
Because there are systems where the wording:
"we have checked many times and so far we have not found any errors"
it may be insufficient.
Especially if the error can lead to:
- data loss;
- a security breach;
- failure of critical infrastructure;
- improper equipment management;
- large financial losses;
- a threat to human life.
Formal verification allows you to move from increasing the number of verified examples to a fundamentally different level of confidence.:
the proof of the specific properties of the system within the framework of a formal model.
Testing looks for errors. Verification proves properties
These approaches are not competitors.
A good engineering system can use both:
testing
+
static analysis
+
formal specification
+
formal verificationTesting helps to detect real errors and verify the operation of the system in a specific environment.
Formal verification allows you to answer questions that cannot be reliably solved by simply going through the test scenarios.
Therefore, it is more correct to talk not about replacing testing, but about the next level of software requirements.
When it is not enough to know that a program normally works, there is a desire to prove that certain errors in it are impossible.
But here comes the next question.
If we were able to prove the correctness of the program, who guarantees that the computer itself will execute the proven program correctly?
More on this in the following articles in the series.
Современное программное обеспечение проверяют постоянно. Пишут unit-тесты, интеграционные тесты, проводят нагрузочное тестирование, статический анализ и аудит кода.
Но даже если прошли миллионы тестов, остаётся принципиальный вопрос:
можем ли мы утверждать, что программа работает правильно во всех допустимых случаях?
Обычное тестирование такого ответа не даёт.
Именно для этого существует формальная верификация.
Тест проверяет отдельные случаи
Рассмотрим простую функцию, принимающую два 32-битных числа.
Количество возможных комбинаций входных данных может измеряться миллиардами миллиардов. Если добавить состояние памяти, последовательность предыдущих операций, параллельно выполняющиеся процессы и внешние события, пространство возможных состояний становится практически необозримым.
Тестирование выбирает из этого пространства отдельные точки:
вход 1 → результат правильный
вход 2 → результат правильный
вход 3 → результат правильный
...Чем качественнее тесты, тем больше важных ситуаций они покрывают.
Но успешное выполнение тестов означает только:
программа правильно сработала в проверенных случаях.
Из этого логически не следует, что она правильно сработает во всех остальных случаях.
Это не недостаток тестирования. Это его природа.
Формальная верификация задаёт другой вопрос
Формальная верификация основана на математических методах.
Сначала формально задаётся свойство, которое должна выполнять система. Затем проверяется, следует ли это свойство из реализации и заданных предположений.
Упрощённо:
спецификация
+
реализация
↓
математическая проверка
↓
свойство выполняется
для всех состояний моделиНапример, вместо проверки тысячи различных значений индекса можно сформулировать свойство:
для любого допустимого входа
обращение к массиву
никогда не выходит за его границыИ попытаться доказать именно это утверждение.
Что можно доказать
Формальная верификация не обязательно пытается доказать абстрактное утверждение «программа идеальна».
Обычно доказываются конкретные свойства.
Например:
- программа не обращается за пределы разрешённой памяти;
- определённое состояние системы невозможно;
- пользователь без соответствующих прав не получит доступ к данным;
- две операции не нарушат заданный порядок;
- значение переменной всегда остаётся в допустимом диапазоне;
- алгоритм выдаёт результат, соответствующий формальной спецификации;
- система после определённого события обязательно перейдёт в требуемое состояние.
То есть вопрос становится значительно точнее:
какое именно свойство системы мы хотим гарантировать?
Это важное отличие формальной верификации от привычного представления о поиске ошибок.
Доказательство тоже имеет границы
Фраза «программа формально верифицирована» сама по себе недостаточна.
Всегда нужно спрашивать:
что именно было доказано и относительно какой модели?
Допустим, мы доказали правильность некоторой программы.
Но она работает не сама по себе.
Есть ещё:
исходный код
↓
компилятор
↓
машинный код
↓
операционная система
↓
процессорОшибка компилятора теоретически может изменить правильную программу.
Ошибка операционной системы — нарушить её предположения.
Ошибка процессора — выполнить машинную инструкцию не так, как ожидалось.
Кроме того, доказательство опирается на формальную спецификацию. Если сама спецификация описывает не то, что действительно требуется от системы, математически правильная реализация всё равно может оказаться практически неправильной.
Поэтому формальная верификация не устраняет необходимость тестирования. Даже при наличии доказательств остаётся необходимость проверять предположения, интеграцию и соответствие реальной системы модели.
Зачем тогда нужна формальная верификация
Потому что существуют системы, где формулировка:
«мы много раз проверили и пока ошибки не обнаружили»
может быть недостаточной.
Особенно если ошибка способна привести к:
- потере данных;
- нарушению безопасности;
- отказу критической инфраструктуры;
- неправильному управлению оборудованием;
- большим финансовым потерям;
- угрозе жизни человека.
Формальная верификация позволяет перейти от увеличения количества проверенных примеров к принципиально другому уровню уверенности:
доказательству конкретных свойств системы в рамках формальной модели.
Тестирование ищет ошибки. Верификация доказывает свойства
Эти подходы не являются конкурентами.
Хорошая инженерная система может использовать одновременно:
тестирование
+
статический анализ
+
формальную спецификацию
+
формальную верификациюТестирование помогает обнаруживать реальные ошибки и проверять работу системы в конкретном окружении.
Формальная верификация позволяет ответить на вопросы, которые невозможно надёжно закрыть простым перебором тестовых сценариев.
Поэтому правильнее говорить не о замене тестирования, а о следующем уровне требований к программному обеспечению.
Когда недостаточно знать, что программа обычно работает, возникает желание доказать, что определённые ошибки в ней невозможны.
Но здесь появляется следующий вопрос.
Если мы смогли доказать правильность программы, кто гарантирует, что сам компьютер выполнит доказанную программу правильно?
Об этом — в следующих статьях серии.
Share
