MATLAB EXPO 2014 Dry Run 0 モデル検証＆Polyspace

Size: px

Start display at page:

Download "MATLAB EXPO 2014 Dry Run 0 モデル検証＆Polyspace"

ゆりないざわ
4 years ago
Views:

1 Polyspace によるソフト不具合修正のフロントローディング MathWorks Japan Application Engineering アプリケーションエンジニアリング部 Application Engineer アプリケーションエンジニア Fred Noto 能戸フレッド 2014 The MathWorks, Inc. 1

2 Polyspace の静的解析ソリューション Polyspace はコードの信頼性を確保するための機能を提供自動生成コードハンドコード検証可能コード証明形式手法 (No False negative) Polyspace Code Prover ファイル単位プロジェクト単位検証可能エラー検出エラー予防バグ検出 (False negative) Polyspace Bug Finder コンパイラー警告コーディングルールコードメトリックス Polyspace Bug Finder TM Polyspace Code Prover TM 2

3 このようなことでお困りでしょうか? 動的テスト完了後製品リリース後にエラーが判明した! C Code Review Integration Test Hardware Testing! C CC C C Unit Test source1.c source2.c source3.c 全てのエラーを検出できた? 3

4 このようなことでお困りでしょうか? ソフトウェアバグが残されて検証を進めている可能性 Code Review Integration Test Hardware Testing Unit Test = バグ後段階で検出したバグは修正コストが高い! 製品リリース後のバグはより危険! 4

5 コード検証の目的要求仕様通りの設計かを確認要求仕様に問題ないことを確認 C 動的検証 C CC 不具合 ( ゼロ割等 ) がないことを確認コーディングルール準拠の確認! C 静的検証 C 適切な検証手法を使用してプロセスを効率化 5

6 モデルベースデザインでも自動生成コードとハンドコードと統合していませんか? インターフェイス RTOS 等制御アルゴリズム故障診断自動生成コード ( モデル ) S-Function ( ハンドコード ) コード検証が必要になります 6

設計の簡素化カバレッジ確認非到達状態遷移検出テストケース生成コード検証スタンダード準拠確認

7 モデル検証とコード検証の役割分担シミュレーション設計エラー検出機能的エラー検出数学エラー検出カバレッジエラー検出手戻りを最低限にするには早期の検証が求められますモデル検証モデル標準確認設計エラー検出設計の簡素化カバレッジ確認非到達状態遷移検出テストケース生成コード検証スタンダード準拠確認エラー不在の証明ハンドコードの検証実装エラー検出 Polyspace Bug Finder Polyspace Code Prover 7

8 Polyspace Bug Finder のスピーディー解析バグ検出コード作成後すぐに欠陥を検出修正コーディングルールチェックエラー予防と再利用性向上 MISRA 準拠を確認コードメトリックス解析コードの複雑度を測定開発プロセスの上流で不具合を発見! コードを統合前に多くの欠陥を修正! コード開発の効率に繋がる! 時間を掛けずに大部分のバグを識別コード作成修正 Bug Finder 解析レポート自動生成素早い欠陥検出修正を可能とする Polyspace Bug Finder 8

9 コーディングルールの確認 MISRA C チェッカー MISRA AC AGC 自動生成コード用 MISRA C++ チェッカー JSF++ チェッカーカスタマイズルールのオンオフ設定カスタムルール Polyspace コードルールチェックによりエラーの予防可能 9

Polyspace Bug Finder: 検出項目リスト Numerical Integer division by zero Float division by zero Integer conversion overflow Unsigned integer conversion overflow Sign change integer conversion overflow Float

