The post has been translated automatically. Original language: Russian
Tests are one of the main development tools. They help you quickly check whether the program is working in known scenarios, and allow you to notice errors after changes to the code. It is difficult to imagine modern development without them.
But tests have a natural limitation.: they only check the cases that we have selected in advance. If an error occurs in a rare combination of conditions that is not included in the test suite, the system may look fully functional for a long time.
That is why in complex systems, tests alone are sometimes not enough.
What does the test actually check?
A typical test usually starts with a specific set of conditions. We set the input data, perform a function or sequence of actions, and compare the result with the expected result.
For example, if we check the memory controller, we can write data to a specific address, read it back and make sure that the value has not changed. Such a test really shows that a particular operation is working correctly under specific conditions.
But it doesn't say anything about the thousands of other possible states of the system. What happens if at the same moment another processor requests the same memory area? What happens after the reset? What happens if the request arrives during a status change?
For each such case, you can write another test. Then another, and another. However, the number of possible combinations of conditions can grow much faster than the number of tests that are reasonable to maintain.
It's not just the quantity that's the problem.
We can assume that the solution is simple: you need to write more tests. Sometimes it really helps, but the problem is deeper.
The developer must first guess which scenario is worth checking. If no one assumes that a certain sequence of events can lead to an error, there probably won't be a corresponding test.
This is especially noticeable in systems with a large number of states. A processor, device controller, messaging system, or multithreaded program can behave correctly in most common situations, but only make mistakes with a very rare combination of events.
It is these errors that often turn out to be the most unpleasant, because they are difficult to reproduce and even more difficult to find in the logs of the system.
Check the rule, not a single example
Formal verification offers another way of setting the problem. Instead of listing more and more individual scenarios, the developer formulates a rule that must always be followed.
For example, you can set a requirement for memory: the same area should not belong to two processors at the same time. This is no longer a separate scenario, but a common property of the system.
After that, the verification system tries to find a sequence of actions in which this rule is violated. If such an option exists, we get a specific error example.
Instead of asking, "does this script work?" another question arises: "is there a generally acceptable scenario in which the system violates this rule?"
This is a fundamentally different approach.
Tests and formal verification solve different tasks.
Sometimes formal verification is contrasted with testing, but this is not entirely correct. These methods are useful for different tasks and complement each other well.
The test is useful when you need to check a specific example of how the system works. It's simple, straightforward, and usually quick to execute. In addition, the tests are well suited for testing interactions with real hardware, files, network, and other external components.
Formal verification is more useful where there are clear rules that must be followed for a large number of possible states. It helps to explore not just one chosen execution path, but many possible options.
For example, a test may show that the processor has entered the expected state after one specific command. A formal check may try to prove that a certain forbidden transition is not possible at all under any acceptable input conditions.
One method does not override the other.
An example from processor development
We came across this difference when developing Memora8. The processor architecture has rules for memory ownership, processor states, transitions between them, and interactions between multiple components.
It is convenient to check some of these things with regular tests. You can run a command, check the status of the register, write the data to memory and see what happened after the operation.
But it is more convenient to formulate some properties as permanent restrictions. For example, if a memory page belongs to one processor, another processor should not access it until the page is released.
You can write many tests with different query combinations. But a stronger statement of the problem sounds different: it is necessary to check whether there is at all a valid sequence of actions that would violate this rule.
It is for such tasks that we experiment with formal verification and SJV.
What formal verification can't do either
At the same time, it is important not to attribute more opportunities to it than it actually is. Formal verification is not able to automatically understand what the correct system should be.
The developer must still formulate the properties that need to be checked. If you forgot to describe an important rule, it will remain unverified.
In addition, the proof always refers to a specific model. If the model is simplified or incorrectly describes the external environment, the result will also be limited.
Therefore, formal verification does not turn development into a fully automatic process. Rather, it allows you to ask the system stronger questions.
Where is it particularly useful?
This approach is of the greatest interest in systems where the number of possible states is large, and an error can have serious consequences. These can be processors, digital devices, control systems, data exchange protocols, and individual parts of the system software.
Such projects usually already have a large number of tests. Formal verification should not replace them, but can be used for a small set of particularly important properties.
For example, you can check the impossibility of a forbidden state, compliance with memory access rules, or the correctness of transitions between device states. Even a few of these properties can close a whole class of errors that would otherwise require a large number of separate tests.
The main difference is
The test answers the question: "Does the system work correctly in this case?" A formal check allows you to ask a more general question: "Can the system ever violate this rule?"
For simple programs, the first question is often enough. But as the number of states and interactions between the components increases, the second one becomes more interesting.
Therefore, it is not a question of choosing between tests and formal verification. A more practical approach is to understand the strengths of each method and use them where they provide the most benefit.
Tests remain the foundation of development. Formal verification adds the opportunity to explore what is difficult to cover with a set of pre-conceived examples.
Тесты — один из основных инструментов разработки. Они помогают быстро проверить, работает ли программа в известных сценариях, и позволяют заметить ошибки после изменений в коде. Без них современную разработку сложно представить.
Но у тестов есть естественное ограничение: они проверяют только те случаи, которые мы заранее выбрали. Если ошибка возникает в редком сочетании состояний, которое не попало в набор тестов, система может долго выглядеть полностью исправной.
Именно поэтому в сложных системах одних тестов иногда оказывается недостаточно.
Что на самом деле проверяет тест
Обычный тест обычно начинается с конкретного набора условий. Мы задаём входные данные, выполняем функцию или последовательность действий и сравниваем полученный результат с ожидаемым.
Например, если мы проверяем контроллер памяти, можно записать данные по определённому адресу, прочитать их обратно и убедиться, что значение не изменилось. Такой тест действительно показывает, что конкретная операция в конкретных условиях работает правильно.
Но он ничего не говорит о тысячах других возможных состояний системы. Что произойдёт, если в тот же момент другой процессор запросит ту же область памяти? Что будет после сброса? Что произойдёт, если запрос придёт во время изменения состояния?
Для каждого такого случая можно написать ещё один тест. Затем ещё один, и ещё один. Однако количество возможных сочетаний условий может расти намного быстрее, чем количество тестов, которые разумно поддерживать.
Проблема не только в количестве
Можно предположить, что решение простое: нужно написать больше тестов. Иногда это действительно помогает, но проблема глубже.
Разработчик должен сначала догадаться, какой сценарий стоит проверить. Если никто не предполагает, что определённая последовательность событий может привести к ошибке, соответствующего теста, скорее всего, просто не будет.
Особенно это заметно в системах с большим количеством состояний. Процессор, контроллер устройства, система обмена сообщениями или многопоточная программа могут вести себя правильно в большинстве обычных ситуаций, но ошибаться только при очень редкой комбинации событий.
Именно такие ошибки часто оказываются самыми неприятными, потому что их трудно воспроизвести и ещё сложнее найти по журналам работы системы.
Проверять правило, а не отдельный пример
Формальная проверка предлагает другой способ постановки задачи. Вместо того чтобы перечислять всё больше отдельных сценариев, разработчик формулирует правило, которое должно выполняться всегда.
Например, для памяти можно задать требование: одна и та же область не должна одновременно принадлежать двум процессорам. Это уже не отдельный сценарий, а общее свойство системы.
После этого система проверки пытается найти последовательность действий, при которой это правило нарушается. Если такой вариант существует, мы получаем конкретный пример ошибки.
Вместо вопроса «работает ли этот сценарий?» появляется другой вопрос: «существует ли вообще допустимый сценарий, при котором система нарушит это правило?»
Это принципиально другой подход.
Тесты и формальная проверка решают разные задачи
Иногда формальную проверку противопоставляют тестированию, но это не совсем правильно. Эти методы полезны для разных задач и хорошо дополняют друг друга.
Тест удобен, когда нужно проверить конкретный пример работы системы. Он прост, понятен и обычно быстро выполняется. Кроме того, тесты хорошо подходят для проверки взаимодействия с реальным оборудованием, файлами, сетью и другими внешними компонентами.
Формальная проверка полезнее там, где есть чёткие правила, которые должны выполняться для большого количества возможных состояний. Она помогает исследовать не один выбранный путь выполнения, а множество возможных вариантов.
Например, тест может показать, что процессор после одной конкретной команды перешёл в ожидаемое состояние. Формальная проверка может попытаться доказать, что определённый запрещённый переход вообще невозможен при любых допустимых входных условиях.
Один метод не отменяет другой.
Пример из разработки процессора
Мы столкнулись с этой разницей при разработке Memora8. В архитектуре процессора есть правила владения памятью, состояния процессоров, переходы между ними и взаимодействие между несколькими компонентами.
Часть таких вещей удобно проверять обычными тестами. Можно выполнить команду, проверить состояние регистра, записать данные в память и посмотреть, что произошло после операции.
Но некоторые свойства удобнее формулировать как постоянные ограничения. Например, если страница памяти принадлежит одному процессору, другой процессор не должен получить к ней доступ до освобождения этой страницы.
Можно написать много тестов с разными комбинациями запросов. Но более сильная постановка задачи звучит иначе: необходимо проверить, существует ли вообще допустимая последовательность действий, которая нарушит это правило.
Именно для таких задач мы экспериментируем с формальной проверкой и SJV.
Что формальная проверка тоже не может сделать
При этом важно не приписывать ей больше возможностей, чем есть на самом деле. Формальная проверка не способна автоматически понять, какой должна быть правильная система.
Разработчик всё равно должен сформулировать свойства, которые требуется проверить. Если важное правило забыли описать, оно останется вне проверки.
Кроме того, доказательство всегда относится к определённой модели. Если модель упрощена или неверно описывает внешнее окружение, результат тоже будет ограниченным.
Поэтому формальная проверка не превращает разработку в полностью автоматический процесс. Она скорее позволяет задавать системе более сильные вопросы.
Где это особенно полезно
Наибольший интерес такой подход представляет в системах, где количество возможных состояний велико, а ошибка может иметь серьёзные последствия. Это могут быть процессоры, цифровые устройства, системы управления, протоколы обмена данными и отдельные части системного программного обеспечения.
В таких проектах обычно уже есть большое количество тестов. Формальная проверка не должна заменять их, но может использоваться для небольшого набора особенно важных свойств.
Например, можно проверять невозможность запрещённого состояния, соблюдение правил доступа к памяти или правильность переходов между состояниями устройства. Даже несколько таких свойств способны закрыть целый класс ошибок, для которого иначе потребовалось бы большое количество отдельных тестов.
Главное различие
Тест отвечает на вопрос: «Правильно ли система работает в этом случае?» Формальная проверка позволяет задать более общий вопрос: «Может ли система когда-либо нарушить это правило?»
Для простых программ первого вопроса часто достаточно. Но по мере роста количества состояний и взаимодействий между компонентами второй становится всё более интересным.
Поэтому речь не идёт о выборе между тестами и формальной проверкой. Более практичный подход — понимать сильные стороны каждого метода и использовать их там, где они дают наибольшую пользу.
Тесты остаются основой разработки. Формальная проверка добавляет возможность исследовать то, что трудно охватить набором заранее придуманных примеров.
Share
