中小企業の形式手法への取り組み中小企業の形式手法への取り組み株式会社サニー技研ソフトウェア基盤技術課米田真之中本加那

(1)

中小企業の形式手法への取り組み

株式会社サニー技研ソフトウェア基盤技術課

米田真之、中本加那

(2)

アジェンダ

1. 自社（自己）紹介

2. 機能安全と形式手法

3. 主な活動内容

－機能安全活動

－名産研活動

4. 各研究会での企業としてのアプローチ

5. 企業での形式手法導入にむけて

6. まとめ

(3)

•自社紹介

会社名株式会社サニー技研

Sunny Giken Inc.

設立 1974年7月資本金 5,000万円（払込）代表者中村和彦社員数 70名事業内容：－マイクロコンピュータを応用した各種機器の開発・製造・販売－各種工場のFAシステム開発－車載LANに関するツール開発・販売・適合試験－携帯電話機など情報通信機器のソフトウエアの開発－半導体試験装置の開発＜本社/伊丹開発センター＞〒664-0858 兵庫県伊丹市西台3-1-9 TEL：072-775-0339 / FAX：072-778-1709 ＜名古屋事業所＞〒460-0003 名古屋市中区錦2-19-18 丸三証券名古屋ビル加入団体： TOPPERS

(4)

(5)

•機能安全とは

機能的な工夫（安全機能）を導入して、許容できるレベルの安全を確保

すること。機能そのものの危険性を取り除くこと（本質安全）と比較され

る。

_全安全_全安全_全安全_{全安全ライフサイクル}_{ライフサイクル}_{ライフサイクル}_{ライフサイクル} 9 安全関連系： E/E/PE 実現(ソフトウェア安全ライフサイクル) 10 安全関連系：その他の技術実現 11 外的リスク軽減施設実現 6 7 8 すべての計画作成すべての適用及び保全計画すべての安全妥当性確認計画すべての設置及び引渡し計画 1 概念 2 すべての対象範囲の定義 3 潜在危険及びリスク解析 4 すべての安全要求事項 5 安全要求事項の割り当て 12 すべての計画及び引渡し 13 すべての妥当性確認 14 すべての運用、保全及び修理 ₁₅ _{すべての部分改修及び改造} 適切な安全ライフサイクルに戻る全安全全安全全安全全安全ライフサイクルライフサイクルライフサイクルライフサイクル 9 安全関連系： E/E/PE 実現(ソフトウェア安全ライフサイクル) 10 安全関連系：その他の技術実現 11 外的リスク軽減施設実現 6 7 8 すべての計画作成すべての適用及び保全計画すべての安全妥当性確認計画すべての設置及び引渡し計画 1 概念 2 すべての対象範囲の定義 3 潜在危険及びリスク解析 4 すべての安全要求事項 5 安全要求事項の割り当て 12 すべての計画及び引渡し 13 すべての妥当性確認 14 すべての運用、保全及び修理 ₁₅ _{すべての部分改修及び改造} 適切な安全ライフサイクルに戻る 9 安全関連系： E/E/PE 実現(ソフトウェア安全ライフサイクル) 9 安全関連系： E/E/PE 実現(ソフトウェア安全ライフサイクル) 10 安全関連系：その他の技術実現 10 安全関連系：その他の技術実現 11 外的リスク軽減施設実現 11 外的リスク軽減施設実現 6 7 8 すべての計画作成すべての適用及び保全計画すべての安全妥当性確認計画すべての設置及び引渡し計画 1 概念 1 概念 2 すべての対象範囲の定義 2 すべての対象範囲の定義 3 潜在危険及びリスク解析 3 潜在危険及びリスク解析 4 すべての安全要求事項 4 すべての安全要求事項 5 安全要求事項の割り当て 5 安全要求事項の割り当て 12 すべての計画及び引渡し 12 すべての計画及び引渡し 13 すべての妥当性確認 13 すべての妥当性確認 14 すべての運用、保全及び修理 14 すべての運用、保全及び修理 ₁₅₁₅ _{すべての部分改修及び改造}_{すべての部分改修及び改造} 適切な安全ライフサイクルに戻る

