文献

J-GLOBAL ID：201702262563822061   整理番号：17A1629071

SPINに基づく飛行制御システム故障のモデル化と検証【Powered by NICT】

Flight control system failure modeling and verification based on SPIN

著者 (3件)： Wei Qianxin (School of Reliability and Systems Engineering, Beihang University, Beijing 100191, China) ,  Jiao Jian (School of Reliability and Systems Engineering, Beihang University, Beijing 100191, China) ,  Zhao Tingdi (School of Reliability and Systems Engineering, Beihang University, Beijing 100191, China)
資料名： Engineering Failure Analysis  (Engineering Failure Analysis)
巻： 82  ページ： 501-513  発行年： 2017年 
JST資料番号： W0684A  ISSN： 1350-6307  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： イギリス (GBR)  言語： 英語 (EN)

抄録/ポイント： 安全性が重要なシステム領域では,モデルベース安全解析は破壊評価と検証は,危険をもたらす可能性のあるシステムにおける故障およびそれらの組合せが存在するかどうかを検証するためにモデル検査を利用するためにますます一般的な方法である。形式的方法として,モデル検査は,安全要件を満たすかどうかを検証するシステムモデルの状態空間を調査する。Promelaと呼ばれる高度にプロセス記述言語に基づいて,スピンはシステムの実行を記述し,システムの故障危険を同定するためのランダムまたは対話型シミュレーションを実行するためにシステムモデルを分野適応できることが効率的なモデル検査器である。飛行制御システム(FCS)は航空機の安全が重要なシステムの一つである。本論文では,潜在的故障と危険をもたらす可能性のあるFCSのそれらの組合せであるかどうかをモデル検査による解析に用いることができる方法を提案した。Promelaによる記述されるシステムモデルはFCSの制御論理に基づくスピンプラットフォームを構築し,FCSのサブシステムは互いに相互作用するプロセスのための抽出した。検証すべき特性を線形時間論理(LTL)公式により定義される。FCSの故障の可能な組合せは,モデル検査によって生成された反例を分析することによって確認できる,FCSの危険をもたらす事故経路も見出すことができる。SPINモデル検査の結果は,提案した方法がFCSの危険をもたらす故障の組合せを検証し,見つけるために効果的に使用できることを示した。Copyright 2017 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【Powered by NICT】

シソーラス用語： *飛行制御 ,  *モデリング ,  システムモデル ,  安全解析 ,  モデル検査 ,  相互作用 ,  *故障 ,  航空機 ,  安全性 ,  *制御系 ,  仕様記述言語
準シソーラス用語： サブシステム ,  状態空間 ,  モデルベース ,  *SPIN , 【Automatic Indexing@JST】

著者キーワード (4件)： 故障モデリング ,  故障検証 ,  モデル検査 ,  飛行制御システム

分類 (5件)： 金属材料  (HC04020L) ,  パイプライン・空気・水力輸送  (QD05010T) ,  信頼性  (KB04040H) ,  線路構造,軌道材料  (RC07030B) ,  工業・技術設計  (HA05000Q)

タイトルに関連する用語 (5件)： SPIN ,  飛行制御 ,  システム故障 ,  モデル化 ,  検証