<4D F736F F F696E74202D F8C608EAE8EE CC8E598BC6899E F815B834E F4A C982A882AF82E98C608EAE8EE C991CE82B782E98EE DD2E >

Size: px

Start display at page:

Download "<4D F736F F F696E74202D F8C608EAE8EE CC8E598BC6899E F815B834E F4A C982A882AF82E98C608EAE8EE C991CE82B782E98EE DD2E >"

よしおちとく
5 years ago
Views:

1 第 3 回形式手法の産業応用ワークショップ JAXA における形式手法に対する取組み ~ ソフトウェア IV&V における形式手法の活用事例 ~ 2012/11/12 宇宙航空研究開発機構情報計算工学センター吉川健 1

2 Summary JAXAの開発する主な宇宙機ソフトウェアについてソフトウェアエンジニアリング技術の取り組み IV&V(Independent Verification and Validation) とは IV&Vにおける形式手法の取り組み事例紹介分かったこと課題今後の計画 2

3 JAXA の開発する主な宇宙機ソフトウェアについて 3

4 JAXA の開発する主な宇宙機 4

5 宇宙分野のソフトウェアの種類と特徴人工衛星ロケット姿勢制御系データ処理系ミッション系スタートラッカー / GPSR などセンサー系など組込み系が中心最近は書換可能のものもあるアセンブラ C 言語再利用 / シリーズ化放射線の影響航法誘導制御系等高信頼性 / 多数決アセンブラ C 言語ハードリアルタイム宇宙ステーション管制システムマニュピュレータ実験装置など膨大な数のソフトウエア高い安全要求 (2 故障でも安全に!) コマンドデータ処理の独立性システム構成にクルーが入る Ada C 言語地上管制システム管制システム等安全性 C JAVA 言語 5

6 宇宙用ソフトウエアの置かれる状況組み込みソフトとの共通課題上流工程の不確定さ ( 要求元は? 決まらない?) 機能要求の増加と複雑化による検証の限界ハードウエア主体の文化開発の外注化の加速宇宙特有の問題容易に修理できない開発期間製品が単発 6

7 ソフトウェアエンジニアリング技術の取り組み 7

8 宇宙機搭載ソフトウエアの特徴と信頼性向上対策 8

9 宇宙分野のソフトウエアと安全確保の概要安全性信頼性確保のための取組み宇宙機ソフトウエア開発基本的動作 ( 標準等 ) 品質プログラム標準技術標準経験則を含めた教育プロセス改善各立場での改善サイクルメトリクスによる可視化独立検証及び有効性確認 (IV&V) 専門的観点のチェック新規技術の研究高信頼性 RTOS 検証高信頼性モデルベース開発健康維持基礎体力健康維持自己診断専門家による検査新規装置を使った検査 9

10 IV&V(Independent Verification and Validation) とは 10

11 ソフトウエア IV&V の概要ソフトウエア製品の正しさ及び品質をソフトウエアライフサイクルを通して評価するためのシステムエンジニアリングプロセス 11

12 IV&V 評価のイメージシステム仕様運用シナリオ安全要求ソフトウェア要求分析プロセスソフトウェア要求仕様ソフトウェア検証計画統合試験仕様統合試験プロセスソフトウェア設計プロセスソフトウェア設計仕様結合試験プロセス結合試験仕様ソフトウェア製作プロセス単体試験プロセスソースコード単体試験仕様開発成果物開発プロセス 12

13 IV&V における要求分析プロセスでの視点 ( 評価観点 )(1/2) No 観点サブ観点詳細観点 1 上位下位の追跡可能性システム仕様とのトレーサビリティ 2 上位下位の等価性システム仕様との等価性 3 整当該成果物とインタフェース仕様の追跡可能性インタフェース仕様とのトレーサビリティ 4 合同一機器内でのインタフェース仕様の等価性 5 性外部機器とのインタフェース仕様の等価性当該成果物とインタフェース仕様の等価性 6 地上システムとのインタフェース仕様 ( テレコマ ) の等価性 7 搭載ハードウェアとのインタフェース仕様の等価性 8 ソフトウェアへの機能要求とソフトウェア要求仕様の適合性 9 ソフトウェアへの性能要求とソフトウェア要求仕様の適合性 10 システム要求ソフトウェアへの要求との適合性ハードウェア構成とソフトウェア要求仕様の適合性 11 環境に対するソフトウェア要求仕様の適合性 12 検証方法による検証可能性 13 妥運用シナリオとソフトウェア機能の適合性 14 当運用シナリオとソフトウェア性能の適合性性運用シナリオとの適合性 15 運用に必要なテレメトリコマンドとソフトウェア機能の適合性 16 運用シナリオのソフトウェア検証計画への反映 17 ユーザ要求との適合性ユーザ要求に対するソフトウェア要求仕様の適合性 18 他の要求仕様案に対する現状ソフトウェア要求仕様の優位性現状ソフトウェア仕様の適正さ 19 適用する設計基準への合致 20 ソフトウェア検証の妥当性ソフトウェア検証計画の妥当性 13

