文献

J-GLOBAL ID：202002238735768155   整理番号：20A1868477

Cから相互作用ツリーへ:ネットワーク化サーバの仕様化,検証,および試験【JST・京大機械翻訳】

From C to interaction trees: specifying, verifying, and testing a networked server

著者 (9件)： Koh Nicolas (University of Pennsylvania, USA) ,  Li Yao (University of Pennsylvania, USA) ,  Li Yishuai (University of Pennsylvania, USA) ,  Xia Li-yao (University of Pennsylvania, USA) ,  Beringer Lennart (Princeton University, USA) ,  Honore Wolf (Yale University, USA) ,  Mansky William (University of Illinois at Chicago, USA) ,  Pierce Benjamin C. (University of Pennsylvania, USA) ,  Zdancewic Steve (University of Pennsylvania, USA)
資料名： ACM Proceedings  (ACM Proceedings)
号： CPP 2019  ページ： 234-248  発行年： 2019年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： Cに実装されたネットワークサーバの最初の形式的検証を示した。反応計算を表現するための一般的構造である相互作用ツリーを用いて,異種検証と試験ツール(Coq,VST,QuickChick)を一緒に連結し,サーバラン(CertiKOS)の運転システムの行動を公知する。主定理は,CプログラムのCompCert意味論を用いて,直接”1クライアントの時間”スタイルで書かれた,許容できるサーバ行動の仕様を接続する。メッセージの低レベル緩衝と多重TCP接続のインタリービングにより導入された変動性を,ネットワーク精密化,観測精密化の変種を用いて捉えた。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： *相互作用 ,  意味論 ,  *ネットワーク ,  多重化 ,  インタリービング ,  精密化
準シソーラス用語： *ネットワーク化 ,  ネットワークサーバ ,  TCPコネクション , 【Automatic Indexing@JST】

著者キーワード (7件)： クイックチック ,  TCP ,  VST ,  形式的検証 ,  相互作用ツリー ,  ネットワーク精密化 ,  試験

分類 (1件)： 計算機網  (JC03000K)

タイトルに関連する用語 (5件)： 相互作用 ,  サーバ ,  仕様 ,  検証 ,  試験