文献

J-GLOBAL ID：202002227941111261   整理番号：20A0328400

記号モデル検査を用いたスマート契約のビジネス論理のデバッグ【JST・京大機械翻訳】

Debugging Smart Contract’s Business Logic Using Symbolic Model Checking

著者 (1件)： Shishkin E. (InfoTeCS, Advanced Research Department, Moscow, Russia)
資料名： Programming and Computer Software  (Programming and Computer Software)
巻： 45  号： 8  ページ： 590-599  発行年： 2019年 
JST資料番号： W4866A  ISSN： 0361-7688  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： スマート契約はブロックチェーン内で実行する特別なタイプのプログラムである。許容可能で透明で,それらは耐故障性と打ち切り耐性サービスを実行するための手段を提供する。残念ながら,その不適合性は,ブロックチェーンで出版する前に,ビジネス論理と実装が正しいアップフロントであることを保証する重大な挑戦を引き起こす。いくつかの大きな事故は,この技術のユーザがスマート契約の正当性を検証するために特別なツールを必要とすることを実際に示している。既存の自動チェッカーは,良く知られた実装バグのみを検出することができ,ビジネス論理の正当性の問題を残している。本研究では,状態特性とトレース特性の両方を表現できる,Solidityプログラミング言語の部分集合に対する形式仕様法と共に,記号モデル検査技術を提示した。後者は時間的性質の弱い類似性を構成する。著者らは,提案した技術を,有名なTheDAOの若い兄弟であるミニDAOスマート契約について評価した。本論文では,このスマート契約のビジネスロジックにおいて,数秒で非自明な誤りを検出することができた。Copyright Pleiades Publishing, Ltd. 2019 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 部分集合 ,  プログラミング言語 ,  フォールトトレランス ,  *モデル検査 ,  ソフトウェア障害 ,  *デバッギング ,  類似性 ,  忍容性
準シソーラス用語： 許容性 ,  ブロックチェーン , 【Automatic Indexing@JST】

分類 (2件)： 図形・画像処理一般  (JE04010I) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (6件)： 記号 ,  モデル検査 ,  契約 ,  ビジネス ,  論理 ,  デバッグ