これまでの活動内容報告書・成果物実績実務家のための形式手法シリーズ、教材及び副読本の公開

本文を印刷する

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

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

概要

  日常生活で使用する様々なサービスや製品にはソフトウェアが密接に関係しています。サービスや製品の規模や利用形態の複雑さが増すにつれ、ソフトウェアの品質に問題が生じた場合の原因究明には時間がかかり、サービスや製品を利用する国民に及ぼす経済的損失や社会的影響などの発生リスクは増えていきます。このようなリスクを抑制するためには、ソフトウェアの品質向上を図る必要があり、様々な取組みがされてきました。その中でもとりわけ形式手法(*1)は、数学的に厳密な仕様を記述し検証することができるため、曖昧さや抜けを防ぐ、実装の間違いを見つけ出す、といった利点があり、高い安全性を要求される製品に関連する国際規格である、IEC 61508(*2) 及び自動車業界に対するISO 26262(*3)でも、形式手法の適用が推奨されています。

  これに対してIPAでは、2010年4月に「人材育成WG」を2012年4月に「厳密な仕様記述WG」を発足させ、今回、以下の3点を公開できる運びとなりました。

実務家のための形式手法シリーズの公開

  • 「厳密な仕様記述を志すための形式手法入門 第二版」
  • 「対象を如何にモデル化するか?」
  • 「厳密な仕様記述入門」

「厳密な仕様記述を志すための形式手法入門 第二版」
  とかく形式手法は難しいという開発現場の認識を変えるべく、現場のソフトウェア開発従事者が特に上流工程で苦労している部分への効果を理解できるように、形式手法の現場導入で得られた実践的な知見を反映した初版を昨年11月に公開し、その後開催したセミナーからのフィードバックを反映したものです。
 
「対象を如何にモデル化するか?」
  教材の「実践法:モデル化の手順と事例」、「実践法:モデル化の課題例」では形式手法を活用する具体的手順と課題を説明しており、その部分の副読本としての位置づけになります。教材と副読本を効果的に活用していただけるように、シラバスの強化も行いました。
 
「厳密な仕様記述入門」
  開発ライフサイクルの上流における仕様書についての厳密な定義及び記述に対する入門書として位置づけています。この入門書は、形式手法をベースとして記述していますが、日本語による仕様書記述においても役立つ内容となっています。

「品質の高いソフトウェアの効率的な開発」の一助として、これら三つの成果を統合的に活用していただけることを期待します。


脚注

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

使用条件

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

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


ダウンロード

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

「実務家のための形式手法:厳密な仕様記述を志すための形式手法入門 第二版」
【構成】
  • シラバス
  • なぜ形式手法か
  • 形式手法導入に関わるガイダンス
  • 事例:成功事例
  • 事例:種々の事例
  • 事例:実証実験
  • 実践法:モデル化の手順と事例
  • 実践法:モデル化の課題例
  • 参考資料
下記3つの形式を、それぞれZIPファイル圧縮形式での提供となっております。
スライド(PDF形式)一括ダウンロード[5.39MB]
スライドショー(PPSX形式)一括ダウンロード[5.06MB]
ノート付きスライド(PDF形式)一括ダウンロード[27.1MB]
「シラバス」にはスライドショー、ノート付きスライドはありません。
  
「対象を如何にモデル化するか?」形式記述サンプル付(zip形式)[1.57MB]
「厳密な仕様記述入門」 [4.73MB]PDF文書

更新履歴

2013年4月1日 「厳密な仕様記述入門」P110~P111図3-4を更新しました。

報告書・成果物実績