10 Polyspace Bug Finder: 検出項目リスト Numerical Integer division by zero Float division by zero Integer conversion overflow Unsigned integer conversion overflow Sign change integer conversion overflow Float conversion overflow Integer overflow Unsigned integer overflow Float overflow Invalid use of std. library integer routine Invalid use of std. library float routine Shift of a negative value Shift operation overflow Static memory Array access out of bounds Null pointer Pointer access out of bounds Unreliable cast of function pointer Unreliable cast of pointer Invalid use of std. library memory routine Invalid use of standard library string routine Arithmetic operation with NULL pointer Other Race condition Invalid use of other standard library routine Large pass-by-value argument Assertion Format string specifiers and arguments mismatch Dynamic memory Use of previously freed pointer Unprotected dynamic memory allocation Release of previously deallocated pointer Invalid free of pointer Memory leak Programming Invalid use of = operator Invalid use of == operator Declaration mismatch Invalid use of floating point operation Wrap-around on unsigned integer Missing null in string array Qualifier removed in conversion Wrong type used in sizeof Dataflow Write without further read Non-initialized variable Non-initialized pointer Variable shadowing Missing or invalid return statement Unreachable code Dead code Partially accessed array Uncalled function Pointer to non initialized value converted to const pointer Code deactivated by constant false condition Polyspace Bug Finder GUI *) bold: checks that are part of Bug Finder analysis only 10

Polyspace Code Prove でコードの正しさを証明 Quality( 品質 )

テストケースは不要対応言語 :C/C++/Ada Process( プロセス ) ランタイムエラーの早期検出

グリーン : 正常ランタイムエラーが存在しないレッド : エラー実行される度にランタイムエラーグレー :

