Incremental Modelling and Verification of the PCI Express Transaction Layer
PCI Express is a modern, high-performance communication protocol implementing highly 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 w...
| Glavni autor: | |
|---|---|
| Format: | Conference item |
| Izdano: |
IEEE
2009
|
| _version_ | 1826296953678331904 |
|---|---|
| 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 highly 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 which is naturally hard to verify formally. We recently proposed a new methodology, based on a series of model transformation steps, to revise the traditional modelling and verification workflow for designing on-chip protocols. We present the application of the new approach to the PCI Express transaction layer. 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-07T04:24:15Z |
| format | Conference item |
| id | oxford-uuid:cc11f45c-83c6-4d2e-b389-280d5bb3c145 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T04:24:15Z |
| publishDate | 2009 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:cc11f45c-83c6-4d2e-b389-280d5bb3c1452022-03-27T07:19:15ZIncremental Modelling and Verification of the PCI Express Transaction LayerConference itemhttp://purl.org/coar/resource_type/c_5794uuid:cc11f45c-83c6-4d2e-b389-280d5bb3c145Department of Computer ScienceIEEE2009Böhm, PPCI Express is a modern, high-performance communication protocol implementing highly 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 which is naturally hard to verify formally. We recently proposed a new methodology, based on a series of model transformation steps, to revise the traditional modelling and verification workflow for designing on-chip protocols. We present the application of the new approach to the PCI Express transaction layer. 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 Modelling and Verification of the PCI Express Transaction Layer |
| title | Incremental Modelling and Verification of the PCI Express Transaction Layer |
| title_full | Incremental Modelling and Verification of the PCI Express Transaction Layer |
| title_fullStr | Incremental Modelling and Verification of the PCI Express Transaction Layer |
| title_full_unstemmed | Incremental Modelling and Verification of the PCI Express Transaction Layer |
| title_short | Incremental Modelling and Verification of the PCI Express Transaction Layer |
| title_sort | incremental modelling and verification of the pci express transaction layer |
| work_keys_str_mv | AT bohmp incrementalmodellingandverificationofthepciexpresstransactionlayer |