2024-03-29T09:58:08Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001028482023-11-14T00:51:14Z06164:06165:06522:07655
人工衛星のソフトウェアIV&VにおけるD-Caseを利用した短期間でのフォーマルメソッド適用Rapid Application of A Formal Method with D-Case in software IV&V for Artificial Satellitesjpn形式仕様http://id.nii.ac.jp/1001/00102825/Conference Paperhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=102848&item_no=1&attribute_id=1&file_no=1Copyright (c) 2014 by the Information Processing Society of Japan九州大学大学院システム情報科学研究院九州大学大学院システム情報科学研究院九州大学大学院システム情報科学研究院九州大学大学院システム情報科学研究院宇宙航空研究開発機構情報・計算工学センター宇宙航空研究開発機構情報・計算工学センター宇宙航空研究開発機構情報・計算工学センター宇宙航空研究開発機構情報・計算工学センター大森, 洋一日下部, 茂林, 信宏荒木, 啓二郎神戸, 大輔寺西, 誠川口, 真司梅田, 浩貴人工衛星の開発は軌道制御ハードウェア,基本ソフトウェア,ミッション固有機器など複数の専門家組織の分担により行われ,特にソフトウェア開発の初期段階における検証手段の確立が課題となっている.このように独立した組織間のコミュニケーションには仕様書が決定的な役割を果たす.フォーマルメソッドは,数理的なモデルにより対象を記述し開発の初期段階からの検証を可能とする.しかし,対象の仕様を理解するのに適した仕様書の記述項目や優先順位は,各専門家組織,たとえばソフトウェア開発者と検証者の間で必ずしも一致しない.このとき,関係者の間でフォーマルメソッドによるモデルの仕様全体における目的や位置づけを共有する必要がある.本研究では,検証目的に限定した情報のみを抽出することで、短期間でフォーマルなモデルを記述する手法を提案する.情報を限定するための手段として,検証すべき目的をゴールとするディペンダブルケース (D-Case) を作成・利用する.提案手法を実際の仕様書に対して適用したところ,D-Case の個別衛星へのカスタマイズ,仕様書とのマッピングにより,検証に必要な仕様理解に必要な時間を短縮できる,また不足している情報を明確に指摘できるといった成果が得られた.Development of an artificial satellite is collaboration of multiple specialist teams, such as orbit control hardware, basic software, and mission inherent instruments. Therefore, establishment of the verification method especially in the early stage of software development is still a problem. Specification plays decisive role in the communication among such independent teams. Formal methods can describe the target as a mathematical model and verify it in early development stage. However, the contents and priority of the specification for understanding the target is not necessarily in accordance among different teams, for example, between software developers and verifiers. Stakeholders of the development team need to share the purpose and importance of the formal model in whole the specification because all aspect can not be expressed in the model. We propose a method to compose a rapid formal model with a dependable case (D-Case) which conducted goal analysis. As case studies, applying the proposed method achieved that required time for specification understanding could be shortened and the lacked information could be clearly pointed out.ソフトウェアエンジニアリングシンポジウム2014論文集201427322014-08-252014-08-22