文献

J-GLOBAL ID：201202285775511291   整理番号：12A1032196

原子力工学分野におけるセーフティクリティカルソフトウェアのモデル検査

Model checking of safety-critical software in the nuclear engineering domain

著者 (6件)： LAHTINEN J. (VTT Technical Res. Centre of Finland, Systems Res., P.O. Box 1000, FI-02044 Espoo, FIN) ,  VALKONEN J. (VTT Technical Res. Centre of Finland, Systems Res., P.O. Box 1000, FI-02044 Espoo, FIN) ,  BJOERKMAN K. (VTT Technical Res. Centre of Finland, Systems Res., P.O. Box 1000, FI-02044 Espoo, FIN) ,  FRITS J. (Dep. of Information and Computer Sci., School of Sci., Aalto Univ., PO Box 15400, FI-00076 Aalto, FIN) ,  NIEMELAE I. (Dep. of Information and Computer Sci., School of Sci., Aalto Univ., PO Box 15400, FI-00076 Aalto, FIN) ,  HELJANKO K. (Dep. of Information and Computer Sci., School of Sci., Aalto Univ., PO Box 15400, FI-00076 Aalto, FIN)
資料名： Reliability Engineering & System Safety  (Reliability Engineering & System Safety)
巻： 105  ページ： 104-113  発行年： 2012年09月 
JST資料番号： D0980B  ISSN： 0951-8320  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： イギリス (GBR)  言語： 英語 (EN)

抄録/ポイント： 計装・制御(I&C)システムはセーフティクリティカルプロセスの運用で重要な役割を果たしている。ディジタルプログラマブル論理コントローラ(PLC)によって,システム確認と検証法に対する高度な要件を設定する複雑な制御タスクを可能となる。システムの総合検証では試験とシミュレーションが重要な役割を果たすが,制限されたシステム挙動の数が時間制限によって解析されるだけなので,包括的は評価には適していない。さらに開発ライフサイクルにおいて試験をするのは遅すぎ,そのために設計誤差の補正は高くつく。この論文では,原子力工業分野におけるソフトウェア開発での形式法の役割について論じる。システム検証の有望なアプローチとして,システム設計モデルの正しさを検証するためのモデル検査,計算機支援形式法を提出する。この論文の主な貢献は,原子力分野におけるセーフティクリティカルシステムをモデル化するための系統的方法を開発することにある。これまで検出されなかった誤差を見出す二つの事例研究をレビューする。さらに,モデル検査プロセスにおける信頼性を向上させるために取らなければならない行動についても論じる。Copyright 2012 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.

シソーラス用語： *ソフトウェア ,  *モデル検査 ,  原子力工学 ,  ソフトウェア開発 ,  計装 ,  無停電電源 ,  検証 ,  事例研究 ,  プロセス制御 ,  モデリング
準シソーラス用語： *セーフティクリティカルソフトウェア ,  UPS【電源装置】 ,  システム検証

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

タイトルに関連する用語 (3件)： 原子力工学 ,  セーフティクリティカルソフトウェア ,  モデル検査