文献

J-GLOBAL ID：201802232795434519   整理番号：18A0873992

記号制約に基づくPLCプログラムの正しさ検証【JST・京大機械翻訳】

Correctness Verification of PLC Program Based on Symbolic Constriant

著者 (2件)： Zhang Ye (電子工程学院 合肥230037) ,  Lu Yuliang (電子工程学院 合肥230037)
資料名： Jisuanji Kexue  (Jisuanji Kexue)
巻： 44  号： z2  ページ： 348-352  発行年： 2017年 
JST資料番号： C2530A  ISSN： 1002-137X  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 中国語 (ZH)

抄録/ポイント： 記号制約はプログラム中の変数関係を記述し、モデル検査、記号実行などのプログラムの静的分析方法に広く応用される。プログラマブル論理コントローラ(PLC)プログラムの正当性検証に記号制約を適用し,プログラムの論理エラーを発見できる。人工的計算記号の制約は,冗長的に乾燥するだけでなく,エラー率も高い。記号制約に基づく正しい検証法を提案して,PLCソースコードの制御フローとデータ流れを分析し,プログラムの制御フローグラフを構築し,それを静的単一代入形式の3アドレスコードに変換する。..PLCプログラムの制御フローチャートとデータフローチャートの制御フローチャートを,それぞれ,提案した.PLCプログラムの制御フローチャートとデータフローチャートの分析を通して,提案した。.PLCプログラムの制御フローチャートとデータフローチャートの制御フローチャートは,それぞれ,制御フローチャートとデータ流れを分析することによって,静的単一割当の形式の3アドレスコードに変換できる。最後に,各変数のシンボル制約を反復計算法を用いて求めた。Data from Wanfang. Translated by JST【JST・京大機械翻訳】

シソーラス用語： 制御装置 ,  モデル検査 ,  冗長性 ,  誤り率 ,  逐次近似 ,  *プログラムの正しさ
準シソーラス用語： SSA形式 ,  制御フロー ,  ソースコード , 【Automatic Indexing@JST】

著者キーワード (5件)： Programmable logic controller ,  Symbolic constraints ,  Correctness verification ,  Three address code ,  Static single assignment

分類 (2件)： 電気式制御機器  (IC02020Y) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (5件)： 記号 ,  制約 ,  PLC ,  プログラムの正しさ ,  検証