Incremental and Verified Modelling of the PCI Express Protocol
PCI Express is a modern, high-performance communication protocol implementing sophisticated features to meet today's performance demands. Although an off-chip protocol, PCI Express implements many principles of future on-chip communication architectures. It is a highly complex protocol that is...
| Main Author: | |
|---|---|
| Format: | Journal article |
| Published: |
2010
|
| _version_ | 1797106041035423744 |
|---|---|
| author | Böhm, P |
| author_facet | Böhm, P |
| author_sort | Böhm, P |
| collection | OXFORD |
| description | PCI Express is a modern, high-performance communication protocol implementing sophisticated features to meet today's performance demands. Although an off-chip protocol, PCI Express implements many principles of future on-chip communication architectures. It is a highly complex protocol that is hard to verify formally. We present the application of a new approach to the PCI Express transaction and data link layers. The methodology is based on a series of model transformation steps and revises the traditional modelling and verification workflow for designing on-chip protocols. Major parts of PCI Express, including performance-related optimisations and fault-tolerance features, are modelled incrementally to control the complexity and composed to a single model. The work has been accomplished in the Isabelle/HOL theorem prover. By restricting the models to an executable subset of the specification language, we have been able to combine the advantages of specifying in a theorem prover with the advantages of executable models in a functional programming language. |
| first_indexed | 2024-03-07T06:56:02Z |
| format | Journal article |
| id | oxford-uuid:fe2cd476-e690-4dec-993c-e6b6ad6288be |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:56:02Z |
| publishDate | 2010 |
| record_format | dspace |
| spelling | oxford-uuid:fe2cd476-e690-4dec-993c-e6b6ad6288be2022-03-27T13:34:20ZIncremental and Verified Modelling of the PCI Express ProtocolJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:fe2cd476-e690-4dec-993c-e6b6ad6288beDepartment of Computer Science2010Böhm, PPCI Express is a modern, high-performance communication protocol implementing sophisticated features to meet today's performance demands. Although an off-chip protocol, PCI Express implements many principles of future on-chip communication architectures. It is a highly complex protocol that is hard to verify formally. We present the application of a new approach to the PCI Express transaction and data link layers. The methodology is based on a series of model transformation steps and revises the traditional modelling and verification workflow for designing on-chip protocols. Major parts of PCI Express, including performance-related optimisations and fault-tolerance features, are modelled incrementally to control the complexity and composed to a single model. The work has been accomplished in the Isabelle/HOL theorem prover. By restricting the models to an executable subset of the specification language, we have been able to combine the advantages of specifying in a theorem prover with the advantages of executable models in a functional programming language. |
| spellingShingle | Böhm, P Incremental and Verified Modelling of the PCI Express Protocol |
| title | Incremental and Verified Modelling of the PCI Express Protocol |
| title_full | Incremental and Verified Modelling of the PCI Express Protocol |
| title_fullStr | Incremental and Verified Modelling of the PCI Express Protocol |
| title_full_unstemmed | Incremental and Verified Modelling of the PCI Express Protocol |
| title_short | Incremental and Verified Modelling of the PCI Express Protocol |
| title_sort | incremental and verified modelling of the pci express protocol |
| work_keys_str_mv | AT bohmp incrementalandverifiedmodellingofthepciexpressprotocol |