UMLを用いたシステム運用管理プロセスの形式的表現および妥当性検証

• Item type: Journal(1)
• 公開日: 2009-02-15
• タイトル: UMLを用いたシステム運用管理プロセスの形式的表現および妥当性検証
• タイトル / 言語: en
• タイトル: Formal Description and Verification of System Management Processes Using UML
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 特集：組織における情報システム開発
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: 情報と情報技術
• 著者所属: 株式会社富士通研究所
• 著者所属: 株式会社富士通研究所
• 著者所属: 株式会社富士通研究所
• 著者所属: 株式会社富士通研究所
• 著者所属(英): en
• 著者所属(英): Fujitsu Laboratories Limited.
• 著者所属(英): en
• 著者所属(英): Fujitsu Laboratories Limited.
• 著者所属(英): en
• 著者所属(英): Fujitsu Laboratories Limited.
• 著者所属(英): en
• 著者所属(英): Fujitsu Laboratories Limited.
• 著者名: 菊池, 慎司; 土屋, 哲; 関口, 敦二; 勝山, 恒男
• 著者名(英): Shinji, Kikuchi; Satoshi, Tsuchiya; Atsuji, Sekiguchi; Tsuneo, Katsuyama
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 今日，システムの運用管理においては，その信頼性向上のために，セキュリティや内部統制といった様々な観点からシステム運用管理作業（プロセス）をチェックすることが求められている．しかし現状では，運用管理プロセスは自然言語によって記述されているため，定められたプロセスが，与えられた制約条件を充足できるかどうかを判定するのが非常に困難である．この現状を打破するためには，プロセスと要件を形式的に記述し，その妥当性の機械的判定を可能にすることが必要である．そこで本論文では，UMLを用いたシステム運用管理プロセスの形式的記述方法と，その妥当性をモデル検査により検証する手法を提案する．本手法は，システム運用管理プロセスの内容を，3種類のUML図を用いて厳密に記述することと，それらの図から運用プロセスの挙動モデルを構築することで，図の間の不整合を形式的手法によって検出することを可能にする．また，モデル検査ツールNuSMVを用いて本手法の実装を行い，それを例題に適用することで，短時間で運用プロセスの検証が可能であることを示す．本手法によりシステム運用プロセスの妥当性検証を機械的に支援することで，システム運用管理の信頼性向上が可能になると考えられる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In order to improve reliability in today's system management tasks, it is required to define system management processes formally and to check the validity of them from various viewpoints such as security or compliance with policies. It is, however, difficult to determine whether system management processes defined in natural language can satisfy given constraints. Therefore, methods to check the system management processes' validity are highly demanded. In this paper, we propose a method to design system management processes and verify their consistency. We first define a formal description method for system management processes using three types of UML diagrams which enable us to design system management processes from different aspects strictly. Next, we construct state transition models representing the processes' behavior. Then, we verify the process definition by applying model checking technique for the models. We implement the verification function using model checker NuSMV and show that our method can check the validity of process in a short period of time through our case study. Our method will be able to contribute to improve the reliability of system management operations by helping system administrators define valid processes.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 50, 号 2, p. 637-650, 発行日 2009-02-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764