これまでの活動内容報告書・成果物実績報告書:実務家のための形式手法 教材「厳密な仕様記述を志すための形式手法入門」の公開

本文を印刷する

報告書:実務家のための形式手法 教材「厳密な仕様記述を志すための形式手法入門」の公開

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

概要

  日常生活で使用する様々なサービスや製品には、ソフトウェアが密接に関係しています。サービスや製品の規模や利用形態の複雑さが増すにつれ、ソフトウェアの品質に問題が生じた場合の原因究明には時間がかかり、サービスや製品を利用する国民に及ぼす経済的損失や社会的影響などの発生リスクは増えていきます。
  こうしたリスク抑制のためには、ソフトウェアの品質向上を図る必要があり、様々な取組みが行われてきました。その中でも「形式手法」(*1)は、数学的なアプローチを用いて厳密な仕様を記述し検証することができるため、曖昧さや抜けを防ぎ、実装の間違いを見つけ出す、といった利点があります。また、高い安全性を要求される製品に関連する国際規格であるIEC 61508(*2)や自動車分野の機能安全に関する国際規格であるISO 26262(*3)でも、形式手法の適用が推奨されています。
  IPA/SECでは、形式手法の普及促進、形式手法導入に関わる人材育成を目的に、2010年4月に「形式手法人材育成WG」(現「人材育成WG」) を発足し、活動を行ってきました。今回、本WGの活動成果である、「実務家のための形式手法:厳密な仕様記述を志すための形式手法入門」教材を公開します。
  本教材は、ソフトウェア開発現場における「形式手法は難しい」という先入観を払拭するとともに、特に上流工程でソフトウェア開発従事者が苦労している部分への形式手法適用の効果を理解できるように開発されており、形式手法の現場導入で得られた種々の実践的知見も反映した教材となっています。
  また、”開発対象を厳密かつコンパクトに記述し、その成果物である仕様書を実装に結びつけ、検証する”といった、開発ライフサイクルを通して実際に形式手法を適応するという導入の観点からの留意点や、組織内で開発経験を共有し活用するため、形式手法導入をプロセスとして文書化し、運用する点についても説明しています。


2013年1月25日に「厳密な仕様記述における形式手法成功事例調査報告書」を公開しました。

脚注

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

ダウンロード

  以下の資料をダウンロードいただけます。

「実務家のための形式手法:厳密な仕様記述を志すための形式手法入門」
  • シラバス
  • なぜ形式手法か
  • 形式手法導入に関わるガイダンス
  • 事例:成功事例
  • 事例:種々の事例
  • 事例:実証実験
  • 実践法:モデル化の手順と事例
  • 実践法:モデル化の課題例
  • 参考資料
注:当ページのコンテンツは下記3つの形式を、それぞれZIPファイル圧縮形式での提供となっております。
スライド(PDF形式)一括ダウンロード[3.52MB]
スライドショー(PPSX形式)一括ダウンロード[3.19MB]
ノート付きスライド(PDF形式)一括ダウンロード[22.5MB]
「シラバス」にはスライドショー、ノート付きスライドはありません。

更新履歴

2012年12月27日 「なぜ形式手法か」、「実践法:モデル化の手順と事例」一部変更

報告書・成果物実績