Event-Bモデルの開発
Event-Bモデルは離散遷移システムです。CONTEXTは固定された集合、定数、公理を保持し、MACHINEは変数、不変条件、ガード付きイベントを保持します。このスキルはProBを使用して到達可能な振る舞いをチェックし、well-definednessを検証します。対話型のRodin証明はサポートしません。
1. 必要なツールの確認
rossi 0.1.8+ および eventb-animate 6.4+ が必要です。これらを確認してください。自分でインストールやアップグレードは絶対に行わないでください。どちらかが存在しないか、バージョンが古い場合は、処理を中止してユーザーに依頼してください。
command -v rossi eventb-animate
rossi --version
eventb-animate --version
2. モデリング前のスコープ設定
モデルの README.md に簡潔な要件シートを記述してください。
- システム境界と明示的な除外事項
- 観測可能なイベントとその実行主体
- 状態の型と、常に成立すべき安全特性
- 到達可能な成功シナリオ1つ、重要な禁止シナリオ1つ、および終端状態が意図的かどうか
大規模なモデルや複数レベルのリファインメントがある場合は、レベルごとに1行の要件-リファインメント対応表を追加します：要件/標準節、新規または置き換えられた状態、影響を受けるイベント、不変条件/グルーイング関係、および検証質問。あるレベルの行に無関係な懸念が混在している場合は分割してください。
デフォルトでは1つのマシンを使用し、固定データはその独立した懸念に応じてできるだけ多くの小さなコンテキストに分割してください。リファインメントレベルは、それが明確な要件を分離するか、データ表現を置き換える場合にのみ追加し、その理由とグルーイング不変条件を最初に記述してください。リファインメントはツールであり、必須の儀式ではありません。
各モデルを独自のプロジェクトディレクトリに配置してください。コンポーネントごとに1ファイルを使用し、ファイル名はコンポーネント名に合わせてください。.eventb ファイルに散文のコメントを入れないでください。説明は README.md に保持してください。
3. 関連するリファレンスのみを読む
| 目的 | 読むべきもの |
|---|---|
正確な .eventb 文法とアクション形式 | references/syntax.md |
| 演算子またはその優先順位 | references/math-toolkit.md |
| 状態、不変条件、イベントの選択方法 | references/modelling.md |
| 正当なリファインメント手順、またはチェーンの計画 | references/refinement.md |
| コアなリアクティブシステムパターン | references/patterns.md の該当する見出し |
| 離散時間、デッドライン、モード、センサー/アクチュエータ | references/patterns-control.md |
| 複数参加者：トポロジ、ラウンド、合意、チャネル、長時間実行操作 | references/patterns-distributed.md |
| アクセス制御、認可ポリシー、予約 | references/patterns-security.md |
| 事後条件からのループ導出、またはインタプリタ/ISA | references/patterns-algorithms.md |
| CLIトラブルシューティングまたは条件付き高度コマンド | references/tooling.md |
| 最終設計レビュー | references/best-practices.md |
ウィットネスやデータリファインメントが関係する場合にのみ examples/counter/ から始めてください。イベント分割/収束には examples/cars_on_bridge/ を、終了アルゴリズムには examples/array_maximum/ を使用してください。小さな単一マシンモデルを始めるためだけに例を読まないでください。
4. 最小限の有用なモデルを作成する
- キャリアセットと固定ポリシー/設定をコンテキストに配置します。
- すべての変数を最初の不変条件で型付けし、次に実際の安全ルールを記述します。
- センシングまたは制御がシステム境界を越える場合は、物理状態、報告状態、命令状態を区別し、それらの間の許容される遅延/不確実性を明記します。
INITIALISATIONですべての不変条件が成立するようにします。- 各イベントに、機能要件および遷移のみの要件、ならびに不変条件保存に必要なすべてのガードを設定します。アクションは同時に実行され、未割り当ての変数は変更されません。
- 後続の状態目標がそれを観測する必要がある場合は、重要な結果を状態で表現します。専らカバレッジを得るためにノーオペレーションイベントを追加しないでください。有効なノーオペレーションはデッドロックとライブネスの振る舞いを変更します。
- 有限チェックシナリオは小さく保ちます。広い非決定論的パラメータは操作の有効化を増やし、有限チェックを不完全または遅くする可能性があります。
5. コアゲートの実行
モデルのプロジェクトディレクトリから実行します。無関係なモデルを含む親ディレクトリからは実行しないでください。.zip をビルドします。これにはアニメーターが必要とするチェック済みファイルが含まれます。
rossi fmt -i .
rossi validate .
rossi fmt --check .
rossi build . -o /tmp/model.zip
eventb-animate --json /tmp/model-report.json /tmp/model.zip
eventb-animate wd /tmp/model.zip
以下の場合にのみ結果を受け入れます。
- バリデーションとビルドにエラーがないこと。
missing or ill-typed witnessおよびevent is inaccurate警告は、コマンドがゼロで終了しても失敗として扱います。 - レポートのステータスが
"ok"であり、不変条件違反がないこと。 - 予期しないデッドロックがないこと。意図的な終端状態の場合は、終端述語を文書化し、デッドロックフリーを主張する代わりに
--no-deadlockを付けて再実行します。 - 人間が確認する
Covered operationsブロックに期待されるイベントが含まれていること（レポートv3は操作カバレッジを保存しないため、監査が必要な場合はコマンド出力をキャプチャします）。 - 有限受理シナリオの場合、
completion.classificationがcompleteであること。 - すべてのwell-definedness義務が解決されていること。
終了コード0は完全性の証明ではありません。有限モデルが不完全と報告された場合は、理由と関連するProBの上限を調べてください。
eventb-animate info --prefs /tmp/model.zip \
| rg 'MAX_(INITIALISATIONS|OPERATIONS)|DEFAULT_SETSIZE'
既知の有限選択肢を列挙するのに十分なだけ MAX_INITIALISATIONS または MAX_OPERATIONS を引き上げ、再実行して completion.classification: "complete" を要求します。意図的に汎用的/無制限のモデルについては、境界付きの結果を正直に報告し、網羅的ゲートが重要な場合は別の小さな有限シナリオを追加してください。
リファインメントチェーンがある場合は、-m <machine> を使用してすべてのレベルでモデルチェックと wd を繰り返してください。
6. 質問に答える場合に限定して対象証跡を追加する
状態述語が到達可能かどうかという質問に対しては、目標トレースを使用します。
eventb-animate -m M --goal '<predicate>' --no-invariant --no-deadlock \
--save /tmp/scenario.json /tmp/model.zip
eventb-animate replay -m M -t /tmp/scenario.json /tmp/model.zip
目標に到達すると、意図的に終了コード1で終了します。PERFECT リプレイを要求してください。不変条件またはデッドロックの失敗があった場合は、モデルを変更する前にその反例を保存してリプレイしてください。
状態目標は、アクションがない、またはガードのみのイベントが発火したことを証明できません。これは有効状態に達するとすぐに停止する可能性があります。特定の遷移を確認するには、完全チェックの Covered operations ブロックを使用するか、テスト生成を対象にします。
eventb-animate testgen -m M --operations EVENT_NAME \
--out /tmp/scenario-traces /tmp/model.zip
これらのコマンドは、そのより狭い目的が該当する場合にのみ使用してください。
testgen: 特定の遷移を証拠として示す、またはリプレイ可能な操作フィクスチャを生成します。網羅的チェックよりも強力なゲートではなく、「未カバー」は決定的ではありません。--symbolic ic3|kinduction: 非有界の不変条件安全性チェック。デッドロックのチェック、イベントカバレッジの報告、トレースの提供は行いません。po: すでに.bpo/.bps証明を持つ既存のRodinプロジェクトをゲートします。import/export: Rodinとの相互運用。通常の作成ループではありません。
これらの条件付きワークフローについては references/tooling.md を参照してください。デフォルトのProBバックエンドが通常の作成パスです。
7. 読みやすい成果物で仕上げる
.eventb ファイルと、スコープ、モデル形状、平易な言葉での安全不変条件、リファインメント対応表（ある場合）、正確なチェックコマンド、完全性、イベントカバレッジ、WD結果、および意図的な抽象化を含む短い README.md を提供してください。クリーンな有界実行は「境界内でバグが見つからなかった」ことを意味します。完全な有限実行は、チェックされた到達可能な振る舞いのみを証明します。到達不能な状態のために強すぎる非帰納的不変条件を受け入れる可能性があります。これはEvent-Bの不変条件/リファインメント証明義務を解決するものではありません。その主張をサポートするのは該当する証明ゲートのみです。references/refinement.md の「モデルチェックは証明ではない」を参照してください。