文献

J-GLOBAL ID：201802228378140283   整理番号：18A1911959

検証されたコードに対する正しい構築仕様【JST・京大機械翻訳】

Correct-by-construction specification to verified code

著者 (6件)： Ge Ning (School of Software, Beihang University, Beijing, China) ,  Ge Ning (IRT-Saint Exupery, Toulouse, France) ,  Ge Ning (Systerel, Aix-en-provence-Toulouse, France) ,  Dieumegard Arnaud (IRT-Saint Exupery, Toulouse, France) ,  Jenn Eric (IRT-Saint Exupery, Toulouse, France) ,  Voisin Laurent (Systerel, Aix-en-provence-Toulouse, France)
資料名： Journal of Software: Evolution and Process  (Journal of Software: Evolution and Process)
巻： 30  号： 10  ページ： e1959  発行年： 2018年 
JST資料番号： W0214A  ISSN： 2047-7473  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： Event-Bは,システム開発のための形式的含意と方法である。この方法の鍵となる特徴は,修正毎のシステム設計を生成することである。正しい設計が確立されると,残りの作業は設計から正しいコードを生成するか実行することである。2つの主要な問題は,修正ごとの設計から正しいソフトウェアへのプロセスに残っている。第一に,Event-B設計は,いくつかの技術的制約により「準正しい」であり,例えば,Rodinプラットフォームによる生活性特性を証明することは依然として困難である。浮動小数点演算によるEvent-B設計を構築することは可能でなく,時にはEvent-Bモデルは不完全であり,第三者ライブラリに依存しなければならない。したがって,これらのモデリングと証明ギャップを補完するための方法が必要である。第二に,自動コード発生器の正当性を証明することは非常に困難である。したがって,コード発生器を証明することなく,生成されたコードの正当性を保証するための方法が必要である。本論文では,Event-BモデルとCコードの間の高レベル言語(HLL)と呼ばれる中間形式言語を導入することにより,上記2つの問題に取り組んだ。Event-Bモデルは追加のスケジュール構成でHLLに変換される。ここで,Event-B不変量とシステム不変量(ここではデッドロックフリー性と生存性特性)を,S3と呼ばれるSATベースのモデルチェッカーを用いて証明する。この証明はEvent-Bモデルに関するHLLモデルの正当性を保証する。次に,Cコードを,ほとんどの関数に対してHLLモデルから自動的に生成し,Event-Bで定義された関数契約に従って,第三者に対して人手で実装した。生成したC符号の正当性は等価性証明を用いて保証され,実装されたC符号の正当性は適合性証明を用いて保証される。本論文を通して,著者らは,提案方法を例示するために,トラフィック光制御装置を使用した。次に,この方法を3輪ロボットの自動保護機能に適用し,その実現可能性を評価した。Copyright 2018 Wiley Publishing Japan K.K. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 浮動小数点演算 ,  光制御 ,  含意 ,  ロボット ,  適応性 ,  高水準言語 ,  システム設計 ,  コード生成 ,  *モデリング ,  等価性 ,  計算機システム開発 ,  ソフトウェア ,  不変量
準シソーラス用語： 再生器 ,  システム開発 ,  Event-B , 【Automatic Indexing@JST】

著者キーワード (6件)： C ,  コード生成 ,  等価性証明 ,  Event-B ,  形式的方法 ,  特性証明

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (3件)： 検証 ,  構築 ,  仕様