Phát triển Từng Bước và Có Chứng Minh Cơ Học của Giao Thức Nhận Dạng Cây IEEE 1394

Giao thức nhận dạng cây IEEE 1394 minh họa tính đầy đủ của phương pháp lập trình sự kiện, được sử dụng cùng với Phương pháp B. Phương pháp này cung cấp một khung hoàn chỉnh để phát triển các mô hình toán học của các thuật toán phân tán. Một sự phát triển cụ thể được thực hiện dựa trên một loạt các mô hình ngày càng tinh vi hơn. Mỗi mô hình được tạo thành từ một số thuộc tính tĩnh (bất biến) và các phần động (các sự kiện có điều kiện). Tính nhất quán nội bộ của mỗi mô hình cũng như tính chính xác của nó liên quan đến sự trừu tượng trước đó được chứng minh bằng công cụ chứng minh của Atelier B, công cụ liên kết với phương pháp B. Trong trường hợp của giao thức nhận dạng cây IEEE 1394, mô hình ban đầu rất sơ khai: nó cung cấp các thuộc tính cơ bản của đồ thị (đối xứng, không chu trình, kết nối), và các phần động của nó chủ yếu chứa một sự kiện duy nhất chọn lãnh đạo trong một lần. Các tinh chỉnh tiếp theo giới thiệu nhiều sự kiện hơn, cho thấy cách mỗi nút của đồ thị tham gia không xác định vào cuộc bầu cử lãnh đạo. Ở một giai đoạn trong quá trình phát triển, việc truyền thông điệp được giới thiệu. Điều này gây ra một vấn đề tiềm năng về sự tranh chấp, giải pháp cho vấn đề này được đưa ra. Giai đoạn cuối của việc tinh chỉnh hoàn toàn địa phương hóa các sự kiện bằng cách làm cho chúng đưa ra quyết định dựa trên dữ liệu địa phương.