文献

J-GLOBAL ID：201702266949299877   整理番号：17A1255009

静的解析および定理証明による正しい安全性が重要なハードウェア記述【Powered by NICT】

Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving

著者 (2件)： Moore Nicholas ,  Lawford Mark
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： FormaliSE  ページ： 58-64  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： PVSの高次証明論理におけるBluespec SystemVerilog記述を埋込むための新しい方法を提案した。以前の埋め込みとは対照的に,筆者らのアプローチはBSVの大きなサブセットを受け入れ,はるかに大きい程度の自動化を提供する。カスタムソフトウェアツールはBSVの行動指向意味論を形質転換状態中心Kripke構造に,自動定理証明を可能にした。PLCのIEC61131 3標準の機能ブロックの一つにそれを適用することによって,検証技術を実証した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： *ハードウェア ,  部分集合 ,  *定理証明 ,  自動化 ,  *安全性 ,  意味論
準シソーラス用語： 機能ブロック ,  自動定理証明 ,  *静的解析 , 【Automatic Indexing@JST】

分類 (2件)： 計算理論  (JB02000A) ,  電気式制御機器  (IC02020Y)

タイトルに関連する用語 (5件)： 静的解析 ,  定理証明 ,  安全性 ,  ハードウェア ,  記述