（注）“SLP”とは“SPEC L-PERFECT”の略称です。

SLPは『主語述語論理モデル』に基づく、文章を対象にした『論理分析』手法です。
文の構造を明らかにするもっとも基礎的な方法です。
SLPはこの基礎的方法で得た成果を基に、他の重要な方法へのアプローチを試みます。

■SLPの状態遷移表への応用

こんな質問をいただきました。


「要求仕様書から状態遷移表を直接手作業で作成しているため、
人為的ミスが発生している」


この原因はなんでしょうか。


要求仕様書に基づいて設計していない？
そもそも要求仕様書がよくない？
そもそも設計者・実装者のスキルが足りない？

でもそれを言ってはおしまい。

少しアプローチしてみましょう。

、、、

こうすればいいのでは。


SLPの状態遷移表へのExport (ZIPファイル/1009KB)

■SLPでEvent-Bの「精義化」を実現する

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

以下の文が長いので実例を先に示します。


またこんな質問をいただきました。


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


Event-Bは要求仕様書の内容を数理論的に証明します。
そこで当社はSLPにEvent-Bの内容無矛盾性のための推論機能と、
その検査機能を追加することを決めました。

しかしその前に、この目標を是とする事例をお見せします。

それは、ある仕様書がEvent-Bでの精義化を経て、
より精細化した事例をお見せします。
もちろん、証明された仕様書です。


ABSのEventBによるモデル化 (ZIPファイル/587KB)


この“証明可能なSLP“のリリースには今後1年を計画しています。