The post has been translated automatically. Original language: Russian
The thesis
The tests show how the system behaved in the selected scenarios.
Formal verification solves a more powerful problem. It allows you to determine whether a certain violation can occur at all under given conditions.
This is no longer an extension of the test suite, but another way to justify correctness.
Review
First, you need to define the exact requirement.
For example, the account balance should not become negative. The engine must not operate in emergency mode. An internal transfer should not change the total amount of funds.
After that, the system's operating rules and acceptable states are set.
Further, mathematical methods allow us to determine whether the necessary requirement follows from these rules.
For such a task, state analysis, logical constraints, automatic solvers, and proof systems are used.
If the result is positive, the conclusion does not apply to a few selected values, but to the entire set of cases that the formal model covers.
Decision
Imagine controlling the speed of an engine.
The acceptable range is set in advance. When the speed changes, the new value must remain within this range.
A regular test will check several numbers.
A more rigorous approach poses another challenge: to prove that any permitted operation maintains an acceptable speed.
To do this, the initial state and the rules of change are represented mathematically.
Then it is checked whether there is at least one valid path that will lead to exceeding the limit.
If there is no such way, the requirement is considered proven within the framework of a given model.
Dignities
The main advantage is the power of the result.
There is no need to guess dangerous values and sequences of actions. The entire class of cases described by the conditions is considered.
This approach is especially useful where a mistake can lead to serious consequences.
Formalization also makes it necessary to describe the requirements more precisely. It is necessary to determine in advance the permissible conditions, limitations, and results of operations.
This reduces the number of ambiguities even before writing the basic logic of the system.
Disadvantages
The proof always refers to specifically formulated requirements.
If an important condition has not been set, the result says nothing about it.
The initial assumptions are also of great importance. An error in the environmental model can make a mathematically correct result useless for a real system.
There is also a practical price.
The more complex the system, the more difficult it is to describe it accurately enough. Therefore, strict methods are often applied primarily to critical parts of the program.
Conclusion
Formal verification allows you to move from observing individual launches to justifying the overall behavior of the system.
But proof is possible only when the requirements are stated explicitly.
This leads to the next step: to make such requirements a natural part of development, so that a single description can be used for testing, analysis, and proof.
Тезис
Тесты показывают, как система повела себя в выбранных сценариях.
Формальная верификация решает более сильную задачу. Она позволяет установить, может ли определённое нарушение возникнуть вообще при заданных условиях.
Это уже не расширение набора тестов, а другой способ обоснования корректности.
Обзор
Сначала нужно точно определить требование.
Например, баланс счёта не должен становиться отрицательным. Двигатель не должен работать в аварийном режиме. Внутренний перевод не должен изменять общую сумму средств.
После этого задаются правила работы системы и допустимые состояния.
Далее математические методы позволяют определить, следует ли нужное требование из этих правил.
Для такой задачи применяют анализ состояний, логические ограничения, автоматические решатели и системы доказательств.
Если результат положительный, вывод относится не к нескольким выбранным значениям, а ко всему множеству случаев, которое охватывает формальная модель.
Решение
Представим управление скоростью двигателя.
Допустимый диапазон задан заранее. При изменении скорости новое значение должно оставаться внутри этого диапазона.
Обычный тест проверит несколько чисел.
Более строгий подход ставит другую задачу: доказать, что любая разрешённая операция сохраняет допустимую скорость.
Для этого исходное состояние и правила изменения представляются математически.
Затем проверяется, существует ли хотя бы один допустимый путь, который приведёт к превышению предела.
Если такого пути нет, требование считается доказанным в рамках заданной модели.
Достоинства
Главное достоинство — сила результата.
Не требуется угадывать опасные значения и последовательности действий. Рассматривается весь класс случаев, описанный условиями.
Такой подход особенно полезен там, где ошибка может привести к серьёзным последствиям.
Формализация также заставляет точнее описывать требования. Необходимо заранее определить допустимые состояния, ограничения и результаты операций.
Это уменьшает число неоднозначностей ещё до написания основной логики системы.
Недостатки
Доказательство всегда относится к конкретно сформулированным требованиям.
Если важное условие не было задано, результат ничего о нём не говорит.
Большое значение имеют и исходные предположения. Ошибка в модели внешней среды способна сделать математически верный результат бесполезным для реальной системы.
Есть и практическая цена.
Чем сложнее система, тем труднее описать её достаточно точно. Поэтому строгие методы часто применяют прежде всего к критическим частям программы.
Вывод
Формальная верификация позволяет перейти от наблюдения отдельных запусков к обоснованию общего поведения системы.
Но доказательство возможно только тогда, когда требования сформулированы явно.
Отсюда возникает следующий шаг: сделать такие требования естественной частью разработки, чтобы одно описание можно было использовать для тестирования, анализа и доказательства.
Share