$pointer_arithmetic (void) { int array[100]; int *p =$ $(get_bus_status() > 0) { if (get_oil_pressure() > 0) { *p$ $= 5; else { i++; i = get_bus_status(); if (i >= 0) { *(p$

11 Polyspace Code Prove でコードの正しさを証明 Quality( 品質 ) ランタイムエラーの証明測定向上管理 Usage( 使用方法 ) コンパイルプログラム実行テストケースは不要対応言語 :C/C++/Ada Process( プロセス ) ランタイムエラーの早期検出自動生成コードハンドコードの解析可能コードの信頼性を測定実機実験前にコード信頼性を確保して手戻りを削減グリーン : 正常ランタイムエラーが存在しないレッド : エラー実行される度にランタイムエラーグレー : デッドコード無実行オレンジ :Unproven 条件によってランタイムエラーパープル :Violation MISRA-C/C++, JSF++ 変数値範囲ツールチップ static void pointer_arithmetic (void) { int array[100]; int *p = array; int i; for (i = 0; i < 100; i++) { *p = 0; p++; if (get_bus_status() > 0) { if (get_oil_pressure() > 0) { *p = 5; else { i++; i = get_bus_status(); if (i >= 0) { *(p - i) = 10; variable I (int32): [0.. 99] assignment of I (int32): [ ] Polyspace は全ての実行パスの結果を証明する! 11

12 Polyspace Code Prover によるランタイムエラー有無の証明 C run-time checks Unreachable Code Out of Bounds Array Index Division by Zero Non-Initialized Variable Scalar and Float Overflow (left shift on signed variables, float underflow versus values near zero) Initialized Return Value Shift Operations (shift amount in 0..31/0..63, left operand of left shift is negative) Illegal Dereferenced Pointer (illegal pointer access to variable of structure field, pointer within bounds) Correctness Condition (array conversion must not extend range, function pointer does not point to a valid function) Non-Initialized Pointer User Assertion Non-Termination of Call (non-termination of calls and loops, arithmetic expressions) Known Non-Termination of Call Non-Termination of Loop Standard Library Function Call Absolute Address Inspection Points C++ run-time checks Unreachable Code Out of Bounds Array Index Division by Zero Non-Initialized Variable Scalar and Float Overflow Shift Operations Pointer of function Not Null Function Returns a Value Illegal Dereferenced Pointer Correctness Condition Non-Initialized Pointer Exception Handling (calls to throws, destructor or delete throws, main/tasks/c_lib_func throws, exception raised is not specified in the throw list, throw during catch parameter construction, continue execution in except) User Assertion Object Oriented Programming (invalid pointer to member, call of pure virtual function, incorrect type for this-pointer) Non-Termination of Call Non Termination of Loop Absolute Address Potential Call Green: reliable safe pointer access Red: faulty out of bounds error Gray: dead unreachable code Orange: unproven may be unsafe for some conditions static void pointer_arithmetic (void) { int array[100]; int *p = array; int i; for (i = 0; i < 100; i++) { *p = 0; p++; if (get_bus_status() > 0) { if (get_oil_pressure() > 0) { *p = 5; else { i++; i = get_bus_status(); if (i >= 0) { *(p - i) = 10; C++ Specific Checks (positive array size, incorrect typeid argument, incorrect dynamic_cast on reference) 12

engineers Software engineers and/or Quality engineers BF 実装

13 Polyspace のワークフロー BF CP Bug Finder Code Prover 要求仕様ソフトウェアリリース BF CP Quality Assurance Engineers モデル検証設計ソフトウェア統合テスト BF Design engineers Software engineers and/or Quality engineers BF 実装ソフトウェア単体テスト CP Software engineers Software engineers and/or Quality engineers 13

14 MathWorks ツールチェーンへの統合 PolyspaceのSimulink 連携機能でモデル修正が容易 Simulink 環境からPolyspace 解析を実行 Polyspaceで発見した不具合をSimulinkモデルで強調表示モデルの入力パラメータ情報を利用 14

15 Polyspace のメリット早期段階でのコード検証によりスムーズな流れを実現 C C Code Review Polyspace Bug Finder Polyspace Code Prover Unit Test C CC source1.c source2.c source3.c Integration Test Hardware Testing C 15

16 Polyspace ソースコード静的検証 ~ まとめ ~ Polyspace Bug Finder で素早くコードの欠陥を検出! 早期段階で不具合の修正が可能! Polyspace Code Prover でクリティカルシステムにランタイムエラーの有無を証明! 時間を掛けずに大部分のバグを識別両ツールを使用して効率的にソフトウェアの品質を管理向上! 形式手法の解析によるコード信頼性 Simulink 環境から実行可能ファイルプロジェクト単位で使用可能安全なコードを確保して実機実験へ 16

17 トレーニングコンサルティングサービス投資効果トレーニングサービス定期トレーニング ; 東京名古屋大阪にて定期開催基礎コース (11) 応用コース (11) 専門コース (4) をご提供オンサイトトレーニング ; お客様サイトにて開催ご要望に応じて 3 つのレベルでカリキュラムのカスタマイズが可能投資対効果の最大化コンサルティングサービスカスタム Jumpstart ; 顧客モデルをベースにした短期集中型ツール導入サポート Advisory Service; 顧客 Project に合わせた中長期アドバイザリサービス 17

18 制御設計関連トレーニングコース MATLAB 関連 MATLAB 基礎 MATLAB によるデータ処理と可視化 MATLAB のプログラミング手法 MATLAB の最適化手法 MATLAB と Simulink による制御設計 Simulink 関連 MATLAB/Simulink によるモデルベース開発 Simulink 基礎基礎応用コース名基礎期間 3 日期間 1 日 2 日 1 日 2 日期間 2 日期間 2 日応用 SimPowerSystems による電力系統の物理モデリング Simulink への外部コードの取り込み Simscape によるマルチドメインシステムの物理モデリング SimMechanics による力学系の物理モデリング期間 1 日 1 日 1 日 1 日 Simulink モデルの検証と妥当性確認 Simulink モデルの管理 Stateflow 関連 Stateflow 基礎コード生成関連リアルタイムコードの生成およびテストの基礎 Embedded Coder による量産向けコード生成 Polyspace 関連 Polyspace によるコード検証専門基礎基礎専門専門期間 1 日 2 日期間 2 日期間 1 日期間 3 日期間 2 日 18

19 Thank You For Your Attention ご清聴ありがとうございました 2014 The MathWorks, Inc. MATLAB and Simulink are registered trademarks of The MathWorks, Inc. See for a list of additional trademarks. Other product or brand names may be trademarks or registered trademarks of their respective holders. 19

Presentation Title

Presentation Title 次世代システムに求められるソフトウェア検証技術 ~ 静的解析の価値と有効性 ~ MathWorks Japan Application Engineering Application Engineer 能戸フレッド Fred Noto 2017 The MathWorks, Inc. 1 Polyspace のコード証明 Polyspace は品質保証の上検証工数の削減に貢献しますコード内のエラーをどう検出しますか?