The post has been translated automatically. Original language: Russian
The thesis
Property-based testing works well when you need to test a lot of input data.
But for many programs, the main difficulty lies not in the input data, but in the state of the system.
The user logs in, creates an object, modifies it, cancels the operation, repeats the action. The result depends on what happened before.
In such cases, it is more convenient to check not individual values, but a model of acceptable behavior.
Review
The model describes the states of the system and the transitions between them.
For example, an order can be created, confirmed, paid, shipped, and completed.
Some transitions are allowed. Others are impossible.
The paid order can be sent. A completed order cannot be put back into the waiting state for payment.
Such a scheme can be represented as a set of states and transition rules between them.
Based on it, the verification system creates sequences of actions and executes them in a real program.
After each step, the state of the program is compared with what is expected according to the model.
This way, you can check not a single operation, but long chains of actions.
Decision
The main change is the appearance of an independent description of the behavior of the system.
Consider a simple bank account.
It can be active or blocked. It is allowed to debit money from an active account if the balance is sufficient. Debiting is prohibited from a blocked account.
Instead of several pre-written scenarios, you can set these states and transition rules.
After that, the system builds the sequences itself.
Open an account. Transfer money. Deduct part of the amount. Block the account. Try to perform another operation.
The person sets the rules, and the check sequences are created automatically.
This is especially useful where the error occurs after only a few actions.
Dignities
The model allows you to explore significantly more behavior sequences than a developer usually writes manually.
It detects status errors well. For example, an operation that is valid after one action, but becomes incorrect after another sequence.
The model also makes the rules of the system explicit.
The developer is forced to determine which states exist, which transitions are allowed, and which conditions must be met.
This already looks like not just a set of tests, but a description of the program's behavior.
Disadvantages
The quality of the check depends entirely on the quality of the model.
If an important condition or rule is missing in the model, the system will not be able to check it.
There is also the issue of size.
Even a small number of states and actions can generate a huge number of sequences. It is often impossible to check them all.
Therefore, the tools usually select only a part of the possible paths.
In addition, the model and the actual program exist separately. They may differ not only because of an error in the program, but also because of an error in the model itself.
Thus, successful model-based testing still does not mean that all possible system states have been investigated.
Conclusion
Model-based testing shifts attention from individual inputs to the behavior of the program over time.
This is an important step.
Now we are already describing the states, transitions, and rules of the system, not just the expected results of individual calls.
But verification still usually covers only a fraction of the possible paths.
The next question becomes even more interesting: is it possible to explore the state space systematically and automatically to look for a violation of a given property?
This is where model verification methods come in.
Тезис
Тестирование на основе свойств хорошо работает, когда нужно проверять множество входных данных.
Но у многих программ главная сложность находится не во входных данных, а в состоянии системы.
Пользователь входит в систему, создаёт объект, изменяет его, отменяет операцию, повторяет действие. Результат зависит от того, что происходило раньше.
В таких случаях удобнее проверять не отдельные значения, а модель допустимого поведения.
Обзор
Модель описывает состояния системы и переходы между ними.
Например, заказ может быть создан, подтверждён, оплачен, отправлен и завершён.
Некоторые переходы разрешены. Другие невозможны.
Оплаченный заказ можно отправить. Завершённый заказ нельзя снова перевести в состояние ожидания оплаты.
Такую схему можно представить как набор состояний и правил перехода между ними.
На её основе система проверки создаёт последовательности действий и выполняет их в реальной программе.
После каждого шага состояние программы сравнивается с тем, которое ожидается согласно модели.
Таким образом можно проверять не отдельную операцию, а длинные цепочки действий.
Решение
Главное изменение состоит в появлении независимого описания поведения системы.
Рассмотрим простой банковский счёт.
Он может быть активным или заблокированным. С активного счёта разрешено списывать деньги, если остаток достаточен. С заблокированного счёта списание запрещено.
Вместо нескольких заранее написанных сценариев можно задать эти состояния и правила переходов.
После этого система сама строит последовательности.
Открыть счёт. Зачислить деньги. Списать часть суммы. Заблокировать счёт. Попытаться провести ещё одну операцию.
Человек задаёт правила, а последовательности проверок создаются автоматически.
Это особенно полезно там, где ошибка возникает только после нескольких действий.
Достоинства
Модель позволяет исследовать значительно больше последовательностей поведения, чем обычно пишет разработчик вручную.
Она хорошо обнаруживает ошибки состояния. Например, операцию, которая допустима после одного действия, но становится неправильной после другой последовательности.
Модель также делает правила системы явными.
Разработчик вынужден определить, какие состояния существуют, какие переходы разрешены и какие условия должны выполняться.
Это уже похоже не просто на набор тестов, а на описание поведения программы.
Недостатки
Качество проверки полностью зависит от качества модели.
Если в модели отсутствует важное состояние или правило, система не сможет проверить его.
Есть и проблема размера.
Даже небольшое число состояний и действий может породить огромное количество последовательностей. Проверить их все часто невозможно.
Поэтому инструменты обычно выбирают только часть возможных путей.
Кроме того, модель и реальная программа существуют отдельно. Они могут расходиться не только из-за ошибки в программе, но и из-за ошибки в самой модели.
Таким образом успешное тестирование на основе модели всё ещё не означает, что исследованы все возможные состояния системы.
Вывод
Тестирование на основе модели переносит внимание с отдельных входных данных на поведение программы во времени.
Это важный шаг.
Теперь мы уже описываем состояния, переходы и правила системы, а не только ожидаемые результаты отдельных вызовов.
Но проверка всё ещё обычно охватывает лишь часть возможных путей.
Следующий вопрос становится ещё интереснее: можно ли исследовать пространство состояний систематически и автоматически искать нарушение заданного свойства?
Именно к этому переходят методы проверки моделей.
Share
