形式仕様に基づくソフトウェア開発手法の紹介: Bメソッドを中心に

摘要

社会におけるソフトウェアの重要性が高まり，開発における効率および信頼性がより強く求められている中，形式仕様に対する注目が産業界でも高まってきている．形式仕様においては，「作りたいシステム」を厳密な文法?意味論の定まった言語で記述することにより，曖昧さや不完全さが排除されるとともに，特にツールによる科学的?系統的な分析?検証が可能となる．本稿においては，形式仕様の基本的な考え方を解説する．この解説においては特に，抽象的な仕様モデルから「正しいことがわかっているプログラム」を導出する手法であるBメソッドの記述例を示す．本稿ではさらに，他の手法や適用事例，研究事例，最近の動向についても俯瞰する．%Formal specifications have been attracting more and more attentions, as software plays the key roles in the society and its development is strongly required to be efficient and reliable. Formal specifications eliminate unambiguity and incompleteness through description based on languages with rigorous syntax and semantics, as well as scientific, systematic analysis and verification. This paper provides introduction to fundamental approaches in formal specifications. This paper specifically presents an example description with B-Method, a method to derive "programs proved to be correct" from abstract specification models. This paper also provides overview of other methods, application cases, research studies and recent trends.