核心概念
IEEE 1394リンク層の4つの正式なモデルを提示し、それらの主な特徴を議論する。
要約
本論文では、IEEE 1394リンク層の4つの正式なモデルを提示する。
最初のモデルはµCRLで記述されたものであり、1997年にB. Luttikによって開発された。このモデルは、その後H. Garavel、J.F. Groote、M. Sighireanuによって改善された。
次にLOTOSモデルが1997年にM. Sighireanuによって開発された。このモデルは、CADPツールセットを使ってモデル検査を行うことを目的としていた。2023年にH. Garavel によって大幅に改訂された。
2005年にJ.F. Grooteによってmcrl2モデルが開発された。このモデルはµCRLモデルを翻訳したものであり、データ型定義の簡潔さが特徴である。
最後に、2022年にO. Oulkaidとm. Kemehによってlntモデルが開発された。このモデルはlotosモデルを系統的に翻訳したものであるが、その後H. Garavel によって大幅に改訂され、lntの特徴を活かした形になった。
これらのモデルは、通信プロトコルの形式的な分析に関する重要な事例研究である。各モデルの主な特徴が議論されている。
統計
IEEE 1394規格の策定には100人以上の専門家が10年以上かけて取り組んだ。
3人の博士課程学生が数週間でデッドロックエラーを発見した。
引用
"IEEE 1394 (also called "FireWire") is an interface standard that specifies a serial bus architecture for high-speed communications."
"Although the IEEE 1934 serial bus is no longer used today (deployed in Apple products from 1999 to 2016, it has been gradually replaced by USB 2, USB 3, and Gigabit Ethernet), it is an inspiring example for the formal methods community."