Imperial College London > Talks@ee.imperial > Featured talks > Incremental and Verified Modelling of the PCI Express Protocol

Incremental and Verified Modelling of the PCI Express Protocol

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact George A Constantinides.

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 modelling 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. Models are build incrementally using generic composition rules and each modelling step encapsulates a specific protocol feature. For verification, correctness results of the generic composition rules are instantiated and verification is spead over the incremental modelling process. Using this approach, we model major parts of PCI Express, including performance-related optimisations and fault-tolerance features, incrementally to control the complexity of the model. The work has been accomplished in the Isabelle/HOL theorem prover.

This talk is part of the Featured talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Changes to Talks@imperial | Privacy and Publicity