|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
InnoChain: a Distributed Ledger for Industry with Formal Verification on all Implementation Levelsстатья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАКДата последнего поиска статьи во внешних источниках: 1 февраля 2021 г.
- Авторы: Kukharenko Vladimir Aleksandrovich, Ziborov Kirill Viktorovich, Sadykov Rafael Faritovich, Naumchev Alexandr Vladimirovich, Rezin Ruslan Maratovich, Merkin-Janson Leonid Albertovich
- Журнал: Моделирование и анализ информационных систем
- Том: 27
- Номер: 4
- Год издания: 2020
- Издательство: Яросл. гос. ун-т
- Местоположение издательства: Ярославль
- Первая страница: 454
- Последняя страница: 471
- DOI: 10.18255/1818-1015-2020-4-454-471
- Аннотация: Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации и формальной верификации. Формальная спецификация и верификация протокола консенсуса необходима, но недостаточна. Необходимо удостовериться, что программная реализация узлов СРР соответствует данному протоколу. Верифицированная программная реализация протокола должна запускаться на достаточно надежной операционной системе. Так называемые “умные контракт”, которые являются важной частью прикладных реализаций конкретных бизнес-процессов на основе СРР, также должны быть верифицируемы.В данной работе мы описываем реализующийся в настоящее время индустриальный проект, результатом которого станет СРР, верифицированная по меньшей мере на четырех описанных выше технологических уровнях. Мы также описываем наш опыт формальной спецификации и верификации протокола HotStuff - отказоустойчивого протокола для гарантированного достижения консенсуса в присутствии византийских процессов и лидера.
- Добавил в систему: Садыков Рафаэль Фаритович