文献

J-GLOBAL ID：202202280498829748   整理番号：22A1105451

VRM要求モデルのための形式的検証【JST・京大機械翻訳】

Formal Verification for VRM Requirement Models

著者 (5件)： Zhang Yang (College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China) ,  Hu Jun (College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China) ,  Wang Lisong (College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China) ,  Gu Qingfan (Department of Software, China National Aeronautic Radio Electronics Research Institute, Shanghai, China) ,  Rong Hao (Department of Software, China National Aeronautic Radio Electronics Research Institute, Shanghai, China)
資料名： Lecture Notes in Electrical Engineering  (Lecture Notes in Electrical Engineering)
巻： 878  ページ： 961-969  発行年： 2022年 
JST資料番号： W5070A  ISSN： 1876-1100  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 要求レベルでは,形式的検証と解析は,形式的方法で複雑なシステムを開発するタスクの注意の焦点である。モデル検査は,複雑な安全臨界ソフトウェアシステムの解析と自動化検証のための技術である。本論文では,形式技術に基づく要求モデル検証法を提案し,開発プロセスへのモデル検査活動を実践した。最初に,VRM(変数関係モデル)における表明表現によって定義されるモデルの構文論と意味論を分析した。次に,著者らは,VRMモデルを,イベントテーブル,条件テーブルおよびモデルクラステーブルに分類するために前処理し,そして,セマンティック補完的作業の助けを借りて,VRMモデルをオートマトン状態転送図表に変換した。最後に,VRMモデルからモデル検証ツール(nuXmv)までの自動モデル変換フレームワークを設計し,形式的仕様言語VRMと記号モデルチェッカーnuXmvの間のトランスレータを実装する。本論文では,いくつかの深さにおける著者らの翻訳と抽象化アプローチを議論し,いくつかの予備的例を用いてその実現可能性を説明した。Copyright The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 安全性 ,  意味論 ,  オートマトン ,  自動化 ,  言語 ,  構文論 ,  臨界 ,  変換 ,  *モデル ,  *検証 ,  形式的手法【計算機】 ,  モデル検査
準シソーラス用語： モデル検証 ,  *形式的検証 ,  開発プロセス ,  モデル変換 , 【Automatic Indexing@JST】

著者キーワード (5件)： VRMモデル ,  nuXmv ,  モデル検査 ,  モデル翻訳 ,  安全検証

分類 (1件)： 計算機システム開発  (JD02010R)

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