The post has been translated automatically. Original language: Russian
The thesis
Testing looks for cases in which the program does not work correctly.
Formal verification raises another question.
Is it possible to prove that a given property holds for all program states that the model considers?
This is no longer an increase in the number of tests. The verification method itself is changing.
Review
For formal verification, the requirement must first be precisely defined.
For example, the account balance should never go negative.
The engine must not operate in an emergency condition.
After a successful transfer, the total amount of money in the two accounts should be saved.
Then the behavior of the program is described in a form suitable for mathematical analysis.
The tool checks whether the required property follows from the specified program rules.
Logical formulas, state checking, automatic solvers, or proof-building systems can be used for this.
The result is not just a successful program run on multiple data.
It proves that the property holds for the entire set of states under consideration.
Decision
Consider the engine speed change function.
There is a condition: the new value must be within the acceptable range.
There is an invariant: the engine speed should never exceed the set limit.
During testing, you can check the values 0, 20, 50, 99 and several erroneous cases.
With symbolic execution, it is possible to explore many paths with previously unknown meanings.
Formal verification goes further.
It must be shown that when the preconditions are fulfilled, each valid operation preserves the invariant.
If this is proven, it is no longer necessary to check each possible speed value separately.
The proof applies immediately to the entire range that is described in the conditions.
Dignities
The main advantage of formal verification is the strength of the result.
The test shows that the error did not occur in a particular startup.
A formal check can show that a certain violation is impossible under the given conditions.
This approach is especially important for systems where the cost of error is high. These are equipment management, transportation, communications, financial transactions, and other critical systems.
The formal specification also makes it necessary to formulate the requirements precisely.
Phrases like "the system must work correctly" are not enough. It is necessary to determine what exactly is considered the correct state and which transitions are acceptable.
Disadvantages
Formal verification does not mean that the program is absolutely error-free.
Specific properties are proved.
If an important property is not formulated, the proof says nothing about it.
The result also depends on the initial assumptions.
If the environmental model is incorrect, the program can be proven correct relative to the model and still work incorrectly in the real system.
Another difficulty is the cost of formalization.
For a complex program, describing all the requirements and constructing proofs can take considerable effort.
Therefore, formal verification is often applied only to the most important parts of the system.
Conclusion
Formal verification draws a clear line between verification and proof.
Testing answers the question of whether a violation has been found.
Formal verification can answer a stronger question: is it possible to violate a given property at all.
But for this, the properties of the program must be expressed explicitly and related to its behavior.
The next step is to make such a specification a natural part of the development itself, so that the same properties can be used for testing, analysis, and proof.
Тезис
Тестирование ищет случаи, в которых программа работает неправильно.
Формальная верификация ставит другой вопрос.
Можно ли доказать, что заданное свойство выполняется для всех состояний программы, которые рассматривает модель?
Это уже не увеличение числа тестов. Меняется сам способ проверки.
Обзор
Для формальной верификации сначала нужно точно определить требование.
Например, баланс счёта никогда не должен становиться отрицательным.
Двигатель не должен работать при аварийном состоянии.
После успешного перевода общая сумма денег на двух счетах должна сохраниться.
Затем поведение программы описывается в форме, пригодной для математического анализа.
Инструмент проверяет, следует ли требуемое свойство из заданных правил программы.
Для этого могут использоваться логические формулы, проверка состояний, автоматические решатели или системы построения доказательств.
Результатом становится не просто успешный запуск программы на нескольких данных.
Получается обоснование того, что свойство выполняется для всего рассматриваемого множества состояний.
Решение
Рассмотрим функцию изменения скорости двигателя.
Есть условие: новое значение должно находиться в допустимом диапазоне.
Есть инвариант: скорость двигателя никогда не должна превышать установленный предел.
При тестировании можно проверить значения 0, 20, 50, 99 и несколько ошибочных случаев.
При символическом выполнении можно исследовать множество путей с неизвестным заранее значением.
Формальная верификация идёт дальше.
Нужно показать, что при выполнении предусловий каждая допустимая операция сохраняет инвариант.
Если это доказано, больше не требуется проверять каждое возможное значение скорости отдельно.
Доказательство относится сразу ко всему диапазону, который описан в условиях.
Достоинства
Главное преимущество формальной верификации состоит в силе результата.
Тест показывает, что ошибка не возникла в конкретном запуске.
Формальная проверка может показать, что определённое нарушение невозможно при заданных условиях.
Особенно важен этот подход для систем, где цена ошибки высока. Это управление оборудованием, транспорт, связь, финансовые операции и другие критические системы.
Формальная спецификация также заставляет точно сформулировать требования.
Фразы вроде «система должна работать правильно» недостаточно. Нужно определить, что именно считается правильным состоянием и какие переходы допустимы.
Недостатки
Формальная верификация не означает доказательства абсолютной безошибочности программы.
Доказываются конкретные свойства.
Если важное свойство не сформулировано, доказательство ничего о нём не говорит.
Результат также зависит от исходных предположений.
Если модель внешней среды неверна, программа может быть доказана корректной относительно модели и всё равно работать неправильно в реальной системе.
Ещё одна трудность — стоимость формализации.
Для сложной программы описание всех требований и построение доказательств может потребовать значительных усилий.
Поэтому формальная верификация часто применяется только к наиболее важным частям системы.
Вывод
Формальная верификация проводит чёткую границу между проверкой и доказательством.
Тестирование отвечает на вопрос: удалось ли найти нарушение.
Формальная верификация может ответить на более сильный вопрос: возможно ли нарушение заданного свойства вообще.
Но для этого свойства программы должны быть выражены явно и связаны с её поведением.
Следующий шаг — сделать такую спецификацию естественной частью самой разработки, чтобы одни и те же свойства можно было использовать для тестирования, анализа и доказательства.
Share
