実務家のための形式手法　

本ページの情報は、2013年3月時点のものです。本事業は終了しているため、お問い合わせには対応できません。

サービスや製品の規模や利用形態の複雑さが増すにつれ、ソフトウェアの品質に問題が生じた場合の原因究明には時間がかかり、サービスや製品を利用する国民に及ぼす経済的損失や社会的影響などの発生リスクは増えていきます。

　このようなリスクを抑制するためには、ソフトウェアの品質向上を図る必要があり、様々な取組みがされてきました。その中でもとりわけ形式手法(脚注1)は、数学的に厳密な仕様を記述し検証することができるため、曖昧さや抜けを防ぐ、実装の間違いを見つけ出す、といった利点があり、高い安全性を要求される製品に関連する国際規格である、IEC 61508(脚注2) 及び自動車業界に対するISO 26262(脚注3)でも、形式手法の適用が推奨されています。

注釈

1. (脚注1)
   形式手法:数学的な規範を用いることで、曖昧性や不正確さを排除する手法。形式的仕様記述と形式検証に大別される。形式的仕様記述は、数学的な規範で仕様を記述して、仕様の曖昧性を排除する手法。
2. (脚注2)
   IEC 61508：IECが策定した一般的な機械を対象とした機能安全に関する国際規格。IEC（国際電子標準会議）は電気・電子技術分野の国際規格の策定を行っている組織
3. (脚注3)
   ISO 26262：ISOが策定した自動車分野の機能安全に関する国際規格。ISO（国際標準化機構）は電気・電子技術分野を除く国際規格の策定を行っている組織

使用条件

1. 本資料の著作権は、独立行政法人　情報処理推進機構が保有しています。
2. 本資料は著作権法による保護を受けており、本資料の使用者は、本資料の全部または一部を項番3に定める場合を除き、独立行政法人　情報処理推進機構の許諾なく無断で複製、改変、公衆送信、販売、出版、翻訳/翻案等の著作権法上の利用行為は営利目的、非営利目的に関わらず禁じられています。
3. 独立行政法人　情報処理推進機構は、本資料の使用者が、以下の著作権表示を明記することを条件として、(1)及び(2)の行為を行うことを許諾します。
   著作権表示：Copyright©2013 独立行政法人 情報処理推進機構
   (1)本資料の全部または一部を複製すること。
   (2)本使用条件に記載されている使用条件を配布先に遵守させることを条件に本資料の複製物を無償で再配布すること。
   
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. 本資料へのお問い合わせについては、独立行政法人　情報処理推進機構までご連絡下さい。

実務家のための形式手法シリーズ、教材及び副読本

• 厳密な仕様記述を志すための形式手法入門 第二版スライド(ZIP:5.4 MB)
• 厳密な仕様記述を志すための形式手法入門 第二版スライドショー(ZIP:5.1 MB)
• 厳密な仕様記述を志すための形式手法入門 第二版ノート付きスライド(ZIP:27.2 MB)
• 「対象を如何にモデル化するか？」形式記述サンプル付(zip形式)(ZIP:1.6 MB)
• 「厳密な仕様記述入門」(PDF:4.8 MB)

関連情報