機能安全規格は国際規格であ

る「IEC 61508」をベースとして

おり、製品カテゴリごとに専用

の規格が策定されている。

(6)

•安全規格、IEC61508とSIL（安全度水準）

IEC61508には安全度水準（SIL＝Safety Integrity Level）が定められて

おり、故障の発生頻度により４段階に分けられている。

10

－6

以上 10

－5

未満

10

－2

以上 10

－1

未満

1

10

－7

以上 10

－6

未満

10

－3

以上 10

－2

未満

2

10

－8

以上 10

－7

未満

10

－4

以上 10

－3

未満

3

10

－9

以上 10

－8

未満

10

－5

以上 10

－4

未満

4 高頻度作動要求又は

連続モード運用

（単位時間当たりの

危険側故障確率［1／時間］）

低頻度作動要求モード運用

（作動要求当たりの設計上の

機能失敗平均確率）

安全度水準

（SIL）

(7)

•安全規格、IEC61508とSIL（安全度水準）

SILのレベルによって半形式手法、形式手法が推奨（または強く推奨）

されている

HR

R

信頼ができて検証されたモジュール

などの使用

HR

構造化プログラミング

HR

R

設計及びコーディング規約

HR

モジュラー・アプローチ

HR

R

-防衛プログラミング

HR

R

コンピュータ支援による設計ツール

HR

R

-形式手法

HR

R

半形式手法

HR

構造化手法

SIL-4

SIL-3

SIL-2

SIL-1

技法

(8)

V字開発モデル

•形式手法とは

数学的理論を背景にしたシステムの設計及び検証の手法。

自然言語で書かれた仕様を専門の言語で記載することにより、あいまいさや矛盾を

排除する。自動証明器により数学的正しさを証明することも出来る。

システム全体を完全に形式化するのではなく、システムの一部を形式化する、ライト

ウェイトな形式手法がとられることが多い。

要求

仕様

アーキテクチャ設計

モジュール設計

コーディング

形式手法による検証

評価

(9)

•各手法の紹介

各活動（後述）にて扱った手法

番外で調査、実践した手法（モデル検査）

-ありありありあり紹介資料あり MITライセンス -Alloy -あり -ありあり -GPL -ISO/IEC 13568 :2002 Z記法 CZT -ありありありあり紹介資料あり CPL -B/EventB Rodin＋PlugIn ありあり -あり公式サポート検証は無償 C++ソースコード生成機能は有償 -ISO_IEC_13817-1 :1997 VDM/VDM++ VDMTools 国内適用例適用例シミュレート自動検証証明課題日本語資料有償/無償時間遷移規格化手法ありありありあり -紹介資料あり SPINパブリックライセンスあり -Promela SPIN ありありあり -公式サポート有償あり -UPPAAL

(10)

(11)

その

その前

前

前に

に

に・・・

に

・・・

• 形式手法の企業としての導入障害

1. 必要な知識や環境が不明

2. 形式手法自体の(特に日本語での)情報量が少ない

• 中小企業での採択の難しさ

1. 認知度の低さ(導入の効果)

2. 導入コスト(費用対効果)

3. 手軽さが無い

- ツールの使用が想定される人にとってはハードルが高い？

- 手軽なツールは有償が多い

(12)

（（（（株株株）株）））ヴィッツヴィッツヴィッツヴィッツ ((((株株株株))))サニーサニーサニーサニー技研技研技研技研東海東海東海東海ソフトソフトソフトソフト((((株株株))))株アイシン精機(株) (株)東海理化トヨタ自動車(株) 名古屋市工業研究所北海道立工業試験場 (株)豊通エレクトロニクス評価依頼評価依頼評価依頼評価依頼評価依頼評価依頼評価依頼評価依頼評価結果評価結果評価結果評価結果評価結果評価結果評価結果評価結果アイシンAW(株) 日本システム安全研究所名古屋大学組込みシステム研究センター産業技術総合研究所：システム検証研究センター筑波大学 (株)ルネサステクノロジコンサルタントコンサルタントコンサルタントコンサルタントコンサルタントコンサルタントコンサルタントコンサルタントアドバイザアドバイザアドバイザアドバイザアドバイザアドバイザアドバイザアドバイザ

