(「精義化」は refinement の当社の訳語です。)

こんな質問をいただきました。「要求仕様を形式的な正しさを保証する方法（SLP）から、内容的な正しさへと保証する方法はないでしょうか。というのも、数学関数でモデルを構成するツールを使っていますが、仕様が間違っている場合にはモデルが正しいという保証はありませんから。」

Event-Bは要求仕様書の内容を数理論的に証明します。そこで当社はSLPにEvent-Bの内容無矛盾性のための推論機能と、その検査機能を追加することを検討しております。最近は大規模システムの証明にもEvent-Bが用いられたなどの事例も出始めています（”Using Event-B for Critical Device Software Systems”）。「証明可能なSLP」は研究途上ですが、途上の事例をお見せします。ある仕様書がEvent-Bでの精義化を経て、より精細化した事例です。もちろん、証明された仕様書です。

• ABSのEventBによるモデル化 [ZIP 0.6 MB]

日本語訳　ファイル一覧

お断り

原著 Modeling in Event-B: System and Software Engineering は著作権で保護されており、日本語訳はAbrial博士とCambridge University Pressの許可により掲載されています。この日本語訳を有償で販売してはいけません。原著についての情報 もご覧ください。この日本語訳は 原著の正誤表 を反映しています。

The original book Modeling in Event-B: System and Software Engineering is in copyright, that the translation appears with permission of the Author of Cambridge University Press. This translation should not be sold or resold. See also the webpage for more information about the original book. This translation corresponds with the errata sheet for the original book.

Event-Bについての情報

• Event-B.org
• 原著の第1章 (PDF)
• 原著の第2章 (PDF)
• Cambridge University Press
• 形式手法 Event-B