An executable specification of the PCI-X bus standard in AsmL

In this paper, we describe an executable formal specification of the PCI-X bus standard using the abstract state machines language, AsmL. PCI-X, is the latest extension of the PCI local bus that is designed to meet increased I/O demands of recent technologies. The actual specification of PCI-X, provided by the PCI special interest group (PCI-SIG), is informal (in natural English). Hence, it is prone to inherent problems of incompleteness, inconsistency and ambiguity. In our approach, we first model the bus in UML and then map it to AsmL. This AsmL model can be executed using the Asmlt tool that can generate the finite state machine (FSM) of the model. Such FSM can be of great use for verification purposes