文献

J-GLOBAL ID：202002245931993095   整理番号：20A2085262

イベントBを用いたランツーコンプレションスタイルステートチャートの形式的検証【JST・京大機械翻訳】

Formal Verification of Run-to-Completion Style Statecharts Using Event-B

著者 (6件)： Morris Karla (Sandia National Laboratories, Livermore, CA, USA) ,  Snook Colin (ECS, University of Southampton, Southampton, UK) ,  Hoang Thai Son (ECS, University of Southampton, Southampton, UK) ,  Hulette Geoffrey (Sandia National Laboratories, Livermore, CA, USA) ,  Armstrong Robert (Sandia National Laboratories, Livermore, CA, USA) ,  Butler Michael (ECS, University of Southampton, Southampton, UK)
資料名： Communications in Computer and Information Science  (Communications in Computer and Information Science)
巻： 1269  ページ： 311-325  発行年： 2020年 
JST資料番号： W5071A  ISSN： 1865-0929  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 産業で普及しているが,完成の意味論に対する「実行によるステートチャート表記は,正式な精密化と厳密な検証方法を欠いている。状態チャートモデルは,逐次プロセスによる環境トリガーに応答する複雑な制御システムを設計するために通常用いられる。モデルは,通常,コンクリートレベルで構築され,人間の判断に依存するアニメーション技術を用いて検証され,検証された。一方,イベントBは,初期抽象化からの精密化に基づいており,自動定理証明器により形式的検証を行うように設計されている。著者らは,完成のステートチャートモデリング表記に精緻化への精緻化の概念を導入し,そして,定理証明のためのイベント-B’sツールサポートをレバレッジする。イベント-B精密化への完了の意味論を完了する困難さを記述し,解決策を示唆した。このアプローチを例証し,システムの反応性の性質にもかかわらず,臨界(例えば,安全)不変特性が証明によってどのように検証できるかを示した。また,時間論理モデル検査アプローチを用いて,期待した反応を試験することにより,システムの行動的側面をいかに検証できるかも示した。Copyright Springer Nature Switzerland AG 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 意味論 ,  制御系 ,  コンクリート ,  臨界 ,  シーケンシャル処理 ,  定理証明 ,  精密化 ,  アニメーション ,  時間論理 ,  *状態遷移図 ,  モデル検査 ,  Event-B
準シソーラス用語： 形式的検証 ,  自動定理証明 ,  ツールサポート , 【Automatic Indexing@JST】

著者キーワード (3件)： 実行から完成 ,  状態チャート ,  精密化

分類 (3件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R) ,  システム設計・解析  (IA02030D)

タイトルに関連する用語 (2件)： イベント ,  形式的検証