The post has been translated automatically. Original language: Russian
In normal development, the source code, tests, and documentation are often sufficient.
But for a complex engineering system, another question arises over time.:
which requirement exactly did we check, which version of the implementation does the result relate to, and what confirms that this property was actually fulfilled?
If a project takes a long time to develop, the simple answer "we have tests" is no longer always sufficient.
The code is changing, requirements are changing, tools are being updated, and new versions are being released. After a few months, separate reports, test results, and checks may exist, but the connection between them must be restored manually.
To solve this problem, we are developing Sekura Noda Assurance.
Its main idea is to store not only knowledge about the project, but also a traceable chain from the requirement to the confirming result.
It looks like this:
Requirement → Specification → Implementation → Verification → Evidence
For a certain project state, this chain can be fixed in an immutable Baseline.
From requirement to implementation
The work begins with the fact that the project explicitly records the requirement or engineering approval.
For example:
- the function must produce a specific result.;
- the architectural constraint must not be violated;
- the module must satisfy the specified property;
- the specific state of the system should not occur.;
- a certain operation must be reproducible.
In Noda, such statements can be stored as Claims or Requirements.
It is important that this is no longer just text in a document.
The requirement becomes an independent object that can be linked to a specific specification, implementation version, verification, and evidence.
Why is the exact version important?
Phrase:
"This property of the system has been verified"
in practice, it is too vague.
It's much more useful to be able to say:
"This property has been tested for this version of the specification, this version of the source code, and these input conditions."
This is exactly the accuracy we are trying to ensure at Assurance.
Specific input revisions are recorded for each verification result.
If the source code has changed later, the old result should not automatically be considered a confirmation of the new version.
Verification Run
The checks themselves are performed in the infrastructure of the project owner.
Noda does not run the compiler, tests, or formal verifier instead of the developer.
After performing the verification locally, you can register the Verification Run in Assurance.
Run describes:
- which versions were used exactly;
- what was the verification tool used?;
- what configuration was used?;
- what result was obtained;
- which reports and artifacts were created.
Instead of the general statement "we checked it", a record of a specific engineering check appears.
Several types of confirmation
Not every requirement needs to be checked in the same way.
Therefore, Assurance supports multiple Evidence profiles.
FORMAL
FORMAL is intended for the results of formal verification.
For such an Evidence, you can fix:
- the formal specification;
- the exact version of the implementation;
- completed Verification Run;
- successful verification result;
- an evidence-based artifact.
At the same time, it is important to understand the boundaries of formal proof.
If a property is proven for certain inputs or areas, it does not automatically mean that any broader statement is proven.
The verification area must be explicitly fixed.
TESTED
TESTED is used for testing results.
You can save:
- source code versions;
- completed set of tests;
- result;
- report.
Thus, testing is associated not just with the project as a whole, but with a specific requirement and a specific implementation version.
REPRODUCIBLE
REPRODUCIBLE is used to check reproducibility.
For example, you can fix:
- the source code;
- the toolchain version;
- assembly parameters;
- the received file;
- his hash.
Reassembly allows you to check whether an identical result is obtained under the same input conditions.
REVIEWED
REVIEWED records an engineering review by a human.
You can save:
- what exactly was checked;
- which version was analyzed;
- verification area;
- result;
- who completed the review.
This way, the review ceases to exist only in discussions, correspondence, or comments to the commit and becomes part of the project's history.
What is coverage?
Testing may be enough for one requirement.
For the other, a formal proof may be required.
For the third, the project can define:
TESTED + REPRODUCIBLE
To do this, Assurance uses the coverage policy.
After setting up the policy, the system can determine the status of the requirement.
The main options are:
COVERED — the required confirmation exists.
GAP confirmation is not enough yet.
UNSUPPORTED — the selected policy cannot be executed by the current set of Evidence.
This allows us to look at the project not as a set of documents and reports, but as a system of related requirements and confirmations.
What happens after the code is changed
One of the most annoying problems with engineering documentation is that the verification result may formally exist, but no longer relate to the current version of the product.
Therefore, the Evidence in Assurance is compared with the current state of the project.
It can be:
CURRENT — the input versions correspond to the current state.
STALE — related inputs have changed.
UNKNOWN — there is not enough information to determine the relevance.
This allows you to distinguish between two completely different situations.:
"This property was tested once."
and
"This property is confirmed for the current version."
Traceability
One of the main tasks of Assurance is to provide an opportunity to go through the entire engineering chain.
For example:
Requirement → Specification → Implementation → Verification → Evidence
And then go back through:
Evidence → Run → Implementation Version → Specification → Requirement
Such traceability is especially important in projects that have been developing for years.
If the connections are not fixed immediately, after a while, individual tests, reports, source code versions, and specifications turn into a set of independent files.
It is becoming increasingly difficult to understand which result belongs to which version.
Project Baseline
Sometimes it is not enough to keep a separate proof.
It is necessary to fix the state of the entire system.
For this purpose, Assurance supports Baselines.
The Baseline is an immutable snapshot of the project status.
It may include:
- requirements;
- versions used;
- Evidence;
- Coverage rules;
- coverage results.
Baselines can be compared with each other.
This allows you to see what has changed between the two project states and which previously confirmed properties may have been affected.
Analysis of changes
If a requirement, specification, or implementation has changed, the following question arises:
what should I check again now?
For this purpose, link analysis and impact analysis are used.
The system can help determine:
- what Evidence is related to the modified object?;
- which checks apply to older versions;
- where the new GAP appeared;
- which properties need to be checked again.
The larger the project gets, the more difficult it is to maintain such a picture manually.
This is not a certificate
Important underline the borders separately.
Sekura Noda Assurance does not issue certificates and does not in itself imply compliance with any industry standard.
The presence of Evidence in the system does not automatically mean compliance with IEC 61508, IEC 62443, ISO 26262, DO-178C, DO-254 or other requirements.
Assurance is also not a substitute for independent assessment, functional safety processes, hazard analysis, instrument qualification, or certification.
His task is more fundamental:
keep an evidence-based history of the project during the development process, rather than trying to restore it retroactively.
From knowledge to evidence
The usual knowledge base answers the question:
What do we know about the project?
Assurance adds the next level:
why do we consider a specific statement to be confirmed for a specific version of the system?
Therefore, the development of Noda can be represented as a chain:
Knowledge → Requirement → Specification → Implementation → Verification → Evidence
A knowledge base and tests may be sufficient for a small project.
But as the system grows, versions, connections, relevance of results, and the ability to go from requirement to concrete proof become increasingly important.
This is exactly the task we are solving at Sekura Noda Assurance.
В обычной разработке часто достаточно исходного кода, тестов и документации.
Но для сложной инженерной системы со временем возникает другой вопрос:
какое именно требование мы проверяли, к какой версии реализации относится результат и чем подтверждается, что это свойство действительно выполнялось?
Если проект развивается долго, простой ответ «у нас есть тесты» уже не всегда достаточен.
Меняется код, меняются требования, обновляются инструменты, появляются новые версии. Через несколько месяцев отдельные отчёты, результаты тестов и проверки могут существовать, но связь между ними приходится восстанавливать вручную.
Для решения этой задачи мы развиваем Sekura Noda Assurance.
Его основная идея — хранить не только знания о проекте, но и прослеживаемую цепочку от требования до подтверждающего результата.
Она выглядит так:
Требование → Спецификация → Реализация → Проверка → Evidence
Для определённого состояния проекта эта цепочка может быть зафиксирована в неизменяемом Baseline.
От требования к реализации
Работа начинается с того, что проект явно фиксирует требование или инженерное утверждение.
Например:
- функция должна выдавать определённый результат;
- архитектурное ограничение не должно нарушаться;
- модуль должен удовлетворять заданному свойству;
- конкретное состояние системы не должно возникать;
- определённая операция должна быть воспроизводимой.
В Noda такие утверждения могут храниться как Claims или Requirements.
Важно, что это уже не просто текст в документе.
Требование становится самостоятельным объектом, который можно связать с конкретной спецификацией, версией реализации, проверкой и доказательным материалом.
Почему важна точная версия
Фраза:
«Это свойство системы проверено»
на практике слишком неопределённа.
Гораздо полезнее иметь возможность сказать:
«Это свойство проверено для данной версии спецификации, данной версии исходного кода и данных входных условий».
Именно такую точность мы пытаемся обеспечить в Assurance.
Для каждого результата проверки фиксируются конкретные входные ревизии.
Если позже исходный код изменился, старый результат не должен автоматически считаться подтверждением новой версии.
Verification Run
Сами проверки выполняются в инфраструктуре владельца проекта.
Noda не запускает компилятор, тесты или формальный verifier вместо разработчика.
После локального выполнения проверки в Assurance можно зарегистрировать Verification Run.
Run описывает:
- какие именно версии использовались;
- каким инструментом выполнялась проверка;
- какая использовалась конфигурация;
- какой результат получен;
- какие отчёты и артефакты были созданы.
Вместо общего утверждения «мы это проверяли» появляется запись о конкретной инженерной проверке.
Несколько видов подтверждения
Не каждое требование нужно проверять одинаково.
Поэтому Assurance поддерживает несколько профилей Evidence.
FORMAL
FORMAL предназначен для результатов формальной верификации.
Для такого Evidence можно зафиксировать:
- формальную спецификацию;
- точную версию реализации;
- завершённый Verification Run;
- успешный результат проверки;
- доказательный артефакт.
При этом важно понимать границы формального доказательства.
Если свойство доказано для определённых входов или области, это не означает автоматически, что доказано любое более широкое утверждение.
Область проверки должна быть явно зафиксирована.
TESTED
TESTED используется для результатов тестирования.
Можно сохранить:
- версии исходного кода;
- выполненный набор тестов;
- результат;
- отчёт.
Таким образом, тестирование связывается не просто с проектом в целом, а с конкретным требованием и конкретной версией реализации.
REPRODUCIBLE
REPRODUCIBLE используется для проверки воспроизводимости.
Например, можно зафиксировать:
- исходный код;
- версию toolchain;
- параметры сборки;
- полученный файл;
- его хеш.
Повторная сборка позволяет проверить, получается ли идентичный результат при тех же входных условиях.
REVIEWED
REVIEWED фиксирует инженерную проверку человеком.
Можно сохранить:
- что именно проверялось;
- какую версию анализировали;
- область проверки;
- результат;
- кто выполнил review.
Так review перестаёт существовать только в обсуждении, переписке или комментариях к commit и становится частью истории проекта.
Что такое coverage
Одному требованию может быть достаточно тестирования.
Для другого может требоваться формальное доказательство.
Для третьего проект может определить:
TESTED + REPRODUCIBLE
Для этого в Assurance используется coverage policy.
После настройки политики система может определить состояние требования.
Основные варианты:
COVERED — необходимое подтверждение существует.
GAP — подтверждения пока недостаточно.
UNSUPPORTED — выбранная политика не может быть выполнена текущим набором Evidence.
Это позволяет смотреть на проект уже не как на набор документов и отчётов, а как на систему связанных требований и подтверждений.
Что происходит после изменения кода
Одна из самых неприятных проблем инженерной документации заключается в том, что результат проверки может формально существовать, но уже не относиться к текущей версии продукта.
Поэтому Evidence в Assurance сравнивается с текущим состоянием проекта.
Оно может быть:
CURRENT — входные версии соответствуют текущему состоянию.
STALE — связанные входы изменились.
UNKNOWN — информации недостаточно для определения актуальности.
Это позволяет различать две совершенно разные ситуации:
«Когда-то это свойство было проверено».
и
«Это свойство подтверждено для текущей версии».
Прослеживаемость
Одна из главных задач Assurance — дать возможность пройти по всей инженерной цепочке.
Например:
Требование → Спецификация → Реализация → Проверка → Evidence
И затем пройти обратно:
Evidence → Run → Версия реализации → Спецификация → Требование
Такая прослеживаемость особенно важна в проектах, которые развиваются годами.
Если связи не фиксировать сразу, через некоторое время отдельные тесты, отчёты, версии исходного кода и спецификации превращаются в набор независимых файлов.
Понять, какой результат относится к какой версии, становится всё сложнее.
Baseline проекта
Иногда недостаточно сохранить отдельное доказательство.
Нужно зафиксировать состояние всей системы.
Для этого Assurance поддерживает Baselines.
Baseline — это неизменяемый снимок состояния проекта.
В него могут входить:
- требования;
- используемые версии;
- Evidence;
- правила покрытия;
- результаты coverage.
Baselines можно сравнивать между собой.
Это позволяет увидеть, что изменилось между двумя состояниями проекта и какие ранее подтверждённые свойства могли быть затронуты.
Анализ изменений
Если изменилось требование, спецификация или реализация, возникает следующий вопрос:
что теперь нужно проверить повторно?
Для этого используется анализ связей и impact analysis.
Система может помочь определить:
- какие Evidence связаны с изменённым объектом;
- какие проверки относятся к старым версиям;
- где появились новые GAP;
- какие свойства требуют повторной проверки.
Чем больше становится проект, тем труднее поддерживать такую картину вручную.
Это не сертификат
Важно отдельно подчеркнуть границы.
Sekura Noda Assurance не выдаёт сертификаты и само по себе не означает соответствие какому-либо отраслевому стандарту.
Наличие Evidence в системе не означает автоматически соответствие IEC 61508, IEC 62443, ISO 26262, DO-178C, DO-254 или другим требованиям.
Assurance также не заменяет независимую оценку, процессы функциональной безопасности, hazard analysis, квалификацию инструментов или сертификацию.
Его задача более фундаментальна:
сохранять доказательную историю проекта в процессе разработки, а не пытаться восстановить её задним числом.
От знаний к доказательствам
Обычная база знаний отвечает на вопрос:
что мы знаем о проекте?
Assurance добавляет следующий уровень:
почему мы считаем конкретное утверждение подтверждённым для конкретной версии системы?
Поэтому развитие Noda можно представить как цепочку:
Знание → Требование → Спецификация → Реализация → Проверка → Evidence
Для небольшого проекта может быть достаточно базы знаний и тестов.
Но по мере роста системы всё более важными становятся версии, связи, актуальность результатов и возможность пройти от требования до конкретного доказательства.
Именно эту задачу мы решаем в Sekura Noda Assurance.
Share
