抄録/ポイント:
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
コストはソースコードからモデルを抽出する高いためコードレベルでのプログラムの検証は益々注目を集めている。コードレベル検証のための利用可能なアプローチの大部分は,アサーションを挿入するプログラムに,アサーションは破られるかどうかをチェックすることにより行った。しかしこのようにして,安全性特性を検証することができ,活性のようなプログラムの他の時間的特性を検証することができない。この問題を解決するために,検証するプログラムをモデル化,シミュレーションおよび検証言語(MSVL)プログラムMで書かれているが本論文で提示した統一モデル検査アプローチと望ましい特性は,伝統的なモデル検査アプローチからのP.異なる命題投影時相論理(PPTL(命題投影時間論理))の式で記述し,所望の特性の否定はMSVLプログラムMの第一に変換した。PはMに有効であるかどうかは,新しいMSVLプログラムの許容実行「MおよびM’」が存在するかどうかを評価することにより確認することができた。この問題はMSVLのコンパイラすなわちMSVを実施できる。提案されたアプローチは,UMC4MSVLと呼ばれるツールに実装した。実験はUMC4MSVLは実世界プログラムの時間的特性を検証するのに有効であることを示した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】