14 IV&V における要求分析プロセスでの視点 ( 評価観点 )(2/2) No 観点サブ観点詳細観点 22 ソフトウェア要求仕様の記述解釈の非曖昧性 23 解釈の非曖昧性ソフトウェア検証計画の記述解釈の非曖昧性 24 正ソフトウェア要求仕様の値の非曖昧性 25 確ソフトウェア検証計画の値の非曖昧性性 26 ソフトウェア要求仕様の記述の無矛盾性複数記述間の無矛盾性 27 データ解釈の無矛盾性 28 条件に対する網羅性条件についての記述の網羅性 29 入出力の完全性機能処理の完全性 30 実行内容の完全性完 31 全入力データへの耐性設計値外の入力への耐性 32 性入力タイミングへの耐性 33 試験網羅性ソフトウェア要求仕様に対するソフトウェア試験仕様 ( 更新 ) の網羅性 14

15 IV&V における形式手法の取り組み事例紹介 15

16 形式手法の分類異論もあるかもしれませんがモデル検査形式仕様記述定理証明プロセス代数など 16

17 ソフトウェア開発の現状とこれまでの形式手法の活用ソフトウェア開発の現状現在のソフトウェア開発ではそのソフトウェア要求仕様が自然言語による文章や図表で記述されることが多いその結果として自然言語で記述することによる仕様の漏れや読み手による認識の齟齬が不具合混入の原因となる IV&V における形式手法の活用状態遷移や動作タイミングなどの評価においてはモデル検査技術である SpecTRM SPIN や Upaal を利用している現状主に文書レビューによる IV&V 評価が行われている箇所に対してモデル検査技術以外の形式手法を活用した評価手法を確立したい 17

18 これまでの取り組みモデル検査ツールの活用 SpecTRM SPIN UPPAAL モデル検査形式仕様記述定理証明プロセス代数など 18

19 事例 1: SpecTRM を中心とした導入事例 ~Model Chain 例 ~ 19

20 事例 1:SpecTRM を中心とした導入事例 ~ モデル検査技術の実プロジェクト適用における問題 ~ モデル検査などに頼りすぎシステム全体の重要な問題を見落とす領域知識の不足絞り込み粒度設定の誤りにより重大な問題を見逃すハード ( 環境 ) 人 ( 運用手順 ) の振舞いのモデル化の必要性連続値計算のようなアルゴリズム ( 制御則など ) の検証が困難 (Matlab SCADE などとの連携 ) モデル検査の得意とするところシミュレーションの得意とするところの観点の区別 20

21 近年の取り組み ( 引続き ) モデル検査ツールの利用形式仕様記述や定理証明器の活用 ( 要求仕様に対する評価にフォーカスしてみた ) モデル検査形式仕様記述定理証明プロセス代数など 21

22 分析対象としたフォーマルメソッド No 手法名主要なツール名区分 1 ACL2 ACL2 定理証明 2 Alloy Alloy Analyzer 形式仕様記述 3 B Atelier B 形式仕様記述 4 Event-B Rodin 形式仕様記述 5 CafeOBJ CafeOBJ 形式仕様記述 ( 代数仕様 ) 定理証明 6 CASL Hets 形式仕様記述 ( 代数仕様 ) 7 CCS The Concurrency Workbench of New プロセス代数 Century 8 CSP The Concurrency Workbench of New プロセス代数 Century 9 Coq Coq proof assistant 定理証明 10 Embedded Validator Embedded Validator 形式仕様記述 ( ブロック線図 ) モデル検査 11 HOL HOL 定理証明 12 Isabelle Isabelle 定理証明 13 LARCH Larch Prover 形式仕様記述 ( 代数仕様 ) 14 LOTOS CADP プロセス代数 15 OBJ3 OBJ3 形式仕様記述 ( 代数仕様 ) 定理証明 16 OCL HOL-OCL 形式仕様記述 17 Petri Nets なしペトリネット 18 PVS PVS 定理証明 19 SCADE Suite SCADE Suite 形式仕様記述 ( 同期型言語 ) モデル検査 20 SDL(Specification and Telelogic Tau SDL Suite 形式仕様記述 Description Language) 21 Simulink Design Verifier Simulink Design Verifier 形式仕様記述 ( ブロック線図 ) モデル検査 22 VDM VDM Tools Kit 形式仕様記述 23 Z Notation Community Z Tools 形式仕様記述 22

23 選定時の視点ソフトウェア要求仕様のモデリングに向くか? ツールとしての成熟度が高いか? ツールが定期的にメンテナンスされているか? No 区分符号意味 1 要求向き評価可能仕様の記述方法によっては評価可能評価不能 2 成熟度成熟未成熟 3 メンテ頻度本調査時点から過去 1~2 年以内に更新されている本調査時点から過去 3~5 年以内に更新されている本調査時点から過去 5 年以上更新されていない 23