平成

平成18年度

年度

年度から

から

から戦略的基盤技術高度化支援事業

戦略的基盤技術高度化支援事業

戦略的基盤技術高度化支援事業（

（（

（中小企業基盤整備機

中小企業基盤整備機

構

構）

））

）

「

「「

「機能安全対応自動車制御用

機能安全対応自動車制御用

機能安全対応自動車制御用プラットフォーム

機能安全対応自動車制御用

プラットフォーム

プラットフォームの

プラットフォーム

の

の開発

開発

開発」

」」

」

における

におけるCAN/FlexRay通信

通信

通信ミドルウェア

通信

ミドルウェア

ミドルウェアの

の

研究開発

研究開発を

を

を実施

実施

•機能安全活動（終了）

(13)

•機能安全活動（終了）

「機能安全対応自動車制御用プラットフォームの開発」

国内自動車メーカが機能安全対策を必要とした時に、対応された基盤

ソフトウェアが存在することと、機能安全対策に必要な対応項目の選

択および重要度を理解していることを目標とした、国内の機能安全に

対する取り組み

IEC 61508では、SIL2 以上の安全度水準で形式手法の使用を推奨し

ている。企業が開発現場への導入を検討する場合に必要な情報を得

るため、形式手法導入の準備段階として、手法調査のためのグループ

を組織し、いくつかの手法に関して試用と評価を行った。

行った手法：Bメソッド、VDM、Z記法

(14)

•名産研活動（現在活動中）

正式名称：財団法人名古屋産業科学研究所

組込みシステム形式手法研究会

目的：本研究会では、組込みソフトウェアおよび組込みシステムを主な対象とし、

形式仕様記述及び形式検証技術によるシステム設計及び検証の実例を積み上げ、

産業応用上の知見を蓄積する。そして、利用上の知見や技術的な課題を整理し、

今後、研究会の成果を公開することで産業界の技術向上に資することを目指す。

活動内容： Alloy、Event-B、プログラム検証ツール(BLAST, SDV など) などの手法や

ツールの調査及び試行

産：アイシンコムクルーズ

サニー技研

東海ソフト

東海理化

日本機能安全

メルコ・パワー・システムズ

官：名古屋市産業科学研究所

名古屋市工業研究所

産業技術総合研究所

学：名古屋大学

(15)

•名産研活動（現在活動中）

参加メンバー (組織名50音順・敬称略) 責任者服部忠（名古屋産業科学研究所）副責任者結縁祥治（名古屋大学）メンバー深津隆志（アイシン・コムクルーズ）尾仲洋和（サニー技研）米田真之（サニー技研）中本加那（サニー技研）水口大知（産業技術総合研究所）岡村真吾（東海ソフト）服部智幸（東海ソフト）足立秀和（東海理化）藤沢寿郎（名古屋産業科学研究所）小川清（名古屋市工業研究所）斉藤直希（名古屋市工業研究所）吉岡律夫（日本機能安全）早水公二（メルコ・パワー・システムズ）

研究会

研究会の

の

の活動状況

活動状況

昨年度は Alloy、Event-B、プログラム検

証ツール(BLAST, SDV など) などの手法

やツールの調査及び試行を行い、利用方

法などについての情報交換を行いました。

今年度も名古屋大学を中心とした各参

加組織の会議室を利用し、およそ2ヶ月に

一度の割合で開催しています。ご興味の

ある方はご連絡ください。

連絡先：

名古屋市工業研究所電子情報部

斉藤直希

E-mail:

[email protected]

(16)

(17)

•各研究会での企業としてのアプローチ

技術者としてあまり触れる事の無かった形式手法だが、産官学のプロ

