BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Incremental Modelling and Verification of the PCI Express Transact
 ion and Data-Link Layers - Peter Boehm - University of Oxford
DTSTART:20100423T130000Z
DTEND:20100423T140000Z
UID:TALK23997@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:*Abstract:* PCI Express is a high-performance communication pr
 otocol implementing highly sophisticated features to meet today`s performa
 nce demands. Although an off-chip protocol\, PCI Express implements many p
 rinciples of future on-chip communication architectures. It is a highly co
 mplex protocol which is hard to verify formally. We recently proposed a ne
 w methodology to replace the traditional formal modelling and verification
  workflow for designing on-chip protocols. The approach provides a structu
 ral approach to incrementally construct models and spread the verification
  process over the modelling workflow.\n\nIn this talk\, we present the app
 lication 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 model
 ling steps. The work has been accomplished in higher order logic using the
  Isabelle/HOL theorem prover. \n\n*Biography:* I am currently a PhD studen
 t at the University of Oxford. My research focuses on verified on-chip com
 munication protocols for high-performance multicore or System-on-Chip arch
 itectures. The project is sponsored by the Engineering and Physical Scienc
 es Research Council (EPSRC) and the Intel Corporation.\n\nBefore joining t
 he verification group in Oxford\, I obtained my M.Sc (Honour`s Degree) in 
 Computer Science at Saarland University\, Germany at the chair for Compute
 r Architecture and Parallel Computing of Prof. Wolfgang Paul. My work cont
 ributed to the Verisoft project (www.verisoft.de)\, in particular to the v
 erification of an automotive system\, covering both the design of a commun
 ication controller and the formal verification of the system in HOL using 
 the Isabelle theorem prover (functional correctness and scheduling).
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR