The post has been translated automatically. Original language: Russian
The thesis
Model-based testing creates multiple sequences of actions and verifies them on a real program.
But the number of possible sequences is growing rapidly. Even a small system can have millions of states and transitions.
A different approach arises. Instead of selecting individual scenarios, you can build a system model and automatically explore all available states within the specified boundaries.
Review
Model verification works with a formal description of the system.
The model defines states, acceptable transitions, and properties that should not be violated.
For example, you can describe two bank accounts and transfer operations between them.
One of the properties may state that the total amount of money remains unchanged after an internal transfer.
The system starts from the initial state and consistently considers all possible transitions.
From each new state, she considers possible actions again.
This is how the state space is gradually built.
If the specified property is violated in one of them, the system shows the sequence of actions that led to the error.
This is an important difference from regular testing. The verification tool does not wait for the developer to select a problematic scenario in advance. He himself is looking for a way to violate the property.
Decision
Consider an equipment management system.
The device can be turned off, ready for operation, running, or in an emergency state.
You can set a rule: the engine should not run if the system is in an emergency state.
The check begins to explore possible actions.
Power on. Starting the engine. The occurrence of an accident. Reset the status. Re-launch.
If there is a sequence in which the engine remains switched on after going into an emergency state, the system will find it and show the path from the initial state to the violation.
The developer does not need to write just such a test in advance.
He needs to define a model and a property.
Dignities
The main advantage lies in the systematic study of conditions.
For the selected model, you can check not just a few random sequences, but the entire space that the tool is able to build under specified conditions.
This approach works especially well for errors related to states, event order, and parallel execution.
The error path found is also useful. The developer gets a specific transition sequence that violates the requirement.
In addition, the requirements become explicit. They need to be expressed in the form of properties that the system can verify.
Disadvantages
The main problem is called the explosion of the state space.
Each new variable, state, or parallel process increases the number of possible combinations.
For a real program, the space may become so large that a complete search will be impossible.
Therefore, the model often has to be simplified.
This creates a second limitation. The model is being checked, not necessarily the running program itself.
If the model does not match the implementation, a successful check does not guarantee the correctness of the program.
Finally, the result depends on the set properties. The tool is able to find a violation of a formulated requirement, but it cannot verify a requirement that no one has described.
Conclusion
Model verification changes the very nature of software verification.
Instead of running the selected tests, the system explores the state space and looks for a way to violate a given property.
This is much closer to verification.
But an important question remains. Even if the model is fully tested, how can its properties be linked to the program code itself?
This requires methods that allow you to set constraints directly for the program and check them before or during execution.
The next step is contracts, preconditions, postconditions, and invariants.
Тезис
Тестирование на основе модели создаёт множество последовательностей действий и проверяет их на реальной программе.
Но число возможных последовательностей быстро растёт. Даже небольшая система может иметь миллионы состояний и переходов.
Возникает другой подход. Вместо выбора отдельных сценариев можно построить модель системы и автоматически исследовать все доступные состояния в заданных границах.
Обзор
Проверка моделей работает с формальным описанием системы.
В модели задаются состояния, допустимые переходы и свойства, которые не должны нарушаться.
Например, можно описать два банковских счёта и операции перевода между ними.
Одно из свойств может утверждать, что общая сумма денег после внутреннего перевода остаётся неизменной.
Система начинает с начального состояния и последовательно рассматривает все допустимые переходы.
Из каждого нового состояния она снова рассматривает возможные действия.
Так постепенно строится пространство состояний.
Если в одном из них заданное свойство нарушается, система показывает последовательность действий, которая привела к ошибке.
Это важное отличие от обычного тестирования. Проверяющий инструмент не ждёт, пока разработчик заранее выберет проблемный сценарий. Он сам ищет путь к нарушению свойства.
Решение
Рассмотрим систему управления оборудованием.
Устройство может быть выключено, готово к работе, запущено или находиться в аварийном состоянии.
Можно задать правило: двигатель не должен работать, если система находится в аварийном состоянии.
Проверка начинает исследовать возможные действия.
Включение питания. Запуск двигателя. Возникновение аварии. Сброс состояния. Повторный запуск.
Если существует последовательность, при которой двигатель остаётся включённым после перехода в аварийное состояние, система найдёт её и покажет путь от начального состояния до нарушения.
Разработчику не нужно заранее писать именно такой тест.
Ему нужно определить модель и свойство.
Достоинства
Главное преимущество состоит в систематическом исследовании состояний.
Для выбранной модели можно проверить не несколько случайных последовательностей, а всё пространство, которое инструмент способен построить в заданных условиях.
Особенно хорошо этот подход работает для ошибок, связанных с состояниями, порядком событий и параллельным выполнением.
Полезен и найденный путь к ошибке. Разработчик получает конкретную последовательность переходов, которая нарушает требование.
Кроме того, требования становятся явными. Их нужно выразить в форме свойств, которые система способна проверить.
Недостатки
Основная проблема называется взрывом пространства состояний.
Каждая новая переменная, состояние или параллельный процесс увеличивает число возможных комбинаций.
Для реальной программы пространство может стать настолько большим, что полный перебор окажется невозможным.
Поэтому модель часто приходится упрощать.
Из этого возникает второе ограничение. Проверяется модель, а не обязательно сама работающая программа.
Если модель не соответствует реализации, успешная проверка ещё не гарантирует правильность программы.
Наконец, результат зависит от заданных свойств. Инструмент способен найти нарушение сформулированного требования, но не может проверить требование, которое никто не описал.
Вывод
Проверка моделей меняет сам характер проверки программного обеспечения.
Вместо запуска выбранных тестов система исследует пространство состояний и ищет путь к нарушению заданного свойства.
Это уже значительно ближе к верификации.
Но остаётся важный вопрос. Даже если модель проверена полностью, как связать её свойства с самим программным кодом?
Для этого нужны методы, которые позволяют задавать ограничения непосредственно для программы и проверять их до или во время выполнения.
Следующий шаг — контракты, предусловия, постусловия и инварианты.
Share
