The post has been translated automatically. Original language: Russian
Usually, the result of checking the program lives for several seconds in the terminal window: the tests have passed, there are no errors, and the build has been completed.
This is not enough for formal verification.
If we claim that a program has certain properties, it is important to know which program has been tested, according to which specification, and under what conditions.
Therefore, a separate result file, SJP, appeared in SJV.
It is associated with a specific program version and specification. It records the checksums of the input files, the verification area, the accepted conditions, the version of the verification system, and the parameters under which the result was obtained.
This means that the confirmation cannot be imperceptibly transferred to the modified program.
The source code, executable file, or specification has changed — the checksums have changed. The old SJP already belongs to a different version of the program and the check must be performed again.
This is especially important for large systems where one module depends on the others. In the future, the results of checking individual modules can be used as confirmed boundaries when checking the next level of the system.
This gradually creates a chain of related verification results.
At the same time, SJP should not be perceived as a universal proof of the correctness of the entire program. It captures only what SJV actually checked: specific properties in a specific model and under specified conditions.
This is a matter of principle for us.
Formal verification should leave behind not the promise "we checked this once", but an accurate and reproducible answer to the question.:
what exactly was tested and which version of the program this result belongs to.
Обычно результат проверки программы живёт несколько секунд в окне терминала: тесты прошли, ошибок нет, сборка завершена.
Для формальной верификации этого недостаточно.
Если мы утверждаем, что программа обладает определёнными свойствами, важно знать, какая именно программа была проверена, по какой спецификации и при каких условиях.
Поэтому в SJV появился отдельный файл результата — SJP.
Он связывается с конкретной версией программы и спецификации. В нём фиксируются контрольные суммы входных файлов, область проверки, принятые условия, версия системы верификации и параметры, при которых получен результат.
Это означает, что подтверждение нельзя незаметно перенести на изменённую программу.
Изменился исходный код, исполняемый файл или спецификация — изменились контрольные суммы. Старый SJP уже относится к другой версии программы и проверку необходимо выполнить заново.
Это особенно важно для больших систем, где один модуль зависит от других. В дальнейшем результаты проверки отдельных модулей можно использовать как подтверждённые границы при проверке следующего уровня системы.
Так постепенно возникает цепочка связанных результатов проверки.
При этом SJP не стоит воспринимать как универсальное доказательство правильности всей программы. Он фиксирует только то, что действительно проверяла SJV: конкретные свойства в конкретной модели и при заданных условиях.
Для нас это принципиально.
Формальная верификация должна оставлять после себя не обещание «мы когда-то это проверяли», а точный и воспроизводимый ответ на вопрос:
что именно было проверено и к какой версии программы относится этот результат.
Share