24 選定したフォーマルメソッド手法名主要なツール名区分概要要求向き? 成熟度? メンテ頻度備考 Event-B Rodin 形式仕様記述 B 言語を基にした形式仕様記述手法記述したモデルに不変式を記述しておくことで定理証明による検証が可能利点抽象度の高い仕様もそれなりにモデル化できる段階的詳細化 (refinement) を記述する仕組みを備えている Rodin(Event-B プラットフォーム ) のライセンスは Common Public License Version 1.0 (CPL). 商用利用も支障なし上述の AtelierB も EventB に対応している VDM CCS VDM Tools Kit The Concurren cy Workbench of New Century 形式仕様記述欠点集合論を用いたモデル化には慣れが必要自動的な検証ができない C 言語にも似た記述方式で仕様を記述する入出力のみを規定する方式と振る舞いを含めて記述する方式を混在させることが可能定理証明による形式的な検証はサポートしていない利点記述方法は比較的なじみやすい仕様アニメーションができる欠点定理証明による形式的な検証はサポートしていないプロセス並列実行されるプロセスを記述するための理論デッドロック代数などを検出可能ツールは複数存在利点比較的習得が容易 VDM Tools Kit は商用利用は有償オープンソースの環境として Overture( がある無償で商用利用も可能ただしプロジェクトの成熟度は低い The Concurrency Workbench of New Century ( n=com_content&view=article&id=54&itemid=65 ) 最終アップデートは 2010/12/14 24

25 事例 2:Event B を用いた導入事例 Event-B を用いたシステム仕様とソフトウェア要求仕様との等価性を評価 1 上位仕様のモデル 2 下位仕様のモデル (1) 上位仕様を Event-B で記述する (2) 下位仕様を Event-B で記述する 3 ツールによる証明 (3) ツールによる証明を行い結果を確認するあるコマンドを受信した際の状態遷移がシステム仕様とソフトウェア要求仕様とで一致していないことが検出された 25

26 事例 3:VDM SL を用いた導入事例 (1/2) VDM-SL を用いたソフトウェア要求仕様に対するソフトウェア試験仕様の網羅性の評価 (1) 試験対象の機能について要求仕様を VDM-SL で記述する (2) 試験ケースを VDM- SL で記述する (3) 仕様アニメーションにより試験ケースを実行する (4) カバレッジ測定コマンドでカバレッジを確認する 1 要求仕様の 8% に対する試験仕様が漏れている 2 要求仕様において試験仕様から漏れている箇所を識別する 26

事例 3:VDM SL を用いた導入事例 (2/2) ( 要求仕様書の記述 ) 過去に再生したファイル領域を再ダウンリンクしたい場合その領域を上書き保護と設定する再生履歴 No をコマンドパラメータとして上書き保護設定コマンドにより上書き保護を設定できること上書き保護は 2 つまで設定できそれぞれ上書き保護 1 上書き保護

27 事例 3:VDM SL を用いた導入事例 (2/2) ( 要求仕様書の記述 ) 過去に再生したファイル領域を再ダウンリンクしたい場合その領域を上書き保護と設定する再生履歴 No をコマンドパラメータとして上書き保護設定コマンドにより上書き保護を設定できること上書き保護は 2 つまで設定できそれぞれ上書き保護 1 上書き保護 2 として管理されなければならない上書き保護設定時上書き保護 1 2 ともに使用されていない場合は上書き保護 1 が使用されなければならない上書き保護 1 がすでに使用済みの場合上書き保護 2 が使用されなければならない上書き保護が 2 つとも設定されている場合は上書き保護設定コマンドはリジェクトされなければならない 27

28 分かったこと課題今後の計画 28

29 事例からわかったこと課題 (1/2) モデル検査ツールと同様にフォーマルメソッド固有の検証証明による不具合 ( の原因 ) の発見だけでなくフォーマルメソッドによるモデリングそのものによる効果も高いモデリングするだけでも十分効果がある仕様記述言語やプロセス代数を用いた評価によりモデル検査による評価に加えて以下の評価が可能システム仕様とソフトウェア要求仕様の等価性同一機器内でのインタフェース仕様の等価性運用シナリオとソフトウェア機能の適合性ソフトウェア要求仕様に対するソフトウェア試験規格の網羅性 29

30 事例からわかったこと課題 (2/2) モデル化にあたり多くの工数が必要短時間化のための取組み / やり方が必要定理証明系ツールの活用について未検討定理証明系ツールで何ができるのかを含め適用方法適用箇所の調査が必要 30

31 今後の計画 IV&V 業務における適用範囲の拡大更なる超上流フェーズへの適用 IV&V 研究成果のモデル化に関連した研究への適用モデルベース開発研究等モデリングの効率化モデリングの標準化マニュアル化モデル検査形式仕様記述系ツール以外 ( 定理証明系など ) の活用の検討 31

32 ご静聴ありがとうございました形式手法普及促進セミナー 2012in 32