これまでの活動内容報告書・成果物実績報告書:形式手法導入課題を解決する「形式手法活用ガイドならびに参考資料」の公開

本文を印刷する

報告書:形式手法導入課題を解決する「形式手法活用ガイドならびに参考資料」の公開

~エンタプライズ系ソフトウェア開発で利用できるノウハウ~

2012年9月28日公開
独立行政法人情報処理推進機構
技術本部 ソフトウェア・エンジニアリング・センター

概要

  IPA/SECでは、ソフトウェア開発の高信頼化に向けた有効な手法と一つとして形式手法の普及活動に取り組んできました。今回、代表的な形式手法である Event-B, SPIN, VDM++ を用いて、基本設計書の品質向上のための検証方法をガイドする「形式手法活用ガイドならびに参考資料」を公開します。
  本資料は、「Dependable Software Forum(略称:DSF)(※)」から譲渡されたもので、2012年4月20日に公開した「情報系の実稼働システムを対象とした形式手法適用実験報告書」でも活用されています。実験報告書と共に参照し、実践的な取組みに活用いただけることを期待します。


※Dependable Software Forum(略称:DSF)
株式会社NTTデータ、富士通株式会社、日本電気株式会社、株式会社日立製作所、株式会社東芝、SCSK株式会社、大学共同利用機関法人 情報・システム研究機構 国立情報学研究所の6社1機関から構成されていました。「形式手法活用ガイド【改訂版】」の完成を受けて2012年6月30日をもって活動を終了いたしました。


使用条件

次の使用条件の下でご利用ください。

  1. 本資料の著作権は、独立行政法人 情報処理推進機構が保有しています。
  2. 本資料は著作権法による保護を受けており、本資料の使用者は、本資料の全部または一部を項番3に定める場合を除き、独立行政法人 情報処理推進機構の許諾なく無断で複製、改変、公衆送信、販売、出版、翻訳/翻案等の著作権法上の利用行為は営利目的、非営利目的に関わらず禁じられています。
  3. 独立行政法人 情報処理推進機構は、本資料の使用者が、以下の著作権表示を明記することを条件として、①及び②の行為を行うことを許諾します。
    著作権表示:Copyright©2012 独立行政法人 情報処理推進機構
    ①本資料の全部または一部を複製すること。
    ②本使用条件に記載されている使用条件を配布先に遵守させることを条件に本資料の複製物を無償で再配布すること。
  4. 独立行政法人 情報処理推進機構は、本資料が第三者の著作権、特許権、実用新案権等の知的財産権を侵害しないことを一切保証するものではなく、また、本資料の内容に誤りがあった場合でも一切責任を負いかねます。
  5. 独立行政法人 情報処理推進機構は、本使用条件に記載された許諾内容を除き、独立行政法人 情報処理推進機構または第三者の著作権、特許権、実用新案権等の知的財産権に基づくいかなる権利を許諾するものではありません。
  6. 独立行政法人 情報処理推進機構は、本資料のシステム開発への利用、開発されたシステムの使用、及び当該システムの使用不能等により生じるいかなる損害についても、なんら責任を負うものではありません。
  7. 本資料を海外へ持ち出す場合及び非居住者に提供する場合には、「外国為替及び外国貿易法」の規制及び米国輸出管理規則等外国の輸出関連法規を確認のうえ、必要な手続きを行って下さい。
  8. 【形式記述サンプル】には、オープンソースのVDMUnitが含まれております。
    VDMUnitの著作権と使用条件は下記となります。
    VDMUnit - an open-source framework for formal specification of test suites in VDM++. Copyright (C) 2005 Marcel Verhoef
    This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.
    This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/.
  9. 本資料へのお問い合わせについては、独立行政法人 情報処理推進機構 ソフトウェア・エンジニアリング・センターまでご連絡下さい。



ダウンロード

注:上記の使用条件に合意願います。

※2012年4月20日DSF発行の「形式手法活用ガイド【改訂版】」に対し著作権の表示及び利用条件を変更したものになります。

以下の資料をダウンロードいただけます。
  • 形式手法活用ガイド導入の手引き
  • 形式手法適用手順(VDM++編)
  • 形式手法適用手順(SPIN編)
  • 形式手法適用手順(Event-B編)
  • 形式手法イディオム集(VDM++編)
  • 形式手法イディオム集(SPIN編)
  • 形式手法イディオム集(Event-B編)
  • 図書館システム記述実験報告書
  • 形式手法スキルアップセミナ報告書(Event-B編)
一括ダウンロード[12MB]ZIP形式
 
【形式記述サンプル】
※本サンプルには一部GPLのファイル(VDMUnit.vpp)があります。上記使用条件項番8をご参照ください。
形式記述サンプル[1.61MB]ZIP形式


参考資料ダウンロード

注:上記の使用条件に合意願います。

本文書は、2012年4月20日にIPA/SECから公開した「情報系の実稼働システムを対象とした形式手法適用実験報告書(別冊 詳細報告書)」にて参照をしているため、参考資料として公開します。
※2011年7月21日DSF発行の「形式手法活用ガイド【リリース版】」に対し著作権の表示及び利用条件を変更したものになります。

以下の資料をダウンロードいただけます。
  • 形式手法活用ガイドの紹介【リリース版】
  • 形式手法適用手順(VDM++編)【リリース版】
  • 形式手法適用手順(SPIN編)【リリース版】
  • 形式手法適用手順(Event-B編)【リリース版】
  • 形式手法イディオム集(VDM++編)【リリース版】
  • 形式手法イディオム集(SPIN編)【リリース版】
  • 形式手法イディオム集(Event-B編)【リリース版】
リリース版一括ダウンロード[9.45MB]ZIP形式

報告書・成果物実績