実務家のための形式手法 | アーカイブ | IPA 独立行政法人 情報処理推進機構本ページの情報は、2013年3月時点のものです。本事業は終了しているため、お問い合わせには対応できません。 サービスや製品の規模や利用形態の複雑さが増すにつれ、ソフトウェアの品質に問題が生じた場合の原因究明には時間がかかり、サービスや製品を利用する国民に及ぼす経済的損失や社会的影響などの発生リスクは増えていきます。 このようなリスクを抑制するためには、ソフトウェアの品質向上を図る必要があり、様々な取組みがされてきました。その中でもとりわけ形式手法(脚注1)は、数学的に厳密な仕様を記述し検証することができるため、曖昧さや抜けを防ぐ、実装の間違いを見つけ出す、といった利点があり、高い安全性を要求される製品に関連する国際規格である、IEC 61508(脚注2) 及び自動車業界に対するISO 26262(脚注3)でも、形式手法の適用が推奨されています。 厳密な仕様記述を志すための形式手法入門 第二
