University of Cambridge > > Microsoft Research Cambridge, public talks > Incremental Modelling and Verification of the PCI Express Transaction and Data-Link Layers

Incremental Modelling and Verification of the PCI Express Transaction and Data-Link Layers

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

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Abstract: PCI Express is a 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 hard to verify formally. We recently proposed a new methodology to replace the traditional formal modelling and verification workflow for designing on-chip protocols. The approach provides a structural approach to incrementally construct models and spread the verification process over the modelling workflow.

In this talk, we present the application of the new approach to the PCI Express transaction and data-link layers. We construct models of both layers using our incremental modelling approach and argue about the correctness. To achieve this, we introduce generic modelling constructs that we can reuse to carry out specific modelling steps. The work has been accomplished in higher order logic using the Isabelle/HOL theorem prover.

Biography: I am currently a PhD student at the University of Oxford. My research focuses on verified on-chip communication protocols for high-performance multicore or System-on-Chip architectures. The project is sponsored by the Engineering and Physical Sciences Research Council (EPSRC) and the Intel Corporation.

Before joining the verification group in Oxford, I obtained my M.Sc (Honour`s Degree) in Computer Science at Saarland University, Germany at the chair for Computer Architecture and Parallel Computing of Prof. Wolfgang Paul. My work contributed to the Verisoft project (, in particular to the verification of an automotive system, covering both the design of a communication controller and the formal verification of the system in HOL using the Isabelle theorem prover (functional correctness and scheduling).

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2019, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity