ＮＴＴﾃﾞｰﾀ／ｴﾝﾀﾌﾟﾗｲｽﾞ市場向けで初めて形式手法活用ｶﾞｲﾄﾞを公開｜物流ﾆｭｰｽ

ﾆｭｰｽ　

用語　

ｾﾐﾅｰ

■ＮＴＴﾃﾞｰﾀ／ｴﾝﾀﾌﾟﾗｲｽﾞ市場向けで初めて形式手法活用ｶﾞｲﾄﾞを公開

ﾃﾞｨﾍﾟﾝﾀﾞﾌﾞﾙ･ｿﾌﾄｳｪｱ･ﾌｫｰﾗﾑが成果第一弾を公開～ｴﾝﾀﾌﾟﾗｲｽﾞ系で初めて形式手法活用ｶﾞｲﾄﾞを公開～　株式会社ＮＴＴﾃﾞｰﾀ､富士通株式会社､日本電気株式会社､株式会社日立製作所､株式会社東芝の５社と､大学共同利用機関法人　情報･ｼｽﾃﾑ研究機構　国立情報学研究所（※１）が参加するﾃﾞｨﾍﾟﾝﾀﾞﾌﾞﾙ･ｿﾌﾄｳｪｱ･ﾌｫｰﾗﾑ（Ｄｅｐｅｎｄａｂｌｅ　Ｓｏｆｔｗａｒｅ　Ｆｏｒｕｍ､略称名はＤＳＦ）は､活動成果の第一弾として､ｴﾝﾀﾌﾟﾗｲｽﾞ（※２）市場向けのｿﾌﾄｳｪｱを対象とした初めての形式手法活用ｶﾞｲﾄﾞを､本日よりＤＳＦ公式ﾎｰﾑﾍﾟｰｼﾞに公開します｡本ｶﾞｲﾄﾞは､ｴﾝﾀﾌﾟﾗｲｽﾞ系ｿﾌﾄｳｪｱを開発するﾌﾟﾛｼﾞｪｸﾄﾒﾝﾊﾞが実際の開発場面に形式手法（※３）を導入するときの参考になると期待します｡　ＤＳＦ公式Ｗｅｂｻｲﾄ　http://www.nttdata.co.jp/dsf/　現在､社会ｼｽﾃﾑはより高信頼･高品質が求められています｡また､自動車や家電等のﾊｰﾄﾞｳｪｱに組み込まれる組込み系ｿﾌﾄｳｪｱを中心に､形式手法を適用した開発を推奨する動きがあり､形式手法に注目が集まっています｡そこで､２００９年１２月にＤＳＦを設立し､具体的に活動するﾜｰｷﾝｸﾞｸﾞﾙｰﾌﾟである形式手法適用評価ＷＧ（Ｆｏｒｍａｌ　Ｍｅｔｈｏｄｓ　Ａｐｐｌｉｃａｔｉｏｎ　ＷＧ､略称名はＦＭＡＷＧ）の中で､形式手法適用事例､及びﾉｳﾊｳを蓄積してきました｡　形式手法活用ｶﾞｲﾄﾞは､ﾃﾞｨﾍﾟﾝﾀﾞﾌﾞﾙ･ｿﾌﾄｳｪｱ（※４）実現の有力な手段である形式手法を実際の開発現場で有効に活用するために､各参加企業が連携して作成しています｡　形式手法はｴﾝﾀﾌﾟﾗｲｽﾞ系ｿﾌﾄｳｪｱの開発に適用する場合のｺｽﾄが膨らむという固定観念と活用できる技術者の不足のため､適用事例が少なく､その効果も一般に公開されていません｡そこで､ＤＳＦは適用効果を確かめるべく記述実験を行い､形式手法がｴﾝﾀﾌﾟﾗｲｽﾞ系ｿﾌﾄｳｪｱ開発上流工程での誤り発見に効果があることを確認しました｡具体的には､ﾚﾋﾞｭｰによって誤りが除去されたと考えられる設計書を形式手法で記述し直すことにより､複数の設計書で書かれている内容の矛盾や仕様の解釈が複数あるという誤りを新たにいくつか発見することができました｡　また､同時に上記実験の結果､形式手法の実務への適用には以下４点の課題が重要であることが分かりました｡　課題１．現場利用を踏まえた適用手順や体制　課題２．形式手法を用いる際の定石や作法の知識　課題３．形式手法に関するｽｷﾙや教育方法　課題４．より現実的な開発場面での効果や利点･欠点　ＤＳＦは上記のうち､課題１～３について対策を検討しました｡･課題１に対して､ｴﾝﾀﾌﾟﾗｲｽﾞ系ｿﾌﾄｳｪｱ開発の上流工程における､要件定義工程の次段階である設計工程に対して､形式手法の適用手順をまとめました｡･課題２に対して､ｴﾝﾀﾌﾟﾗｲｽﾞ系ｿﾌﾄｳｪｱ開発で想定される一般的な設計書の形式記述作成方法に対して､典型的な解決例一覧と､一部､具体例を含む詳細な書き方の解決例を記述しました｡･課題３に対して､ｽｷﾙ教育で必要なｽｷﾙﾏｯﾌﾟやｾﾐﾅﾌﾟﾛｸﾞﾗﾑを設定し､ＤＳＦﾒﾝﾊﾞを対象としたｾﾐﾅを実施して評価しました｡(略)【今後の活動について】　今後､ＤＳＦは､｢課題４．より現実的な開発場面での効果や利点･欠点｣の対策として､より開発現場に近い場面を想定して形式手法適用の有効性を評価する実証実験を企画します｡また､今回公開した成果を実証実験で利用するために､ｲﾃﾞｨｵﾑ集の充実､及び形式手法適用手順のさらなる具体化等の改善を図ります｡そして､実証実験を通して成果の妥当性や形式手法効果の実証を図り､２０１１年度末に実証実験結果を反映させた最終成果を提供する予定です｡【｢形式手法適用評価ＷＧ（ＦＭＡＷＧ）｣について】　ＦＭＡＷＧは､ﾃﾞｨﾍﾟﾝﾀﾞﾌﾞﾙ･ｿﾌﾄｳｪｱ実現の有力な手段である形式手法に着目し､具体的な検討活動を行うﾜｰｷﾝｸﾞｸﾞﾙｰﾌﾟです｡ＦＭＡＷＧは､実際の開発現場で有効に活用できる形式手法の適用事例や適用ﾉｳﾊｳを蓄積･公開し､形式手法を適用したｼｽﾃﾑ開発の可能性を追求するＷＧです｡【注釈】（※１）株式会社ＮＴＴﾃﾞｰﾀ､富士通株式会社､日本電気株式会社､株式会社日立製作所､株式会社東芝の５社と､大学共同利用機関法人　情報･ｼｽﾃﾑ研究機構　国立情報学研究所　株式会社ＮＴＴﾃﾞｰﾀ（代表取締役社長：山下　徹）､富士通株式会社（代表取締役社長：山本　正已）､日本電気株式会社（代表取締役　執行役員社長：遠藤　信博）､株式会社日立製作所（執行役社長：中西　宏明）､株式会社東芝（取締役　代表執行役社長：佐々木　則夫）の５社と､大学共同利用機関法人　情報･ｼｽﾃﾑ研究機構　国立情報学研究所（所長：坂内　正夫）（※２）ｴﾝﾀﾌﾟﾗｲｽﾞ　企業活動を営むための業務ｼｽﾃﾑや社会基盤を支える情報ｼｽﾃﾑのこと｡（※３）形式手法（ﾌｫｰﾏﾙﾒｿｯﾄﾞ，　Ｆｏｒｍａｌ　Ｍｅｔｈｏｄｓ）　数理論理学を基盤として､対象ｼｽﾃﾑ･ｿﾌﾄｳｪｱの機能･振舞いについて正確な記述と系統的な検証を行う手法･技術の総称｡対象を厳密に記述することにより､要求や設計の矛盾､抜け漏れ等の誤りに気付く｡さらにﾂｰﾙを用いて検証することにより､要求や設計の矛盾､抜け漏れ等の誤りを発見することができる｡（※４）ﾃﾞｨﾍﾟﾝﾀﾞﾌﾞﾙ･ｿﾌﾄｳｪｱ（Ｄｅｐｅｎｄａｂｌｅ　Ｓｏｆｔｗａｒｅ）　利用者が信頼･安心して利用できる､頼りになるｿﾌﾄｳｪｱであり､可用性､信頼性､安全性､機密性､完全性､保守性といった複合的要件を満足する｡　●可用性（Ａｖａｉｌａｂｉｌｉｔｙ）：利用者がｼｽﾃﾑを使用し続けることができる性質　●信頼性（Ｒｅｌｉａｂｉｌｉｔｙ）：ｼｽﾃﾑのﾊｰﾄﾞｳｪｱやｿﾌﾄｳｪｱが故障する頻度　●安全性（Ｓａｆｅｔｙ）：ｼｽﾃﾑが人間や環境に危害を及ぼす度合い　●機密性（Ｃｏｎｆｉｄｅｎｔｉａｌｉｔｙ）：ｱｸｾｽを許可された者だけがｼｽﾃﾑで管理する情報にｱｸｾｽできること　●完全性（Ｉｎｔｅｇｒｉｔｙ）：ｼｽﾃﾑで管理する情報を保護して､正確かつ完全である（改ざんされない）こと　●保守性（Ｍａｉｎｔａｉｎａｂｉｌｉｔｙ）：ｼｽﾃﾑが故障したときの修理のしやすさのこと（※５）Ｅｖｅｎｔ－Ｂ　ｼｽﾃﾑの分析､設計を行う形式手法｡集合論と一階述語論理と呼ばれる数学の概念を用いて仕様を表現し検証する｡特に､仕様を段階的に詳細化､具体化する過程で正しさを検証する作業を繰り返し行う｡欧州連合（Ｅｕｒｏｐｅａｎ　Ｕｎｉｏｎ）のﾌﾚｰﾑﾜｰｸﾌﾟﾛｸﾞﾗﾑ（ＦＰ）７支援研究ﾌﾟﾛｼﾞｪｸﾄＤＥＰＬＯＹが統合仕様開発ﾂｰﾙＲＯＤＩＮを開発し無償公開している｡（※６）ｲﾃﾞｨｵﾑ　ｿﾌﾄｳｪｱにおける形式記述の典型的な表現｡（※７）ＳＰＩＮ　ﾓﾃﾞﾙ検査法と呼ぶ自動検証の方法を提供するﾂｰﾙ｡Ｇ．Ｊ．　Ｈｏｌｚｍａｎｎ博士が開発､無償公開しており､国内の産業界ならびに大学等の教育機関でも関心が高い｡分散ｼｽﾃﾑなどの並行ｼｽﾃﾑの表現を記述すること､ならびに自動検証に向いている｡調べることができる性質としては｢ﾃﾞｯﾄﾞﾛｯｸが発生しない｣といった基本的なものに加えて､線形時相論理と呼ばれる形式で表現した処理進行に関わる性質がある｡