The post has been translated automatically. Original language: Russian
You can try to check a small program in its entirety. But as the project grows, this approach quickly becomes inconvenient: there are more components, the connections between them become more complicated, and the verification time increases.
For complex systems, a different principle is needed. Instead of one big check, it is useful to break the project into parts, check each of them separately, and then use the results obtained in a higher-level check.
This approach is especially important for processors, control systems, network protocols, and other projects where one module depends on the behavior of many others.
Why is it difficult to check everything at once
Let's imagine a processor. It has computing units, memory, I/O devices, a data exchange system, state management, and many other components.
If you try to describe all this with one model and check it at the same time, the number of possible states can become huge. Even if each individual component is relatively simple, their combinations quickly increase the complexity of the task.
In addition to computing costs, there is another problem. If the check fails, it becomes more difficult to understand exactly where the cause is: in memory, in the processor, in the exchange rules, or in their interaction.
Therefore, the idea naturally arises to check the system gradually.
First, a separate component
Let's say we have a memory module. Several important rules can be formulated for it: when the processor gets access to the page, when it must release it, and which operations are allowed in each state.
First, only this component is checked. If the properties are met, we get a specific set of statements about its behavior.
For example, you can confirm that one page cannot belong to two processors at the same time. Or that after the page is released, the previous owner no longer has the right to change it.
After that, when checking other components, there is no need to re-examine the entire internal workings of the memory each time. You can use already confirmed properties as known conditions.
A contract instead of an internal device
In regular programming, a similar principle is used all the time. The module provides a specific set of functions, and the rest of the code works with them without knowing all the details of the internal implementation.
The same approach can be used for formal verification. One component provides not only functions, but also a set of proven properties of its behavior.
For example, for a memory module, the external layer can only know a few things: how to get the page, how to release it, and what guarantees the system gives between these actions. How exactly this is implemented internally is no longer so important for the next level of verification.
Such a set of conditions can be considered as a component contract. While it is running, other parts of the system can safely rely on it.
The next level
After checking the memory, you can switch to the processor that works with it. At the same time, it is no longer necessary to re-examine all the internal states of the memory module.
The verification system uses its proven properties as initial conditions. Now you can focus on whether the processor itself is correctly following the rules of working with memory.
The proven processor can then be used in the analysis of a larger subsystem. Gradually, a dependency tree or graph appears, where larger components rely on the results of checking smaller ones.
This is how the system is checked from bottom to top.
What happens when changes occur
This approach is especially useful in an ever-evolving project. If you change a small module, there is no need to automatically invalidate all system checks.
First, you can re-check the modified component. If his external contract remains the same, some of the higher-level results may still be valid.
If the component properties themselves have changed, the system must determine which other checks depended on them. Then the repeated work affects only the necessary part of the project.
It's like building programs. After changing one file, it is usually not the entire project that is rebuilt from scratch, but only the parts associated with it.
How is this related to SJV
This is exactly the idea we use in SJV. The verification result is stored separately and may contain information about which properties were confirmed and on which other results they depended.
If one module uses an already tested component, it can refer to its result. At the same time, the system verifies that the version for which the necessary properties were previously confirmed is being used.
Thus, a chain of checks is gradually being formed. The upper level does not just assume that the lower component is working correctly, but is based on a specific result of its verification.
This is especially important for complex projects where it is impossible to consider the entire system as a whole every time.
An example from Memora8
When developing Memora8, this approach arises naturally. The architecture consists of processors, memory, devices, and exchange mechanisms between them.
Some properties relate only to memory. Others describe the operation of a separate processor. Still others appear only when several components interact.
If you check everything at the same time, the model quickly becomes complex. But if you first confirm the rules of the individual parts, then their interaction, and then move on to larger blocks, the task becomes much clearer.
In addition, this approach helps to see the boundaries of each proof more precisely. We know not just that "Memora8 has been tested", but which parts and properties have been tested.
There are limitations to this approach.
Splitting the system into parts does not solve all the problems. The main difficulty lies in choosing the boundaries between the components and their contracts correctly.
If the contract is too weak, the next level may not have enough information to prove the necessary properties. If it repeats the internal structure of the module in too much detail, the benefits of separation begin to disappear.
There is also a risk that each individual component is working correctly, but the error occurs precisely in the interaction between them. Therefore, after checking the parts, you still need to check the connections and general properties of the system.
Partitioning does not cancel the verification of the entire architecture. It makes this check manageable.
Why is this important for large projects?
In a small program, you can afford to check everything anew every time. In a large system, this approach gradually stops working.
Component verification allows you to limit complexity, reuse the results already obtained, and more accurately determine the consequences of changes. Instead of one huge piece of evidence, a set of smaller, interconnected ones appears.
For us, this is one of the key principles of SJV development. If formal verification is to be applied to real large projects, it must be able to work not only with a single function or module, but also with a system that develops gradually and consists of many dependent parts.
That is why the question is "how to prove the correctness of the entire system?" it is useful to first replace it with a more practical one: "what properties of each part should be checked in order to safely assemble the next level from them?"
Небольшую программу можно попытаться проверить целиком. Но по мере роста проекта такой подход быстро становится неудобным: компонентов становится больше, связи между ними усложняются, а время проверки увеличивается.
Для сложных систем нужен другой принцип. Вместо одной большой проверки полезно разбить проект на части, проверить каждую из них отдельно, а затем использовать полученные результаты при проверке более высокого уровня.
Именно такой подход особенно важен для процессоров, систем управления, сетевых протоколов и других проектов, где один модуль зависит от поведения многих других.
Почему проверять всё сразу трудно
Представим процессор. В нём есть вычислительные блоки, память, устройства ввода-вывода, система обмена данными, управление состояниями и множество других компонентов.
Если попытаться описать всё это одной моделью и проверить одновременно, количество возможных состояний может стать огромным. Даже если каждый отдельный компонент сравнительно прост, их сочетания быстро увеличивают сложность задачи.
Кроме вычислительных затрат возникает и другая проблема. Если проверка завершается ошибкой, становится труднее понять, где именно находится причина: в памяти, в процессоре, в правилах обмена или в их взаимодействии.
Поэтому естественно возникает идея проверять систему постепенно.
Сначала отдельный компонент
Допустим, у нас есть модуль памяти. Для него можно сформулировать несколько важных правил: когда процессор получает доступ к странице, когда обязан его освободить и какие операции разрешены в каждом состоянии.
Сначала проверяется только этот компонент. Если свойства выполняются, мы получаем определённый набор утверждений о его поведении.
Например, можно подтвердить, что одна страница не может одновременно принадлежать двум процессорам. Или что после освобождения страницы предыдущий владелец больше не имеет права её изменять.
После этого при проверке других компонентов нет необходимости каждый раз заново рассматривать всю внутреннюю работу памяти. Можно использовать уже подтверждённые свойства как известные условия.
Контракт вместо внутреннего устройства
В обычном программировании похожий принцип используется постоянно. Модуль предоставляет определённый набор функций, а остальной код работает с ними, не зная всех деталей внутренней реализации.
Для формальной проверки можно применять тот же подход. Один компонент предоставляет не только функции, но и набор проверенных свойств своего поведения.
Например, для модуля памяти внешний уровень может знать только несколько вещей: как получить страницу, как освободить её и какие гарантии система даёт между этими действиями. Как именно это реализовано внутри, для следующего уровня проверки уже не так важно.
Такой набор условий можно рассматривать как контракт компонента. Пока он выполняется, другие части системы могут безопасно на него опираться.
Следующий уровень
После проверки памяти можно перейти к процессору, который с ней работает. При этом уже не нужно заново исследовать все внутренние состояния модуля памяти.
Проверяющая система использует его доказанные свойства как исходные условия. Теперь можно сосредоточиться на том, правильно ли сам процессор выполняет правила работы с памятью.
Затем проверенный процессор можно использовать при анализе более крупной подсистемы. Постепенно возникает дерево или граф зависимостей, где более крупные компоненты опираются на результаты проверки более мелких.
Так система проверяется снизу вверх.
Что происходит при изменениях
Особенно полезен такой подход в постоянно развивающемся проекте. Если изменить небольшой модуль, нет необходимости автоматически считать недействительными все проверки системы.
Сначала можно повторно проверить изменённый компонент. Если его внешний контракт остался прежним, часть результатов более высокого уровня может по-прежнему оставаться действительной.
Если же изменились сами свойства компонента, система должна определить, какие другие проверки от них зависели. Тогда повторная работа затрагивает только необходимую часть проекта.
Это похоже на сборку программ. После изменения одного файла обычно пересобирается не весь проект с нуля, а только связанные с ним части.
Как это связано с SJV
В SJV мы используем именно такую идею. Результат проверки сохраняется отдельно и может содержать сведения о том, какие свойства были подтверждены и от каких других результатов они зависели.
Если один модуль использует уже проверенный компонент, он может ссылаться на его результат. При этом система проверяет, что используется именно та версия, для которой ранее были подтверждены нужные свойства.
Таким образом постепенно формируется цепочка проверок. Верхний уровень не просто предполагает, что нижний компонент работает правильно, а опирается на конкретный результат его проверки.
Это особенно важно для сложных проектов, где невозможно каждый раз рассматривать всю систему как одно целое.
Пример с Memora8
При разработке Memora8 такой подход возникает естественным образом. Архитектура состоит из процессоров, памяти, устройств и механизмов обмена между ними.
Некоторые свойства относятся только к памяти. Другие описывают работу отдельного процессора. Третьи появляются только при взаимодействии нескольких компонентов.
Если проверять всё одновременно, модель быстро становится сложной. Но если сначала подтвердить правила отдельных частей, затем их взаимодействие, а после этого перейти к более крупным блокам, задача становится значительно понятнее.
Кроме того, такой подход помогает точнее увидеть границы каждого доказательства. Мы знаем не просто то, что «Memora8 проверен», а какие именно части и свойства были проверены.
У такого подхода есть ограничения
Разбиение системы на части не решает все проблемы. Главная трудность состоит в правильном выборе границ между компонентами и их контрактов.
Если контракт слишком слабый, следующему уровню может не хватить информации для доказательства нужных свойств. Если он слишком подробно повторяет внутреннее устройство модуля, преимущества разделения начинают исчезать.
Также остаётся риск, что каждый отдельный компонент работает правильно, но ошибка возникает именно во взаимодействии между ними. Поэтому после проверки частей всё равно требуется проверять связи и общие свойства системы.
Разбиение не отменяет проверку всей архитектуры. Оно делает эту проверку управляемой.
Почему это важно для больших проектов
В небольшой программе можно позволить себе каждый раз проверять всё заново. В большой системе такой подход постепенно перестаёт работать.
Компонентная проверка позволяет ограничивать сложность, повторно использовать уже полученные результаты и точнее определять последствия изменений. Вместо одного огромного доказательства появляется набор меньших, связанных между собой.
Для нас это один из ключевых принципов развития SJV. Если формальная проверка должна применяться к реальным большим проектам, она должна уметь работать не только с отдельной функцией или модулем, но и с системой, которая развивается постепенно и состоит из множества зависимых частей.
Именно поэтому вопрос «как доказать правильность всей системы?» полезно сначала заменить более практичным: «какие свойства каждой части нужно проверить, чтобы затем безопасно собрать из них следующий уровень?»
Share
