LOTOS — ISO 8807:1989
並行・分散システムの振る舞いを記述する形式仕様技術です。ISO の規格情報では、2019年に確認され、現行版として掲載されています。
ISO 8807:1989（ISO）Formal Description Techniques
日本の形式仕様記述・形式手法リソース
仕様を数学的な記法で明確に表し、モデルの性質を分析・検証するための規格、学習資料、研究情報をまとめています。
形式仕様記述技術（FDT）とは
Formal Description Technique（FDT）は、システムの振る舞いや構造を、定義された構文と意味に基づいて記述する技術です。曖昧さや仕様間の不整合を見つけやすくし、記述したモデルに対する解析や検証を可能にします。形式化した仕様は対象システム全体の正しさを自動的に保証するものではなく、何をモデル化し、どの性質を確認したかを明示することが大切です。
FDT は形式手法の一部を指す用語として使われます。形式手法には仕様記述のほか、モデル検査や定理証明などの検証技術も含まれます。
Standards
LOTOS と E-LOTOS
E-LOTOS — ISO/IEC 15437:2001
LOTOS を拡張した言語で、分散・並行システムの振る舞いを記述します。ISO の規格情報では、2008年に確認され、現行版として掲載されています。
規格の「現行」は、規格が最新技術であることや、現在広く利用されていることを意味するものではありません。規格状態は変更されることがあるため、ISO の公式情報もご確認ください。
Learn & Practice
日本語の学習・実務資料
実務家のための形式手法
2013年に終了した IPA/SEC 事業のアーカイブです。入門教材、モデル化の手順と事例、形式手法の適用事例調査を参照できます。
IPA の教材・資料一覧VDM++ による形式仕様記述
VDM++ の考え方、記述方法、例題を日本語で紹介する資料です。一部の文法資料・例題は2011年更新のため、ツールの対応状況は各公式サイトでもご確認ください。
国立情報学研究所・VDM++ 資料形式仕様記述の適用事例
IPA の事例報告では、対象とする仕様を選び、実開発システムの設計書に形式手法を適用して早期に問題を発見した取り組みが紹介されています。
情報系の実稼働システムを対象とした適用実験（IPA）試験シラバスの用語解説
IPA の情報処理技術者試験シラバスには、形式手法や VDM-SL、VDM++、Z、SPIN などの用語が掲載されています。
情報処理安全確保支援士試験シラバス追補版（IPA PDF）Research in Japan
国内の研究動向
以下は学会が公開している講演概要・研究紹介です。VDM++による仕様の分析やテスト支援、形式仕様記述の新しい応用を知る手がかりになります。
VDM++ による組織の整合性・制約条件の記述と検証
信州大学による研究発表です。勤務シフト表を題材に、組織の制約をVDM++で記述して検査する方法を扱っています。
FIT2023 講演概要（A-020）画面遷移図から VDM++ 仕様への変換
香川大学による研究発表です。Webアプリケーションの画面遷移図をVDM++仕様に変換し、精密なテストケースの作成などに活用する手法を議論しています。
FIT2023 講演概要（B-011）LLM を用いた形式仕様記述による検証
ソフトウェアエンジニアリングシンポジウムの受賞研究として、LLMを用いた形式仕様記述による検証の試行評価が紹介されています。
SES インタラクティブ賞の受賞研究一覧軽量形式手法・解析技術
日本ソフトウェア科学会の研究紹介では、物理情報システムやAIシステムを対象とした軽量形式手法・解析技術など、関連する研究領域を紹介しています。
日本ソフトウェア科学会・研究紹介このサイトの関連ページ
外部資料の内容・公開状況は各提供元でご確認ください。リンク確認日：2026年10月21日。