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

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

• Peter Boehm - University of Oxford
• Tuesday 23 March 2010, 14:00-15:00
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

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 (www.verisoft.de), 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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.