A Design-for-Verification approach of a Configurable Performance-Critical Concurrent Communication Interface

Suleiman Abu Kharmeh (University of Bristol)

Info

Date	9th February 2011 (week 4, Hilary Term 2011)
Time	11:30
Place	Room 147, Oxford University Computing Laboratory

Abstract

We present a Design-for-Verification approach for a configurable performance-critical concurrent communication interface. To manage the inherent complexity of the problem we decomposed the interface into independent parameterizable communication blocks. Tock-CSP was then used to model the timing and functional specifications of our interface. The FDR2 model checker and its tau-priority model were used to prove that the properties of the configured interface are within the properties of targeted communication protocols.