ジェクトに参加する事で様々な手法を知る機会を得た。

↓

今度は得た知識をいかに企業として生かすか、ビジネスに結びつける

か、導入におけるメリットやデメリットは何かを見極めていく必要がある。

↓

研究会の中でより実務に即した例題を提示し、実践していった。

(18)

•試用例：ドアロック仕様検証（VDM-SL）

機能安全活動中に弊社から提示

↓

調査や、例題の試用に留まっていた活動において

実際の開発において想定される事象に近い例題を

提示。研究会において各手法の実践の足がかりを

作る事になった

仕様

① 車速、ドライバ席のオールロックボタン、チャイルドロック設定(リア席左右)でドライバ席、

コドライバ席、リア左席、リア右席の４つのドアが開錠が可能かチェックする

② ドライバ席は車速が15km/hを超えている場合のみアンロック不可

③ コドライバ席はドライバ席の条件に加えてドライバ席のオールロックボタンがONの場合

アンロック不可

④ リア席は②、③の条件に加え、左右それぞれのチャイルドロックがONならばアンロック

不可

ドライバ席

コドライバ席

リア右席

リア左席

(19)

•試用例：ドアロック仕様検証（VDM-SL）

VDM記述

(20)

•実践例：ソフトウェアウォッチドッグ仕様検証（VDM++）

ソフトウェアウォッチドッグ

（Ｓ/ＷＷ/Ｄ）

マイコンなどのハードウェアに搭載

されているウォッチドッグ機能をソ

フトウェアで実現したもの。

仮想ウォッチドッグはＯＳ等で複数

のタスクが起動する際に、各タスク

が正常に起動または終了している

かを監視し、異常時に通知する。

同じ仕様での複数人（共に企

業人）での記述に挑戦した

(21)

•実践例：ソフトウェアウオッチドッグ仕様検証（VDM++）

元となる仕様

•複数の仮想W/Dとそれをとりまとめるモジュールで

構成される

•とりまとめモジュールはH/Wより取得した時間を各

仮想W/Dに提供する

•仮想W/Dは内部の時間が閾値に達するかを判定し、

とりまとめモジュールに対しOK/NG を通知する

•仮想W/Dは外部からのリセット要求で内部の時間を

リセットする

•仮想W/DからNG 通知を受けたとりまとめモジュール

はH/Wに対しリセットを要求する

同じ仕様での複数人（共に企業人）での記述に挑戦した

(22)

•実践例：ソフトウェアウオッチドッグ仕様検証（VDM++）

(23)

•実践例：ソフトウェアウオッチドッグ仕様検証（VDM++）

記述結果（内容）比較

同じ仕様でも両者で記述に大きな違いが出てしまっている

・閾値の初期値が1

・閾値の初期値が5

・tickで時刻を変え、observeで聞きに行く

・tickで時刻を変えて、更にチェックする

・W/Dクラスを個別にADD/REMOVE可能

・W/DクラスのADD/REMOVEが無い

・変更したい場合は、全てを再登録する必要

あり

・W/Dクラスを集合で扱う

・W/Dクラスを配列で扱っており、何番目の

仮想W/Dかがわかる

・提供しない

・現在時間、閾値、状態を各 W/D毎に提供

し、とりまとめクラスからも見ることができる

・現在時間を保持しない

・リセットされてからリミットまでの時間を持つ

・システムの現在時間を保持する

・リセットすることで、前回の現在時間に合わ

せられる

別メンバー

弊社

(24)

•実践例：ソフトウェアウオッチドッグ仕様検証（VDM++）

考察：

1. 両者ともにかなり実装よりな記述になってしまっていた

→プログラマなのでついコーディングしてしまう？

2. 両者で同じ仕様(図)を見ても記述に大きな違いが出てしまった

→自然言語で書かれた仕様を実装（？）したから細部が違ってしまった

（機能としては要求を満たしている）

→形式記述する事により不備を見つけるだけでなく、曖昧な仕様をより詳細化でき

るのでは無いか

（証明するという目的だけでなく、記述する事に意味がある）

(25)

(26)

両研究会活動にて触れた手法について、特徴や環境整備、予備知識、業務で使用するに

当たっての課題等を調査

・Zの流れを汲む、図による表示

・独自のフォーマットだが、原理はJavaやC++に近い

Alloy

・数学的抽象度が大きい・ISOによる標準化がされている

Z記法

・ツールの種類が豊富、Atelier B、Pro B等

・Event BのRodinプラットフォーム上でPluginとして動くものもある

（ただしRodinのバージョンアップにより非対応となるものもある）

・記述する際の感覚はプログラムに近い

・証明器により、数学的に証明できる課題はある程度自動で証明を完了する。その後、

付加条件を加えたりシステムを変更したりして想定したモデルに矛盾がないことを証明

する

B/EventB

・日本語使用可能、証明課題のみ提示

・数学的知識をあまり必要としない

・モデルの記述がCのクラスに近く、プログラマに取って取っつきやすく、直感的に記述

できる（モデル=クラス）

・作成したクラスのインスタンスを生成し、動的に動作させる事が出来る

VDM/ VDM++

特徴(主観)

手法

(27)

・英語版のみ、コミュニティがある、チュートリアルあり

http://alloy.mit.edu/community/

・現在もバージョンアップが続いている

Alloy

・英語版のみ、コミュニティがある

http://czt.sourceforge.net/

Z記法

・日本語のサイトあり

・個人の方がまとめておられる、初心者には難しい

（バージョン違いによる操作違い、説明の省略）

http://set.style.coocan.jp/wiki/

・公式サイトは英語、チュートリアルあり

http://www.event-b.org/

・現在もバージョンアップが続いている

B/EventB

・日本語のサイトあり、初心者にもわかる

http://www.vdmtools.jp/modules/tinyd1/index.php?id=1

・汎用ライブラリが公開されており、日付/時間/文字などの扱いが容易

VDM/

VDM++

環境整備・教材の取得

手法

(28)

・概念の理解にかかる時間

・習得にかかる時間

・モデル化する範囲

・証明課題は出力されるが証明

器を用意する必要があり、VDM

Tools単体での完全な形式検証は

出来ない

・C++ソースやJavaソースのコンバー

トにはユーザー登録の必要あり

業務で使用するに当たっての課題・

問題

・状態遷移をGUIで表示するので、状態の洗い出し

に適している

Alloy

・数学的基盤があれば、少ない記述で複雑な状態

を示す事が出来る

Z記法

・VDMと同様にプログラマにとっては学習しやすい、

またある程度の自動証明も行うので自動証明出

来なかったもののうち自明で無いものについての

み重点的に仕様レビュー出来る

B/EventB

・文法に慣れ、自然言語の記述をVDMに迅速に落

とし込む事が出来れば動的チェックも出来、仕様

の漏れをコーディング前に発見する事が出来る

・プログラマにとってはハードルが低く、形式手法の

学習としては適している

VDM/

VDM++

有益かどうか

手法

(29)

•導入試用例：自社ソフトウェアの仕様検証（VDM++ & Event-B）

XXXデモシステムソフトウェア仕様（一部略）

◆自動車のインパネを模したインターフェースとする

◆インターフェースはPowerSW、シフトレバー、アクセルペダル、

ブレーキペダルの４つ

◆各インターフェースの説明

・PowerSW

On/Off二つの状態を持つ

・シフトレバー

P, R, N, Dの4つ

・アクセルペダル

On/Off二つの状態を持つ

・ブレーキペダル

On/Off二つの状態を持つ

(30)

•導入試用例：自社ソフトウェアの仕様検証（VDM++ & Event-B）

記述にあたって

・使用した手法：VDM++、Event-B

・使用したツール VDM : VDM++ Toolbox Lite ver.8.3

Event-B ： RODIN platform Ver.2.0.1

（アドオンとしてAtelier B Proversを使用）

それぞれのツールを別の人間が担当して仕様記述した

(31)

•導入試用例：自社ソフトウェアの仕様検証（VDM++ & Event-B）

VDM++, Event-Bによる記述

(32)

•導入試用例：自社ソフトウェアの仕様検証（VDM++ & Event-B）

記述・検証結果比較

・記述がグラフィカルなインターフェースにて行えるので容易である・自動証明器付きなので不具合（反例）を発見しやすい・エディタは別途必要・自然言語の仕様を記述する上で日本語での記述が出来るのは大きなメリットツールを使用しての所感・暗黙知と思われる条件を追加する事により、「PowerをOffにする際には自動的にアクセルペダル、ブレーキペダル共にOffとする」という追加仕様を発見するに至った・自然言語による仕様で暗黙知として記載していないという仕様の曖昧さは見つけられた得られた知見・「PowerをOffにする際アクセルペダルはOffである」という不変条件を追加した際にに反例を発見・重複している記述がある事が判明（「シフトレバーがDまたはRの時、速度が増加する」と「シフトレバーをNにするとアクセルペダルの状態如何にかかわらず速度の増加はしない」）・検証により速度の不変条件を満たさない可能性（「速度タイマ制御」で速度上下限チェックを入れていない為）・「シフトレバーをNにするとアクセルペダルの状態如何にかかわらず速度の増加はしない」の記述必要性が無く、重複した仕様を発見不具合の発見等所要時間・8時間程度・10時間前後 Event-B VDM++

(33)

•導入試用例：自社ソフトウェアの仕様検証（VDM++ & Event-B）

考察：

小さなシステムに対し試験的導入を試みた結果、実際に記述・検証に至るまで時間

を要したものの、仕様の重複や、不備を発見するに至った。ただし今回に関しては実

装を行って動的試験を行った方がかかるコストは少ないという結果になった。

↓

大きなシステムにおいても重要な部分を局所的に形式検証を行えれば良いという考

えの元、だからこそより安全を必要とするならばコストをかけてでも動的試験以前の

形式手法による追加検証を実施していけば良いのではないか。

↓

結果として動的試験のコストが削減できる（手戻りが減少する）はず？

他に影響がある同じ規模のシステム

今回の対象

(34)

•導入試用例：自社ソフトウェアの仕様検証（VDM++ & Event-B）

実践によって得られた知見

形式手法を習得する上で必要と思われた数学的見知やモデル検査等の詳細な知識

が豊富にあるわけではなく、全ての振る舞いを完全に形式検証出来たわけではない

が、記述する（してみる）段階でも何らかの得られるものはあった。

↓

プログラマやエンジニアが片手間で行う様なものではなく、専門部隊を創設しプロフェ

ッショナルを育てていくべきと思っていたが、形式記述の基礎的な文法やツールの使

用方法を習得するだけでも狭い範囲の検証（問題の検知）は可能。

(35)

6.

6. 6. まとめ

まとめ

•機能安全活動や名産研活動に参加する事によって形式手法というも

のを知り、研究者の知識やアドバイスを得た上で企業側としての知識

経験を生かした例題を提示する事が出来た

•研究会を通じて多岐にわたる手法に触れ、各手法の得手不得手を調

査し企業での導入の糸口をつかむことが出来た

•習得する為には、状態遷移やモデル検査に関する知識等形式記述に

おける基礎的な知識が必要だが、基礎的な知識のみでも記述による

仕様不備の検知が出来る事がわかった

•巨大なシステムの全てを検証する必要はなく、より安全が求められる

局所的な部分についてはコストをかけてでも形式検証を行う価値はあ

る（結果として総コストが下がる可能性はある）

(36)

謝辞

本発表をするにあたり、機能安全活動ならびに名産研活動にご参加、

ご指導を頂いたアドバイザ、大学、法人、企業の皆様に感謝いたしま

す。

中小企業の形式手法への取り組み 中小企業の形式手法への取り組み 株式会社サニー技研ソフトウェア基盤技術課 米田真之 中本加那